Matrix algebra of e.left.to.show

Source: enhance.tex 8271–8470. The partition of unity turns the identity parts of F = ∑_k ξ_{m,k} (I + ∇Χ_{m,k}) ∘ X⁻¹ into I, and the orthogonality e.alt.orth of adjacent odd shear gradients (in two independent points) kills the cross terms of FᵗF (e.Emkappa.formula). Also the elementary quadratic-form bounds and the scalar value ⟨⟨J_m^{κ_m}⟩⟩ = κ_{m-1} I.

theorem AVenhance.Infra.Section5.LeftToShow.gram_expansion_of_cross_eq_zero {ι : Type u_1} (S : Finset ι) (ξ : ι → ℝ) (A : ι → Matrix (Fin 2) (Fin 2) ℝ) (hcross : ∀ k ∈ S, ∀ l ∈ S, k ≠ l → (A k).transpose * A l = 0) : (1 + ∑ k ∈ S, ξ k • A k).transpose * (1 + ∑ k ∈ S, ξ k • A k) = 1 + ∑ k ∈ S, (ξ k • ((A k).transpose + A k) + ξ k ^ 2 • ((A k).transpose * A k))

Abstract Gram expansion: if the cross products vanish for distinct indices of S, then (1 + ∑ ξ_k A_k)ᵀ (1 + ∑ ξ_k A_k) = 1 + ∑ (ξ_k (A_kᵀ + A_k) + ξ_k² A_kᵀ A_k).

theorem AVenhance.Infra.Section5.LeftToShow.leadingMatrix_eq_finset {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κm t : ℝ) (x : Homogenization.Vec 2) : leadingMatrix I hΦ m κm t x = 1 + ∑ k ∈ ⋯.toFinset, I.xiMK m (↑k) t • gradMatrix (I.chiMK κm m (↑k) t) (I.xFlowInv hΦ m (lIdx β I.Λ m ↑k) t x)

F as a finite sum: the partition of unity ∑_{k odd} ξ_{m,k} = 1 turns the I parts into I.

theorem AVenhance.Infra.Section5.LeftToShow.leadingMatrix_transpose_mul {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κm t : ℝ) (x : Homogenization.Vec 2) : (leadingMatrix I hΦ m κm t x).transpose * leadingMatrix I hΦ m κm t x = 1 + ∑ k ∈ ⋯.toFinset, (I.xiMK m (↑k) t • ((gradMatrix (I.chiMK κm m (↑k) t) (I.xFlowInv hΦ m (lIdx β I.Λ m ↑k) t x)).transpose + gradMatrix (I.chiMK κm m (↑k) t) (I.xFlowInv hΦ m (lIdx β I.Λ m ↑k) t x)) + I.xiMK m (↑k) t ^ 2 • ((gradMatrix (I.chiMK κm m (↑k) t) (I.xFlowInv hΦ m (lIdx β I.Λ m ↑k) t x)).transpose * gradMatrix (I.chiMK κm m (↑k) t) (I.xFlowInv hΦ m (lIdx β I.Λ m ↑k) t x)))

Source 8402–8435: FᵗF with the cross terms killed (e.alt.orth for |k-k'| = 2, disjoint supports for |k-k'| ≥ 4).

theorem AVenhance.Infra.Section5.LeftToShow.vecNormSq_mulVec (A : Matrix (Fin 2) (Fin 2) ℝ) (v : Homogenization.Vec 2) : Homogenization.vecNormSq (A.mulVec v) = Homogenization.vecDot v ((A.transpose * A).mulVec v)

theorem AVenhance.Infra.Section5.LeftToShow.Matrix.abs_mul_mul_le {a B x y : ℝ} (ha : |a| ≤ B) : |a * x * y| ≤ B * ((x ^ 2 + y ^ 2) / 2)

theorem AVenhance.Infra.Section5.LeftToShow.abs_vecDot_mulVec_le {A : Matrix (Fin 2) (Fin 2) ℝ} {B : ℝ} (hA : ∀ (i j : Fin 2), |A i j| ≤ B) (v : Homogenization.Vec 2) : |Homogenization.vecDot v (A.mulVec v)| ≤ 2 * B * Homogenization.vecNormSq v

theorem AVenhance.Infra.Section5.LeftToShow.kappaSeq_pos {β : ℝ} (I : Ingredients β) {κ : ℝ} (hκ : 0 < κ) (M m : ℕ) : 0 < I.kappaSeq κ M m

The positivity of the sequence κ_m from a positive terminal value.

theorem AVenhance.Infra.Section5.LeftToShow.timeAvgMat_flux_kappaSeq {β : ℝ} (I : Ingredients β) (κ : ℝ) {M m : ℕ} (hm : 1 ≤ m) (hmM : m ≤ M) (hκm : 0 < I.kappaSeq κ M m) : (timeAvgMat fun (t : ℝ) => I.flux (I.kappaSeq κ M m) m t) = I.kappaSeq κ M (m - 1) • 1

Fourth term of e.ergodic.break.up is zero: ⟨⟨J_m^{κ_m}⟩⟩ = KBar_m^{κ_m} = κ_{m-1} I (source 8395; the printed "κ_m I_2" is a typo for κ_{m-1} I_2).