Spacetime L² rate for the averaged pulled temperature gradient.
theorem
AVenhance.Infra.Section4.HmSourceRatesGradient.iterate_gradient_magnitude_eLpNorm_le
{u : ℝ → Homogenization.Vec 2 → ℝ}
(hu : ContDiffOn ℝ (↑⊤) (fun (z : ℝ × Homogenization.Vec 2) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ))
(w : List (Fin 2))
{B : ℝ}
(hB : 0 ≤ B)
(hBenergy : √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (u t))) ≤ B)
:
MeasureTheory.eLpNorm
(fun (z : ℝ × Homogenization.Vec 2) => √(Homogenization.vecNormSq (spaceGrad (iterateSpatialWord w (u z.1)) z.2))) 2
(MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (2 * B)
The Euclidean magnitude of a spatial gradient has the L² bound supplied
by its vector energy. The two coordinate estimates are summed without
changing the normalized space-time measure.
theorem
AVenhance.Infra.Section4.HmSourceRatesGradient.hessian_gradient_majorant_eLpNorm_le
(β D : ℝ)
:
1 ≤ D →
have F := ↑(Nstar β) * ↑(2 * Nstar β).factorial;
have Czero := 2 * (1 + F / 4);
have Cword := 2 * 4 ^ Nstar β * ↑(2 * Nstar β).factorial * (4 * D ^ 3);
∀ (I : Ingredients β) (κ : ℝ) (M : ℕ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ),
0 < epsilon β I.Λ (m - 1) →
0 < I.kappaSeq κ M (m - 1) →
have q := -1 - gamma β / 2;
have invRoot := (√(I.kappaSeq κ M (m - 1)))⁻¹;
have θsize := √(l2NormSq θ₀);
have Bzero := Czero * θsize * invRoot;
have Bword := Cword * θsize * invRoot * epsilon β I.Λ (m - 1) ^ q;
have μ := MeasureTheory.volume.restrict timeCube;
have Tn := T (Nstar β);
have r0 := fun (z : ℝ × Homogenization.Vec 2) => √(Homogenization.vecNormSq (spaceGrad (Tn z.1) z.2));
have r1 := fun (z : ℝ × Homogenization.Vec 2) =>
√(Homogenization.vecNormSq (spaceGrad (iterateSpatialWord [0] (Tn z.1)) z.2));
have r2 := fun (z : ℝ × Homogenization.Vec 2) =>
√(Homogenization.vecNormSq (spaceGrad (iterateSpatialWord [1] (Tn z.1)) z.2));
MeasureTheory.eLpNorm r0 2 μ ≤ ENNReal.ofReal (2 * Bzero) →
have Q := fun (z : ℝ × Homogenization.Vec 2) => 4 * (r1 z + r2 z) + 2 ^ 19 / epsilon β I.Λ (m - 1) * r0 z;
MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => r1 z + r2 z) 2 μ ≤ ENNReal.ofReal (2 * Bword) + ENNReal.ofReal (2 * Bword) →
(∀ (c : ℝ),
0 ≤ c →
∀ (f : ℝ × Homogenization.Vec 2 → ℝ),
MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => c * f z) 2 μ = ENNReal.ofReal c * MeasureTheory.eLpNorm f 2 μ) →
MeasureTheory.eLpNorm Q 2 μ ≤ ENNReal.ofReal (16 * Bword + 2 ^ 20 / epsilon β I.Λ (m - 1) * Bzero)
Combine the gradient and Hessian rows in the Piola majorant.
theorem
AVenhance.Infra.Section4.HmSourceRatesGradient.hessian_gradient_majorant_scale_bound
(β D : ℝ)
:
have F := ↑(Nstar β) * ↑(2 * Nstar β).factorial;
have Czero := 2 * (1 + F / 4);
have Cword := 2 * 4 ^ Nstar β * ↑(2 * Nstar β).factorial * (4 * D ^ 3);
have Cgrad := 16 * Cword + 2 ^ 20 * Czero;
∀ (I : Ingredients β) (κ : ℝ) (M : ℕ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ),
0 < I.kappaSeq κ M (m - 1) →
have q := -1 - gamma β / 2;
have invRoot := (√(I.kappaSeq κ M (m - 1)))⁻¹;
have θsize := √(l2NormSq θ₀);
have Bzero := Czero * θsize * invRoot;
have Bword := Cword * θsize * invRoot * epsilon β I.Λ (m - 1) ^ q;
(epsilon β I.Λ (m - 1))⁻¹ ≤ epsilon β I.Λ (m - 1) ^ q →
16 * Bword + 2 ^ 20 / epsilon β I.Λ (m - 1) * Bzero ≤ Cgrad * √(l2NormSq θ₀) * invRoot * epsilon β I.Λ (m - 1) ^ q
Absorb the inverse spatial scale into the fractional majorant rate.
theorem
AVenhance.Infra.Section4.hm_Gbar_gradient_rate_onA7
(β Ccut : ℝ)
:
∃ (C₁ : ℝ) (Cgrad : ℝ),
0 ≤ Cgrad ∧ Section5.Integration.OnA7Instances β Ccut C₁
fun (I : Ingredients β) (_Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (_hΦ : IsStreamSeq I _Φ) (κ : ℝ) (M : ℕ) (_R : ℝ)
(θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (_θprev : ℝ → Homogenization.Vec 2 → ℝ)
(T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) =>
∀ (i j : Fin 2),
MeasureTheory.eLpNorm
(fun (z : ℝ × Homogenization.Vec 2) => gradMatrix (Section5.Gbar I _hΦ m (T (Nstar β)) z.1) z.2 i j) 2
(MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal
(Cgrad * √(l2NormSq θ₀) * (√(I.kappaSeq κ M (m - 1)))⁻¹ * epsilon β I.Λ (m - 1) ^ (-1 - gamma β / 2))
The actual analytic T profile and the flow package derived from limit-field regularity give the
entrywise spacetime L² rate required by the H_m source reduction.
All thresholds and amplitudes are chosen before the ingredients and data.