The four-term break-up e.ergodic.break.up #
Source: enhance.tex 8305–8394. The source's triangle inequality is the exact identity
ergodic_break_up: every term is a continuous function of time on [0,1], the spatial
quadratic form A ↦ ∫ ∇T·A∇T is linear in A, and the quantities telescope.
theorem
AVenhance.Infra.Section5.LeftToShow.continuousOn_quadForm
{X : Type u_1}
[TopologicalSpace X]
{s : Set X}
{A : X → Matrix (Fin 2) (Fin 2) ℝ}
{u : X → Homogenization.Vec 2}
(hA : ∀ (i j : Fin 2), ContinuousOn (fun (p : X) => A p i j) s)
(hu : ∀ (i : Fin 2), ContinuousOn (fun (p : X) => u p i) s)
:
ContinuousOn (fun (p : X) => Homogenization.vecDot (u p) ((A p).mulVec (u p))) s
Continuity of the quadratic form u ↦ u·A u in terms of continuity of the entries.
theorem
AVenhance.Infra.Section5.LeftToShow.intervalIntegrable_of_continuousOn_Icc
{f : ℝ → ℝ}
(hf : ContinuousOn f (Set.Icc 0 1))
:
theorem
AVenhance.Infra.Section5.LeftToShow.gradQuad_smul_one
(T : ℝ → Homogenization.Vec 2 → ℝ)
(c t : ℝ)
:
theorem
AVenhance.Infra.Section5.LeftToShow.continuousOn_gradQuad
{T : ℝ → Homogenization.Vec 2 → ℝ}
(hg : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => spaceGrad (T p.1) p.2) (Set.Icc 0 1 ×ˢ Set.univ))
{M : ℝ → Matrix (Fin 2) (Fin 2) ℝ}
(hM : ∀ (i j : Fin 2), ContinuousOn (fun (t : ℝ) => M t i j) (Set.Icc 0 1))
:
ContinuousOn (fun (t : ℝ) => gradQuad T (M t) t) (Set.Icc 0 1)
t ↦ ∫ ∇T(t)·M(t) ∇T(t) is continuous on [0,1] for a matrix field with continuous
entries.
theorem
AVenhance.Infra.Section5.LeftToShow.leadingGramAvg_continuousOn
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 1 ≤ m)
{κm : ℝ}
(hκm : 0 < κm)
(i j : Fin 2)
:
ContinuousOn (fun (t : ℝ) => leadingGramAvg I hΦ m κm t i j) (Set.Icc 0 1)
The space average ⟨FᵗF⟩(t) has continuous entries.
theorem
AVenhance.Infra.Section5.LeftToShow.ergodic_break_up
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 1 ≤ m)
{κm : ℝ}
(hκm : 0 < κm)
(κp : ℝ)
{T : ℝ → Homogenization.Vec 2 → ℝ}
(hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ))
(J : ℝ → Matrix (Fin 2) (Fin 2) ℝ)
(hJ : ∀ (i j : Fin 2), Continuous fun (t : ℝ) => J t i j)
:
(κm * spaceTimeGradNormSq (leadingGrad I hΦ m κm T) - κp * spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (T t) x) = ((κm * ∫ (t : ℝ) in 0..1, (∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (leadingGrad I hΦ m κm T t x)) - gradQuad T (leadingGramAvg I hΦ m κm t) t) + ∫ (t : ℝ) in 0..1, gradQuad T (κm • leadingGramAvg I hΦ m κm t - J t) t) + ((∫ (t : ℝ) in 0..1, gradQuad T (J t) t) - ∫ (t : ℝ) in 0..1, gradQuad T (timeAvgMat J) t) + ((∫ (t : ℝ) in 0..1, gradQuad T (timeAvgMat J) t) - κp * ∫ (t : ℝ) in 0..1, ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (spaceGrad (T t) x))
e.ergodic.break.up (source 8305–8394) as an exact identity; the source's inequality is its
triangle inequality. J is any matrix field with continuous entries (it will be J_m^{κ_m}).