Jets of the coefficient and of T in the form used by the twistie1 estimate #
- regularity and periodicity of the coefficient
B_t = K_m(t) + s_{m-1}(t,·); - the jets of
B_tfrom those ofK_m - κ_{m-1} I + s_{m-1}(adding the constantκ_{m-1} I); - the positive jets of
TinL²(unitCell)from thel2NormSqbounds ofRelativeError.PositiveTemperatureJets.
theorem
AVenhance.Infra.Section5.Contracts.se_B_smooth
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 1 ≤ m)
(κ t : ℝ)
(i j : Fin 2)
:
theorem
AVenhance.Infra.Section5.Contracts.se_B_periodic
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(κ t : ℝ)
:
IsZ2Periodic fun (x : Homogenization.Vec 2) => I.Kmat κ m t + I.sMat hΦ m κ t x
theorem
AVenhance.Infra.Section5.Contracts.se_B_jets
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(κm κp t : ℝ)
{CB r L : ℝ}
(hκp : 0 ≤ κp)
(hCB : 0 ≤ CB)
(hr0 : 0 ≤ r)
(hrL : r ≤ L)
(hcoef :
∀ (x : Homogenization.Vec 2) (p : List (Fin 2)) (j k : Fin 2),
|Section4.iterateMatrixWord (fun (y : Homogenization.Vec 2) => I.Kmat κm m t - κp • 1 + I.sMat hΦ m κm t y) p x j
k| ≤ κp * CB * ↑p.length.factorial * r ^ p.length)
(i j : Fin 2)
(w : List (Fin 2))
(x : Homogenization.Vec 2)
:
The jets of B = K_m + s_{m-1} from those of K_m - κ_{m-1} I + s_{m-1}.
theorem
AVenhance.Infra.Section5.Contracts.se_hTb_of_l2
{Tt : Homogenization.Vec 2 → ℝ}
(hT : ContDiff ℝ (↑⊤) Tt)
{M L : ℝ}
(hjets :
∀ (n : ℕ) (i : Fin n → Fin 2),
0 < n →
√(l2NormSq fun (x : Homogenization.Vec 2) =>
(iteratedFDeriv ℝ n Tt x) fun (j : Fin n) => Homogenization.basisVec (i j)) ≤ M * ↑n.factorial * L ^ n)
(hM : 0 ≤ M)
(hL : 0 ≤ L)
(w : List (Fin 2))
:
0 < w.length →
MeasureTheory.eLpNorm (Section4.amnrSpaceWord w Tt) 2 (MeasureTheory.volume.restrict (Torus.unitCell 2)) ≤ ENNReal.ofReal (M * ↑w.length.factorial * L ^ w.length)
From the L² jets on the unit cube to the eLpNorm jets on the unit cell.