The top power of a real 2-form on a weighted pair tuple

Category: 1-Mathlib (CSD-free; upstream target Mathlib.Analysis.Normed.Module.Alternating).

A tuple of 2k vectors is a weighted pair tuple for the 2-form β when β pairs the two members of pair j (the slots 2j and 2j + 1) to ± c j and kills everything else. On such a tuple the k-th exterior power of β (ContinuousAlternatingMap.wedgePow) is k! times the product of the weights: through the shuffle sum on a weighted pair family (wedge_mul_apply_weightedPairs) each of the k + 1 pairs is moved into the last two slots in turn, and what is left behind is a weighted pair tuple of k pairs.

• pairIdx, memIdx — the pair and the member a slot of Fin (2k) belongs to; pairIdx_powEquiv, memIdx_powEquiv — through the re-indexing powEquiv k : Fin (2k) ⊕ Fin 2 ≃ Fin (2(k+1)) the power recurses along, they are slotPair and slotMem;
• IsWeightedPairTuple β c u, with isWeightedPairTuple_iff (the family form through powEquiv) and IsWeightedPairTuple.pairRep (moving one pair into the last two slots leaves a weighted pair tuple, with that pair's weight replaced by the last one's: removeWeight);
• ★★ wedgePow_apply_of_isWeightedPairTuple — the count: β^{∧k} u = k! · ∏ⱼ c j; ★ wedgePow_apply_of_isPairTuple — all weights 1: β^{∧k} u = k!.

Honest scope

⚠️ Real-valued 2-forms, and the tuple must be paired by β exactly; nothing is said about β^{∧k} on other tuples.

References: Alternating/WedgeShuffle.lean (the shuffle sum); Geometry/Manifold/WedgeForm.lean (wedgePow, powEquiv); consumers Instances/ProjectiveSpaceFubiniStudyVolume.lean (the standard symplectic form on standard pairs) and Instances/ProjectiveSpaceTorusVolume.lean (the sum of the Fubini–Study form and the torus area form on the product basis).

Pairs and members of Fin (2k)

def ContinuousAlternatingMap.pairIdx {k : ℕ} (p : Fin (2 * k)) : Fin k

The pair a slot of Fin (2k) belongs to.

Equations

• ContinuousAlternatingMap.pairIdx p = ⟨↑p / 2, ⋯⟩

theorem ContinuousAlternatingMap.pairIdx_def {k : ℕ} (p : Fin (2 * k)) : pairIdx p = ⟨↑p / 2, ⋯⟩

pairIdx, unfolded: the definitional equation.

def ContinuousAlternatingMap.memIdx {k : ℕ} (p : Fin (2 * k)) : Fin 2

Which member of its pair a slot of Fin (2k) is.

Equations

• ContinuousAlternatingMap.memIdx p = ⟨↑p % 2, ⋯⟩

theorem ContinuousAlternatingMap.memIdx_def {k : ℕ} (p : Fin (2 * k)) : memIdx p = ⟨↑p % 2, ⋯⟩

memIdx, unfolded: the definitional equation.

theorem ContinuousAlternatingMap.coe_powEquiv_inl {k : ℕ} (p : Fin (2 * k)) : ↑((DifferentialForm.powEquiv k) (Sum.inl p)) = ↑p

theorem ContinuousAlternatingMap.coe_powEquiv_inr {k : ℕ} (b : Fin 2) : ↑((DifferentialForm.powEquiv k) (Sum.inr b)) = 2 * k + ↑b

theorem ContinuousAlternatingMap.pairIdx_powEquiv_inl {k : ℕ} (p : Fin (2 * k)) : pairIdx ((DifferentialForm.powEquiv k) (Sum.inl p)) = slotPair (Sum.inl p)

theorem ContinuousAlternatingMap.pairIdx_powEquiv_inr {k : ℕ} (b : Fin 2) : pairIdx ((DifferentialForm.powEquiv k) (Sum.inr b)) = slotPair (Sum.inr b)

theorem ContinuousAlternatingMap.memIdx_powEquiv_inl {k : ℕ} (p : Fin (2 * k)) : memIdx ((DifferentialForm.powEquiv k) (Sum.inl p)) = slotMem (Sum.inl p)

theorem ContinuousAlternatingMap.memIdx_powEquiv_inr {k : ℕ} (b : Fin 2) : memIdx ((DifferentialForm.powEquiv k) (Sum.inr b)) = slotMem (Sum.inr b)

