The HTilde_m gradient from the AMNR tensor estimate, at explicit scales #
hm_gradient_le_of_amnr_scales is equation (16)-(18): per r₀ < Jcut, apply
hmr_spaceGrad_eLpNorm_le_of_pAmnr_qMNR; cancel τ'^{-r₀} against (8τ)^{r₀+1} before
summing; use 8τ/τ' ≤ 1/2; then the scale chain. The scale facts enter as real
hypotheses and are discharged in LeadingErrorH.
theorem
AVenhance.Infra.Section5.RelativeError.hm_gradient_eLpNorm_le_sum_of_hmr
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(κ : ℝ)
(T : ℝ → Homogenization.Vec 2 → ℝ)
(hD :
∀ r ∈ Finset.range (Jcut β),
∀ (t : ℝ) (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => I.Hmr hΦ m κ T r t y) x)
{B : ℕ → ℝ}
(hB : ∀ (r : ℕ), 0 ≤ B r)
(hterm :
∀ r ∈ Finset.range (Jcut β),
MeasureTheory.eLpNorm
(fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Hmr hΦ m κ T r z.1 x) z.2)
2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (B r))
:
MeasureTheory.eLpNorm
(fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Hm hΦ m κ T z.1 x) z.2) 2
(MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (∑ r ∈ Finset.range (Jcut β), B r)
The sum over r₀ < Jcut of the termwise ∇Hmr bounds, with the geometric factor kept.
theorem
AVenhance.Infra.Section5.RelativeError.hm_gradient_le_of_amnr_scales
{β C₀ CA K C ν S : ℝ}
(hCA : 0 ≤ CA)
(hS : 0 ≤ S)
(hK : 0 ≤ K)
(hC : 0 ≤ C)
(I : Ingredients β)
(hz : I.Czeta ≤ C₀)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
(hm : 2 ≤ m)
{κ : ℝ}
(T : ℝ → Homogenization.Vec 2 → ℝ)
(hκ : 0 < κ)
(hκν : κ ≤ ν)
(hratio : epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m) ≤ 1)
(hτ : 8 * tau β I.Λ m / tauP β I.Λ m ≤ 1 / 2)
(hX : a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ ≤ K * ν)
(hν : ν ≤ C * (a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ (2 + gamma β)))
(hat : a β I.Λ (m - 1) * tau β I.Λ m ≤ 2 ^ (-28) * epsilon β I.Λ (m - 1) ^ (4 * delta β))
(hHessEntryMeas :
∀ r ∈ Finset.range (Jcut β),
∀ n ∈ Finset.range (Nstar β),
∀ (i j k p : Fin 2),
MeasureTheory.AEStronglyMeasurable
(fun (z : ℝ × Homogenization.Vec 2) => Section4.amnrSpatialDivergenceGradientTensor I hΦ m κ T n r z i j k p)
(MeasureTheory.volume.restrict timeCube))
(hGradientMeas :
∀ r ∈ Finset.range (Jcut β),
MeasureTheory.AEStronglyMeasurable
(fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Hmr hΦ m κ T r z.1 x) z.2)
(MeasureTheory.volume.restrict timeCube))
(hD1 :
∀ r ∈ Finset.range (Jcut β),
∀ n ∈ Finset.range (Nstar β),
∀ (i j k : Fin 2) (t : ℝ) (x : Homogenization.Vec 2),
DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => I.Amnr hΦ m κ n T r t y i j k) x)
(hD2 :
∀ r ∈ Finset.range (Jcut β),
∀ n ∈ Finset.range (Nstar β),
∀ (i j k : Fin 2) (t : ℝ) (x : Homogenization.Vec 2),
DifferentiableAt ℝ
(fun (y : Homogenization.Vec 2) =>
spaceGrad (fun (x : Homogenization.Vec 2) => I.Amnr hΦ m κ n T r t x i j k) y i)
x)
(hHmrD :
∀ r ∈ Finset.range (Jcut β),
∀ (t : ℝ) (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => I.Hmr hΦ m κ T r t y) x)
(hAmnr :
∀ r₀ ∈ Finset.range (Jcut β),
∀ n ∈ Finset.range (Nstar β),
MeasureTheory.eLpNorm (Section4.amnrSpatialDivergenceGradientTensor I hΦ m κ T n r₀) 2
(MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal
(CA * S * (epsilon β I.Λ m ^ 2 / κ) / √ν * (epsilon β I.Λ (m - 1) ^ (-(1 + gamma β / 2))) ^ 2 * (tauP β I.Λ m)⁻¹ ^ r₀))
:
The relative-error estimates at explicit scales. The hypotheses hν, hX, hat are the scale
inputs (2), (7) of the note; hAmnr is the S-normalised tensor estimate (5).