Facts about JHat_m and the replacement J_m → JHat_m of e.TJT.break

Source: enhance.tex 3040–3190 (e.Jhat, e.JJhat, e.jkmn, e.Lmn.def) and 8640–8780 (e.TJT.break). JHat_m^κ = κ I + ∑_{n<N_*} L_{m,n} 𝐣_{m,n} is continuous and 4τ''_m-periodic, is within a_m² ε_m⁴/κ of κ I, and replacing J_m by JHat_m in the time-averaged quadratic form costs the e.JJhat error.

theorem AVenhance.Infra.Section5.LeftToShow.Jhat_entry_continuous_pub {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (i j : Fin 2) : Continuous fun (t : ℝ) => I.Jhat κ m t i j

Public continuity of JHat entries.

theorem AVenhance.Infra.Section5.LeftToShow.Jhat_entry_periodic {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (i j : Fin 2) : Function.Periodic (fun (t : ℝ) => I.Jhat κ m t i j) (4 * tauPP β I.Λ m)

theorem AVenhance.Infra.Section5.LeftToShow.LMN_mul_jMN_abs_bound (n : ℕ) {A E κ τ C : ℝ} (hA : 0 ≤ A) (hE : 0 < E) (hκ : 0 < κ) (hτ : 0 < τ) (hC : 0 ≤ C) (hr : E / (κ * τ) ≤ 1) : ↑n.factorial * 2 ^ n * (4 * Real.pi ^ 2 * κ / E / 2)⁻¹ * (2 * Real.pi ^ 2 * A * E / ↑n.factorial * (E / (4 * Real.pi ^ 2 * κ)) ^ n * (C / τ ^ n)) ≤ C * (A * E ^ 2 / κ)

Abstract-real core of the L_{m,n} 𝐣_{m,n} size: n! 2ⁿ (E/(2π²κ)) times (2π²AE/n!)(E/(4π²κ))ⁿ (C/τⁿ) is at most C A E²/κ once E/(κτ) ≤ 1.

theorem AVenhance.Infra.Section5.LeftToShow.Jhat_sub_kappa_entry_abs_le (β C₀ : ℝ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → ∀ (m : ℕ), 1 ≤ m → ∀ (κ : ℝ), 0 < κ → epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m) ≤ 1 → ∀ (t : ℝ) (i j : Fin 2), |(I.Jhat κ m t - κ • 1) i j| ≤ K * (AVenhance.a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ)

sup |JHat_m^κ - κ I| ≲ a_m² ε_m⁴ / κ when ε_m²/(κ τ_m) ≤ 1.

theorem AVenhance.Infra.Section5.LeftToShow.timeAvgMat_sub_entry_eq_integral' {F G : ℝ → Matrix (Fin 2) (Fin 2) ℝ} (i j : Fin 2) (hf : Continuous fun (t : ℝ) => F t i j) (hg : Continuous fun (t : ℝ) => G t i j) : (timeAvgMat F - timeAvgMat G) i j = ∫ (t : ℝ) in 0..1, (F t - G t) i j

Entrywise difference of time averages is the average of the entrywise difference.

theorem AVenhance.Infra.Section5.LeftToShow.Jhat_sub_timeAvg_entry_abs_le {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) {B : ℝ} (hB : ∀ (t : ℝ) (i j : Fin 2), |(I.Jhat κ m t - κ • 1) i j| ≤ B) (t : ℝ) (i j : Fin 2) : |(I.Jhat κ m t - timeAvgMat (I.Jhat κ m)) i j| ≤ 2 * B

theorem AVenhance.Infra.Section5.LeftToShow.TJT_break {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κm : ℝ} (hκm : 0 < κm) {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 (I.flux κm m t) t) - ∫ (t : ℝ) in 0..1, gradQuad T (timeAvgMat fun (s : ℝ) => I.flux κm m s) t| ≤ |(∫ (t : ℝ) in 0..1, gradQuad T (I.Jhat κm m t) t) - ∫ (t : ℝ) in 0..1, gradQuad T (timeAvgMat (I.Jhat κm m)) t| + 4 * (4 * Real.pi ^ 2 * I.Czeta * ↑(Nstar β) * 2 ^ Nstar β * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κm) * (epsilon β I.Λ m ^ 2 / (κm * tau β I.Λ m)) ^ Nstar β) * ∫ (t : ℝ) in 0..1, ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (spaceGrad (T t) x)

e.TJT.break: replacing J_m by JHat_m costs the e.JJhat error.