e.bracket.FF and e.ergodic.break.up.second

Source: enhance.tex 8396–8510. The space average of FᵗF equals the reduced energy E_m(t): the linear terms ⟨∇Χ_{m,k} ∘ X⁻¹⟩ vanish (mean-zero sines), the quadratic terms are ⟨(∇Χ)ᵗ∇Χ ∘ X⁻¹⟩ = ⟨(∇Χ)ᵗ∇Χ⟩ by measure preservation of the inverse flow, and this is the diagonal matrix movingEnergyGramMean. Then l.flux.to.energy bounds κ_m⟨FᵗF⟩ - J_m.

The explicit corrector gradient entries

theorem AVenhance.Infra.Section5.LeftToShow.gradMatrix_chiMK_entry_form {β : ℝ} (I : Ingredients β) (m : ℕ) (κ : ℝ) (k : ℤ) (t : ℝ) (i j : Fin 2) : ∃ (c : ℝ) (r : Fin 2), ∀ (y : Homogenization.Vec 2), gradMatrix (I.chiMK κ m k t) y i j = c * Real.sin (2 * Real.pi * y r / epsilon β I.Λ m)

Every entry of ∇Χ_{m,k} is a constant multiple of a single-coordinate sine (the constant is 0 for even k, where Χ_{m,k} = 0).

theorem AVenhance.Infra.Section5.LeftToShow.gradMatrix_chiMK_periodic {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (k : ℤ) (t : ℝ) : Ergodic.IsZPeriodic fun (y : Homogenization.Vec 2) => gradMatrix (I.chiMK κ m k t) y

∇Χ_{m,k} is ℤ²-periodic.

theorem AVenhance.Infra.Section5.LeftToShow.spaceAvg_gradMatrix_chiMK {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (k : ℤ) (t : ℝ) (i j : Fin 2) : (spaceAvg fun (y : Homogenization.Vec 2) => gradMatrix (I.chiMK κ m k t) y i j) = 0

The mean of each entry of ∇Χ_{m,k} vanishes.

Averages composed with the inverse flow

theorem AVenhance.Infra.Section5.LeftToShow.spaceAvg_eq_cellAverage (f : Homogenization.Vec 2 → ℝ) : spaceAvg f = Ergodic.cellAverage f

theorem AVenhance.Infra.Section5.LeftToShow.spaceAvg_comp_xFlowInv {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) {g : Homogenization.Vec 2 → ℝ} (hg : Ergodic.IsZPeriodic g) : (spaceAvg fun (x : Homogenization.Vec 2) => g (I.xFlowInv hΦ m l t x)) = spaceAvg g

A ℤ²-periodic function has the same space average after composing with X⁻¹_{m-1,l}(t,·).

theorem AVenhance.Infra.Section5.LeftToShow.spaceAvg_gradMatrix_chiMK_comp_xFlowInv {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κm : ℝ) (k l : ℤ) (t : ℝ) (i j : Fin 2) : (spaceAvg fun (x : Homogenization.Vec 2) => gradMatrix (I.chiMK κm m k t) (I.xFlowInv hΦ m l t x) i j) = 0

⟨∇Χ_{m,k}(t,·)⟩ = 0 and the inverse-flow average.

theorem AVenhance.Infra.Section5.LeftToShow.spaceAvg_gram_chiMK_comp_xFlowInv {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κm : ℝ) (k l : ℤ) (t : ℝ) (i j : Fin 2) : (spaceAvg fun (x : Homogenization.Vec 2) => ((gradMatrix (I.chiMK κm m k t) (I.xFlowInv hΦ m l t x)).transpose * gradMatrix (I.chiMK κm m k t) (I.xFlowInv hΦ m l t x)) i j) = Section3.movingEnergyGramMean I κm m k t i j

Linearity of the space average on continuous functions

theorem AVenhance.Infra.Section5.LeftToShow.BracketFF.spaceAvg_const' (c : ℝ) : (spaceAvg fun (x : Homogenization.Vec 2) => c) = c

theorem AVenhance.Infra.Section5.LeftToShow.BracketFF.spaceAvg_add' {f g : Homogenization.Vec 2 → ℝ} (hf : Continuous f) (hg : Continuous g) : (spaceAvg fun (x : Homogenization.Vec 2) => f x + g x) = spaceAvg f + spaceAvg g

theorem AVenhance.Infra.Section5.LeftToShow.BracketFF.spaceAvg_const_mul' (c : ℝ) (f : Homogenization.Vec 2 → ℝ) : (spaceAvg fun (x : Homogenization.Vec 2) => c * f x) = c * spaceAvg f

theorem AVenhance.Infra.Section5.LeftToShow.BracketFF.spaceAvg_sum' {ι : Type u_1} (S : Finset ι) {f : ι → Homogenization.Vec 2 → ℝ} (hf : ∀ k ∈ S, Continuous (f k)) : (spaceAvg fun (x : Homogenization.Vec 2) => ∑ k ∈ S, f k x) = ∑ k ∈ S, spaceAvg (f k)

The space average of FᵗF

theorem AVenhance.Infra.Section5.LeftToShow.BracketFF.continuous_gradMatrix_comp {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) {k : ℤ} (hk : Odd k) (l : ℤ) (t : ℝ) : Continuous fun (x : Homogenization.Vec 2) => gradMatrix (I.chiMK κm m k t) (I.xFlowInv hΦ m l t x)

Continuity in x of the composed corrector gradient.

theorem AVenhance.Infra.Section5.LeftToShow.BracketFF.spaceAvg_summand {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κm t : ℝ) {k : ℤ} (hk : Odd k) (i j : Fin 2) : (spaceAvg fun (x : Homogenization.Vec 2) => I.xiMK m k t * ((gradMatrix (I.chiMK κm m k t) (I.xFlowInv hΦ m (lIdx β I.Λ m k) t x)).transpose i j + gradMatrix (I.chiMK κm m k t) (I.xFlowInv hΦ m (lIdx β I.Λ m k) t x) i j) + 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)) i j) = I.xiMK m k t ^ 2 * Section3.movingEnergyGramMean I κm m k t i j

