The time bound for twistie1 in terms of the space-time gradients of T #
se_time_bound: for t ∈ (0,1) the slice estimate se_slice_hMinus and the weighted pointwise
bound se_gradDiv_vecNormSq_le (the G(t) = ‖∇ ∇·(B ∇T)(t)‖² term), integrated in time by
se_time_assembly, give the bound by the space-time energies of the gradients of the words of
length ≤ 2 applied to T.
theorem
AVenhance.Infra.Section5.Contracts.se_gdNormSq_le
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 2 ≤ m)
(κm : ℝ)
(Tn : ℝ → Homogenization.Vec 2 → ℝ)
{t : ℝ}
(hT : ContDiff ℝ (↑⊤) (Tn t))
{D L : ℝ}
(hD : 0 ≤ D)
(hL : 0 ≤ L)
(hBb :
∀ (i j : Fin 2) (w : List (Fin 2)) (x : Homogenization.Vec 2),
|Section4.amnrSpaceWord w (fun (y : Homogenization.Vec 2) => (I.Kmat κm m t + I.sMat hΦ m κm t y) i j) x| ≤ D * ↑w.length.factorial * L ^ w.length)
:
gradNormSq (seGd I hΦ m κm Tn t) ≤ ∑ w ∈ scWords2, 14336 * D ^ 2 * (L ^ (2 - w.length)) ^ 2 * gradNormSq (scWordGrad Tn w t)
The energy of ∇ ∇·(B ∇T) at time t by the weighted word energies of T.
theorem
AVenhance.Infra.Section5.Contracts.se_time_bound
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 2 ≤ m)
{κm : ℝ}
(hκm : 0 < κm)
(Tn : ℝ → Homogenization.Vec 2 → ℝ)
(hTc : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => Tn p.1 p.2) (Set.Ici 0 ×ˢ Set.univ))
(hTs : ∀ t ∈ Set.Ioo 0 1, ContDiff ℝ (↑⊤) (Tn t))
(hTper : ∀ t ∈ Set.Ioo 0 1, IsZ2Periodic (Tn t))
(hmean : ∀ t ∈ Set.Ioo 0 1, Homogenization.MeanZeroOn unitCube (twistie1 I hΦ m κm Tn t))
(hsmall : epsilon β I.Λ (m - 1) ^ (2 * delta β) ≤ 1 / 8)
{D M L : ℝ}
(hD : 0 ≤ D)
(hM : 0 ≤ M)
(hL : 2 ^ 10 / epsilon β I.Λ (m - 1) ≤ L)
(hBb :
∀ t ∈ Set.Ioo 0 1,
∀ (i j : Fin 2) (w : List (Fin 2)) (x : Homogenization.Vec 2),
|Section4.amnrSpaceWord w (fun (y : Homogenization.Vec 2) => (I.Kmat κm m t + I.sMat hΦ m κm t y) i j) x| ≤ D * ↑w.length.factorial * L ^ w.length)
(hTb :
∀ t ∈ Set.Ioo 0 1,
∀ (w : List (Fin 2)),
0 < w.length →
MeasureTheory.eLpNorm (Section4.amnrSpaceWord w (Tn t)) 2 (MeasureTheory.volume.restrict (Torus.unitCell 2)) ≤ ENNReal.ofReal (M * ↑w.length.factorial * L ^ w.length))
(hsep : 2 ≤ (16 * L)⁻¹ / 2 ^ 11 * ↑(ergodicFrequency β I.Λ m))
:
(timeHMinusOneNorm fun (t : ℝ) => twistie1 I hΦ m κm Tn t) ≤ ENNReal.ofReal
(72 * √2 * (seCE / ↑(ergodicFrequency β I.Λ m) * 4 * (epsilon β I.Λ m * (a β I.Λ m * epsilon β I.Λ m ^ 2 / κm)) * √(∑ w ∈ scWords2, 14336 * D ^ 2 * (L ^ (2 - w.length)) ^ 2 * spaceTimeGradNormSq (scWordGrad Tn w)) + seCE * (2048 * 40 * D * M * L ^ 3) * (epsilon β I.Λ m * (a β I.Λ m * epsilon β I.Λ m ^ 2 / κm)) * Real.exp (-((16 * L)⁻¹ / 2 ^ 11) * ↑(ergodicFrequency β I.Λ m) / 4096)))
The time bound of twistie1.