e.ergodic.space.kill at a fixed time #
Source: enhance.tex 8510–8640 (the App C flow lemma l.flow.averages with the time variable
fixed). We write FᵗF = 1 + ∑_{k∈S} g_k ∘ X_k⁻¹ with g_k = ξ_k(Gᵀ+G) + ξ_k² GᵀG
(G = ∇Χ_{m,k}), so that
∫|F∇T|² - ∫∇T·⟨FᵗF⟩∇T = ∑_k ∑_{ij} [⟨f_ij · (g_k)_ij ∘ X_k⁻¹⟩ - ⟨f_ij⟩⟨(g_k)_ij⟩]
with f_ij = ∂_iT ∂_jT, and each bracket is bounded by the flow lemma.
Entries of ∇Χ_{m,k}: sup bound and fast periodicity #
theorem
AVenhance.Infra.Section5.LeftToShow.SpaceErgodic.epsilon_pos'
{β : ℝ}
(I : Ingredients β)
(m : ℕ)
:
theorem
AVenhance.Infra.Section5.LeftToShow.SpaceErgodic.a_nonneg'
{β : ℝ}
(I : Ingredients β)
(m : ℕ)
:
theorem
AVenhance.Infra.Section5.LeftToShow.SpaceErgodic.amplitude_abs_le
{β : ℝ}
(I : Ingredients β)
{m : ℕ}
(hm : 1 ≤ m)
{κ : ℝ}
(hκ : 0 < κ)
(k : ℤ)
(t : ℝ)
:
The amplitude 4π² a_m c_{m,k}(t) of an entry of ∇Χ_{m,k} is at most a_m ε_m²/κ.
theorem
AVenhance.Infra.Section5.LeftToShow.gradMatrix_chiMK_entry_form_bdd
{β : ℝ}
(I : Ingredients β)
{m : ℕ}
(hm : 1 ≤ m)
{κ : ℝ}
(hκ : 0 < κ)
(k : ℤ)
(t : ℝ)
(i j : Fin 2)
:
Every entry of ∇Χ_{m,k} is c sin(2π y_r/ε_m) with |c| ≤ a_m ε_m²/κ.
theorem
AVenhance.Infra.Section5.LeftToShow.gradMatrix_chiMK_entry_abs_le
{β : ℝ}
(I : Ingredients β)
{m : ℕ}
(hm : 1 ≤ m)
{κ : ℝ}
(hκ : 0 < κ)
(k : ℤ)
(t : ℝ)
(y : Homogenization.Vec 2)
(i j : Fin 2)
:
|∂iχ{m,k,j}| ≤ a_m ε_m² / κ (e.corrm, gradient part).
theorem
AVenhance.Infra.Section5.LeftToShow.gradMatrix_chiMK_shift
{β : ℝ}
(I : Ingredients β)
{m : ℕ}
(_hm : 1 ≤ m)
(κ : ℝ)
(k : ℤ)
(t : ℝ)
(y : Homogenization.Vec 2)
(n : Fin 2 → ℤ)
:
gradMatrix (I.chiMK κ m k t) (y + fun (i : Fin 2) => ↑(n i) / ↑(ergodicFrequency β I.Λ m)) = gradMatrix (I.chiMK κ m k t) y
The matrix-valued corrector gradient is invariant under ε_m-lattice shifts.
theorem
AVenhance.Infra.Section5.LeftToShow.gradMatrix_chiMK_isFastPeriodic
{β : ℝ}
(I : Ingredients β)
{m : ℕ}
(hm : 1 ≤ m)
(κ : ℝ)
(k : ℤ)
(t : ℝ)
(i j : Fin 2)
:
Ergodic.IsFastPeriodic (ergodicFrequency β I.Λ m) fun (y : Homogenization.Vec 2) => gradMatrix (I.chiMK κ m k t) y i j
The corrector gradients are ε_m-periodic: fast periodic at frequency ε_m⁻¹.
The Gram kernel g_k #
theorem
AVenhance.Infra.Section5.LeftToShow.continuous_gramKernel_grad
{β : ℝ}
(I : Ingredients β)
(κm : ℝ)
{m : ℕ}
(t : ℝ)
{k : ℤ}
(hk : Odd k)
(ξ : ℝ)
:
Continuous fun (y : Homogenization.Vec 2) => gramKernel ξ (gradMatrix (I.chiMK κm m k t) y)
theorem
AVenhance.Infra.Section5.LeftToShow.cellAverage_le_of_forall_le
{g : Homogenization.Vec 2 → ℝ}
{c : ℝ}
(h : ∀ (x : Homogenization.Vec 2), g x ≤ c)
(hg : Continuous g)
:
A pointwise bound by c gives the same bound for the cell average.
Abstract averaging algebra #
theorem
AVenhance.Infra.Section5.LeftToShow.spaceAvg_mul_sub_decomp
{ι : Type u_1}
(S : Finset ι)
{f h : Homogenization.Vec 2 → ℝ}
{g : ι → Homogenization.Vec 2 → ℝ}
{Y : ι → Homogenization.Vec 2 → Homogenization.Vec 2}
{δ : ℝ}
(hf : Continuous f)
(hg : ∀ (k : ι), Continuous (g k))
(hY : ∀ (k : ι), Continuous (Y k))
(hh : ∀ (x : Homogenization.Vec 2), h x = δ + ∑ k ∈ S, g k (Y k x))
(havg : ∀ k ∈ S, (spaceAvg fun (x : Homogenization.Vec 2) => g k (Y k x)) = spaceAvg (g k))
:
The splitting of a product average: if h = δ + ∑_k g_k ∘ Y_k with ⟨g_k ∘ Y_k⟩ = ⟨g_k⟩,
then ⟨f h⟩ - ⟨h⟩⟨f⟩ = ∑_k (⟨f · g_k ∘ Y_k⟩ - ⟨f⟩⟨g_k⟩).
theorem
AVenhance.Infra.Section5.LeftToShow.vecDot_mulVec_eq_sum
(u : Homogenization.Vec 2)
(A : Matrix (Fin 2) (Fin 2) ℝ)
:
theorem
AVenhance.Infra.Section5.LeftToShow.integral_quad_eq_sum
{u : Homogenization.Vec 2 → Homogenization.Vec 2}
{H : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ}
(hu : ∀ (i : Fin 2), Continuous fun (x : Homogenization.Vec 2) => u x i)
(hH : ∀ (i j : Fin 2), Continuous fun (x : Homogenization.Vec 2) => H x i j)
:
∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (u x) ((H x).mulVec (u x)) = ∑ i : Fin 2, ∑ j : Fin 2, spaceAvg fun (x : Homogenization.Vec 2) => u x i * u x j * H x i j
∫ u·(H u) as a sum of averages of u_i u_j H_ij.
theorem
AVenhance.Infra.Section5.LeftToShow.integral_quad_spaceAvgMat
{u : Homogenization.Vec 2 → Homogenization.Vec 2}
{H : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ}
(hu : ∀ (i : Fin 2), Continuous fun (x : Homogenization.Vec 2) => u x i)
:
∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (u x) ((spaceAvgMat H).mulVec (u x)) = ∑ i : Fin 2,
∑ j : Fin 2,
(spaceAvg fun (x : Homogenization.Vec 2) => u x i * u x j) * spaceAvg fun (x : Homogenization.Vec 2) => H x i j
The quadratic form of a spatially averaged matrix field.
The gradient of the slice T(t) #
theorem
AVenhance.Infra.Section5.LeftToShow.contDiff_spaceGrad_coord
{f : Homogenization.Vec 2 → ℝ}
(hf : ContDiff ℝ (↑⊤) f)
(i : Fin 2)
:
ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => spaceGrad f x i
theorem
AVenhance.Infra.Section5.LeftToShow.isZPeriodic_spaceGrad_coord
{f : Homogenization.Vec 2 → ℝ}
(hf : IsZ2Periodic f)
(i : Fin 2)
:
Ergodic.IsZPeriodic fun (x : Homogenization.Vec 2) => spaceGrad f x i
One flow-lemma term #
theorem
AVenhance.Infra.Section5.LeftToShow.space_kill_term_bound
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 1 ≤ m)
{κm : ℝ}
(hκm : 0 < κm)
{T : ℝ → Homogenization.Vec 2 → ℝ}
{t : ℝ}
(hTs : ContDiff ℝ (↑⊤) (T t))
(hTp : IsZ2Periodic (T t))
{Cf r : ℝ}
(hCf : 0 ≤ Cf)
(hr : 0 < r)
(hAn :
∀ (k : ℤ),
Odd k →
I.xiMK m k t ≠ 0 →
∀ (i j : Fin 2),
Ergodic.HasCoordinateAnalyticL1Bounds
(fun (y : Homogenization.Vec 2) =>
↑(spaceGrad (T t) (I.xFlow hΦ m (lIdx β I.Λ m k) t y) i * spaceGrad (T t) (I.xFlow hΦ m (lIdx β I.Λ m k) t y) j))
Cf r)
(hrN : 1 ≤ r * ↑(ergodicFrequency β I.Λ m))
(k : { k : ℤ // Odd k })
(i j : Fin 2)
:
|(spaceAvg fun (x : Homogenization.Vec 2) =>
spaceGrad (T t) x i * spaceGrad (T t) x j * gramKernel (I.xiMK m (↑k) t) (gradMatrix (I.chiMK κm m (↑k) t) (I.xFlowInv hΦ m (lIdx β I.Λ m ↑k) t x)) i j) - (spaceAvg fun (x : Homogenization.Vec 2) => spaceGrad (T t) x i * spaceGrad (T t) x j) * spaceAvg fun (y : Homogenization.Vec 2) =>
gramKernel (I.xiMK m (↑k) t) (gradMatrix (I.chiMK κm m (↑k) t) y) i j| ≤ I.xiMK m (↑k) t * ((512 * Cf * (2 * (a β I.Λ m * epsilon β I.Λ m ^ 2 / κm) + 2 * (a β I.Λ m * epsilon β I.Λ m ^ 2 / κm) ^ 2) * ∑' (k : Fin 2 → ℤ), Real.exp (-(1 / 1024) * ‖k‖)) * Real.exp (-(r * ↑(ergodicFrequency β I.Λ m)) / 1024))
The L¹ flow lemma applied to one (k, i, j).
e.ergodic.space.kill at a fixed time #
theorem
AVenhance.Infra.Section5.LeftToShow.ergodic_space_kill_slice
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 1 ≤ m)
{κm : ℝ}
(hκm : 0 < κm)
{T : ℝ → Homogenization.Vec 2 → ℝ}
{t : ℝ}
(hTs : ContDiff ℝ (↑⊤) (T t))
(hTp : IsZ2Periodic (T t))
{Cf r : ℝ}
(hCf : 0 ≤ Cf)
(hr : 0 < r)
(hAn :
∀ (k : ℤ),
Odd k →
I.xiMK m k t ≠ 0 →
∀ (i j : Fin 2),
Ergodic.HasCoordinateAnalyticL1Bounds
(fun (y : Homogenization.Vec 2) =>
↑(spaceGrad (T t) (I.xFlow hΦ m (lIdx β I.Λ m k) t y) i * spaceGrad (T t) (I.xFlow hΦ m (lIdx β I.Λ m k) t y) j))
Cf r)
(hrN : 1 ≤ r * ↑(ergodicFrequency β I.Λ m))
:
|(∫ (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| ≤ (4 * 512 * Cf * (2 * (a β I.Λ m * epsilon β I.Λ m ^ 2 / κm) + 2 * (a β I.Λ m * epsilon β I.Λ m ^ 2 / κm) ^ 2) * ∑' (k : Fin 2 → ℤ), Real.exp (-(1 / 1024) * ‖k‖)) * Real.exp (-(r * ↑(ergodicFrequency β I.Λ m)) / 1024)
e.ergodic.space.kill at a fixed time t (8604–8630, before integrating in t).