One summand of ⟨FᵗF⟩: the linear terms vanish and the quadratic term is the Gram mean.

theorem AVenhance.Infra.Section5.LeftToShow.spaceAvg_leadingGram_entry {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κm t : ℝ) (i j : Fin 2) : (spaceAvg fun (x : Homogenization.Vec 2) => ((leadingMatrix I hΦ m κm t x).transpose * leadingMatrix I hΦ m κm t x) i j) = 1 i j + ∑ k ∈ ⋯.toFinset, I.xiMK m (↑k) t ^ 2 * Section3.movingEnergyGramMean I κm m (↑k) t i j

Entry (i,j) of ⟨FᵗF⟩: δ_{ij} + ∑_k ξ_{m,k}² ⟨(∇Χ_{m,k})ᵗ∇Χ_{m,k}⟩_{ij}.

theorem AVenhance.Infra.Section5.LeftToShow.movingEnergyGramMean_offDiag {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) {k : ℤ} (hk : Odd k) (t : ℝ) {i j : Fin 2} (hij : i ≠ j) : Section3.movingEnergyGramMean I κ m k t i j = 0

The Gram means of the odd shear correctors are diagonal.

theorem AVenhance.Infra.Section5.LeftToShow.bracket_FF {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm : ℝ} (_hκm : 0 < κm) (t : ℝ) : κm • leadingGramAvg I hΦ m κm t = Section3.movingEnergyReducedSourceMatrix I κm m t ⋯.toFinset

e.bracket.FF (8436–8465): κ_m ⟨FᵗF⟩(t) = E_m(t).

The second term of the break-up

theorem AVenhance.Infra.Section5.LeftToShow.second_term_entry_abs_le {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {C₀ : ℝ} (hΦ : IsStreamSeq I Φ) (hCz : I.Czeta ≤ C₀) (hCh : I.Chat ≤ C₀) {m : ℕ} (hm : 1 ≤ m) {κm : ℝ} (hκm : 0 < κm) (t : ℝ) (hcondition : epsilon β I.Λ m ^ 2 ≤ κm * tau β I.Λ m / 2) (i j : Fin 2) : |(κm • leadingGramAvg I hΦ m κm t - I.flux κm m t) i j| ≤ Section3.lFluxToEnergyConstant C₀ * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κm) * (epsilon β I.Λ m ^ 2 / (κm * tau β I.Λ m))

e.ergodic.break.up.second, pointwise in t, entrywise (via l.flux.to.energy).

theorem AVenhance.Infra.Section5.LeftToShow.ergodic_break_up_second {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {C₀ : ℝ} (hΦ : IsStreamSeq I Φ) (hCz : I.Czeta ≤ C₀) (hCh : I.Chat ≤ C₀) {m : ℕ} (hm : 1 ≤ m) {κm : ℝ} (hκm : 0 < κm) (hcondition : epsilon β I.Λ m ^ 2 ≤ κm * tau β I.Λ m / 2) {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) : |∫ (t : ℝ) in 0..1, gradQuad T (κm • leadingGramAvg I hΦ m κm t - I.flux κm m t) t| ≤ 2 * (Section3.lFluxToEnergyConstant C₀ * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κm) * (epsilon β I.Λ m ^ 2 / (κm * tau β I.Λ m))) * spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (T t) x

e.ergodic.break.up.second integrated in time.