theorem ContinuousAlternatingMap.pairIdx_powEquiv {k : ℕ} (x : Fin (2 * k) ⊕ Fin 2) : pairIdx ((DifferentialForm.powEquiv k) x) = slotPair x

Through powEquiv, pairIdx is slotPair.

theorem ContinuousAlternatingMap.memIdx_powEquiv {k : ℕ} (x : Fin (2 * k) ⊕ Fin 2) : memIdx ((DifferentialForm.powEquiv k) x) = slotMem x

Through powEquiv, memIdx is slotMem.

theorem ContinuousAlternatingMap.slotPair_inl_eq_castSucc {k : ℕ} (p : Fin (2 * k)) : slotPair (Sum.inl p) = (pairIdx p).castSucc

The pair of an inl slot is its pairIdx, as a pair of k + 1.

theorem ContinuousAlternatingMap.slotMem_inl_eq_memIdx {k : ℕ} (p : Fin (2 * k)) : slotMem (Sum.inl p) = memIdx p

The member of an inl slot is its memIdx.

Weighted pair tuples

def ContinuousAlternatingMap.IsWeightedPairTuple {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {k : ℕ} (β : E [⋀^Fin 2]→L[ℝ] ℝ) (c : Fin k → ℝ) (u : Fin (2 * k) → E) : Prop

A tuple of 2k vectors is a weighted pair tuple for the 2-form β, with weights c, when β pairs the two members of pair j (the slots 2j and 2j + 1) to ± c j and kills everything else.

Equations

• One or more equations did not get rendered due to their size.

theorem ContinuousAlternatingMap.isWeightedPairTuple_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {k : ℕ} {β : E [⋀^Fin 2]→L[ℝ] ℝ} {c : Fin (k + 1) → ℝ} {u : Fin (2 * (k + 1)) → E} : β.IsWeightedPairTuple c u ↔ β.IsWeightedPairFamily c fun (x : Fin (2 * k) ⊕ Fin 2) => u ((DifferentialForm.powEquiv k) x)

A weighted pair tuple of k + 1 pairs, read through powEquiv k, is a weighted pair family, and conversely.

def ContinuousAlternatingMap.removeWeight {k : ℕ} (c : Fin (k + 1) → ℝ) (j : Fin (k + 1)) : Fin k → ℝ

The weights with pair j replaced by the last pair.

Equations

• ContinuousAlternatingMap.removeWeight c j i = if i.castSucc = j then c (Fin.last k) else c i.castSucc

theorem ContinuousAlternatingMap.mul_prod_removeWeight {k : ℕ} (c : Fin (k + 1) → ℝ) (j : Fin (k + 1)) : c j * ∏ i : Fin k, removeWeight c j i = ∏ i : Fin (k + 1), c i

The weight of pair j times the product of the remaining weights is the product of all.

theorem ContinuousAlternatingMap.IsWeightedPairTuple.pairRep {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {k : ℕ} {β : E [⋀^Fin 2]→L[ℝ] ℝ} {c : Fin (k + 1) → ℝ} {u : Fin (2 * (k + 1)) → E} (hu : β.IsWeightedPairTuple c u) (j : Fin (k + 1)) : β.IsWeightedPairTuple (removeWeight c j) fun (i : Fin (2 * k)) => u ((DifferentialForm.powEquiv k) ((ContinuousAlternatingMap.pairRep j) (Sum.inl i)))

Moving pair j into the last two slots (pairRep j) leaves a weighted pair tuple of k pairs, with the weight of pair j replaced by the last one's.

theorem ContinuousAlternatingMap.wedgePow_apply_of_isWeightedPairTuple {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (β : E [⋀^Fin 2]→L[ℝ] ℝ) (k : ℕ) (c : Fin k → ℝ) (u : Fin (2 * k) → E) : β.IsWeightedPairTuple c u → (β.wedgePow k) u = ↑k.factorial * ∏ j : Fin k, c j

★★ The count. The k-th power of a real 2-form on a weighted pair tuple of k pairs is k! times the product of the weights.

theorem ContinuousAlternatingMap.wedgePow_apply_of_isPairTuple {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {k : ℕ} (β : E [⋀^Fin 2]→L[ℝ] ℝ) {u : Fin (2 * k) → E} (hu : β.IsWeightedPairTuple (fun (x : Fin k) => 1) u) : (β.wedgePow k) u = ↑k.factorial

★ On a pair tuple (all weights 1) the k-th power is k!.