Open-time HTilde_m gradient: scale engine and generic bound #
Open-time copies of hm_gradient_le_of_amnr_scales and relative_Hm_gradient whose spatial
differentiability premises are only required at positive times.
theorem
AVenhance.Infra.Section5.RelativeError.timeCube_ae_pos :
∀ᵐ (z : ℝ × Homogenization.Vec 2) ∂MeasureTheory.volume.restrict timeCube, 0 < z.1
Almost every point of the time cube has positive time.
theorem
AVenhance.Infra.Section5.RelativeError.hm_gradient_le_of_amnr_scales_Ioi
{β 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 : ℝ),
0 < 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 : ℝ),
0 < 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 : ℝ),
0 < 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).
theorem
AVenhance.Infra.Section5.RelativeError.relative_Hm_gradient_Ioi
(β C₀ CA : ℝ)
(hCA : 0 ≤ CA)
:
∃ (CH : ℝ),
0 ≤ CH ∧ ∃ (Λ₀ : ℝ),
∀ (I : Ingredients β),
I.Czeta ≤ C₀ →
I.Cxi ≤ C₀ →
I.Chat ≤ C₀ →
Λ₀ ≤ ↑I.Λ →
∀ (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ),
∀ κ ∈ permissibleSet β I.Λ,
∀ (M : ℕ),
1 ≤ M →
κ ∈ permittedInterval β I.Λ M →
∀ (m : ℕ),
2 ≤ m →
m ≤ M →
∀ (T : ℝ → Homogenization.Vec 2 → ℝ) (S : ℝ),
0 ≤ S →
(∀ 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 (I.kappaSeq κ M m) T
n r z i j k p)
(MeasureTheory.volume.restrict timeCube)) →
(∀ r ∈ Finset.range (Jcut β),
MeasureTheory.AEStronglyMeasurable
(fun (z : ℝ × Homogenization.Vec 2) =>
spaceGrad
(fun (x : Homogenization.Vec 2) =>
I.Hmr hΦ m (I.kappaSeq κ M m) T r z.1 x)
z.2)
(MeasureTheory.volume.restrict timeCube)) →
(∀ r ∈ Finset.range (Jcut β),
∀ n ∈ Finset.range (Nstar β),
∀ (i j k : Fin 2) (t : ℝ),
0 < t →
∀ (x : Homogenization.Vec 2),
DifferentiableAt ℝ
(fun (y : Homogenization.Vec 2) =>
I.Amnr hΦ m (I.kappaSeq κ M m) n T r t y i j k)
x) →
(∀ r ∈ Finset.range (Jcut β),
∀ n ∈ Finset.range (Nstar β),
∀ (i j k : Fin 2) (t : ℝ),
0 < t →
∀ (x : Homogenization.Vec 2),
DifferentiableAt ℝ
(fun (y : Homogenization.Vec 2) =>
spaceGrad
(fun (x : Homogenization.Vec 2) =>
I.Amnr hΦ m (I.kappaSeq κ M m) n T r t x i j k)
y i)
x) →
(∀ r ∈ Finset.range (Jcut β),
∀ (t : ℝ),
0 < t →
∀ (x : Homogenization.Vec 2),
DifferentiableAt ℝ
(fun (y : Homogenization.Vec 2) =>
I.Hmr hΦ m (I.kappaSeq κ M m) T r t y)
x) →
(∀ r₀ ∈ Finset.range (Jcut β),
∀ n ∈ Finset.range (Nstar β),
MeasureTheory.eLpNorm
(Section4.amnrSpatialDivergenceGradientTensor I hΦ m
(I.kappaSeq κ M m) T n r₀)
2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal
(CA * S * (epsilon β I.Λ m ^ 2 / I.kappaSeq κ M m) / √(I.kappaSeq κ M (m - 1)) * (epsilon β I.Λ (m - 1) ^ (-(1 + gamma β / 2))) ^ 2 * (tauP β I.Λ m)⁻¹ ^ r₀)) →
√(I.kappaSeq κ M m) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) =>
spaceGrad (I.Hm hΦ m (I.kappaSeq κ M m) T s) x) ≤ CH * epsilon β I.Λ (m - 1) ^ (4 * delta β) * S
Gradient bound, open-time variant: the differentiability premises are required only at
t > 0.