L² rate of the Hessian/gradient majorant hmPiolaQ

The pointwise bound of HmPiolaRateCalculus reduces the Piola source rate to the spacetime L² norm of hmPiolaQ, a combination of |∇T| and the two first-order Hessian rows of the terminal iterate. This file reproduces, for that majorant, the L² accounting that hm_Gbar_gradient_rate_onA7 performs for the entries of ∇GDot (whose private intermediate estimates are not exported), together with the active flow bounds from the stream-function estimates.

theorem AVenhance.Infra.Section5.Contracts.HmPiolaRateQ.hmPiola_sqrt_vecNormSq_le_abs_coordinates (v : Homogenization.Vec 2) : √(Homogenization.vecNormSq v) ≤ |v 0| + |v 1|

theorem AVenhance.Infra.Section5.Contracts.HmPiolaRateQ.hmPiola_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 (Section4.iterateSpatialWord w (u t))) ≤ B) : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => √(Homogenization.vecNormSq (spaceGrad (Section4.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.Section5.Contracts.hmPiola_active_flow_bounds {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) (t : ℝ) (l : ℤ) : I.hatXiML m l t ≠ 0 → (∀ (x : Homogenization.Vec 2) (i j : Fin 2), |I.flowGrad hΦ m l t x i j| ≤ 2) ∧ (∀ (x : Homogenization.Vec 2) (i j : Fin 2), |gradMatrix (fun (y : Homogenization.Vec 2) => I.xFlowInv hΦ m l t y) x i j| ≤ 2) ∧ ∀ (x : Homogenization.Vec 2) (p j q : Fin 2), |RelativeError.xFlowHess I hΦ m l t x p j q| ≤ 2 ^ 16 * (epsilon β I.Λ (m - 1))⁻¹

Active flow bounds (stream-function estimates) for every stream sequence: on the support of ξ̂_{m,l}(t), F_l and ∇Y_l are bounded by 2 and the second flow derivative by 2^16/ε_{m-1}.

theorem AVenhance.Infra.Section5.Contracts.hmPiolaQ_eLpNorm_rate_onA7 (β Ccut : ℝ) : ∃ (C₁ : ℝ) (Cgrad : ℝ), 0 ≤ Cgrad ∧ 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 → ℝ) => MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => hmPiolaQ (epsilon β I.Λ (m - 1)) (T (Nstar β)) z.1 z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (Cgrad * √(l2NormSq θ₀) * (√(I.kappaSeq κ M (m - 1)))⁻¹ * epsilon β I.Λ (m - 1) ^ (-1 - gamma β / 2))

The spacetime L² rate of the majorant hmPiolaQ: all thresholds and amplitudes are chosen before the ingredients and data.