Quantitative regularity of the inverse flow in the §2 time window.
theorem
AVenhance.Infra.Construction.Section2FlowInverseBounds.spatialGradient_snorm_le_time_scaled
(f : Homogenization.Vec 2 → Homogenization.Vec 2)
(hf : ContDiff ℝ (↑⊤) f)
(n : ℕ)
{Rsrc Rt Rbase C τ : ℝ}
(hRsrc : 0 < Rsrc)
(hRt : 0 < Rt)
(hRbase : 0 < Rbase)
(hC : 0 ≤ C)
(hτ : 0 ≤ τ)
(hRsrcBase : Rsrc ≤ 9 / 8 * Rbase)
(hRratio : Rsrc / Rt ≤ 1 / 8)
(hnext : FaaDiBruno.snorm f (n + 1) Rsrc ≤ ENNReal.ofReal (16 * C * τ))
:
theorem
AVenhance.Infra.Construction.Section2FlowInverseBounds.inverseFlowJacobian_snorm_from_transport
{β : ℝ}
{I : Ingredients β}
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
{hseq : IsStreamSeq I Φ}
{R M : ℕ → ℝ}
(hscales : Section2Scales I R M)
(m n : ℕ)
(hm : 1 ≤ m)
(hcurrent : Section2StreamInductionHypothesis R M m)
(s t : ℝ)
(ht : |t| ≤ 2 ^ (-25) * (a β I.Λ m)⁻¹)
:
(flowJacobianBarNorm n (2 ^ 11 * (epsilon β I.Λ m)⁻¹) fun (x : Homogenization.Vec 2) =>
constructionFlowInvJacobian hseq m t s x - ContinuousLinearMap.id ℝ (Homogenization.Vec 2)) ≤ ENNReal.ofReal (2 ^ 23 * |t| * a β I.Λ m)
theorem
AVenhance.Infra.Construction.section2_flow_inverse_regbounds_from_previous
{β : ℝ}
{I : Ingredients β}
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
{hseq : IsStreamSeq I Φ}
{R M : ℕ → ℝ}
(hscales : Section2Scales I R M)
(happB2 : AppB2InverseFlowData I Φ hseq R M)
(m : ℕ)
(hm : 1 ≤ m)
(hprev : Section2StreamInductionHypothesis R M (m - 1))
(s t : ℝ)
:
|t| ≤ 2 ^ (-25) * (a β I.Λ m)⁻¹ →
∀ (n : ℕ),
(flowJacobianBarNorm n (2 ^ 11 * (epsilon β I.Λ m)⁻¹) fun (x : Homogenization.Vec 2) =>
constructionFlowInvJacobian hseq m t s x - ContinuousLinearMap.id ℝ (Homogenization.Vec 2)) ≤ ENNReal.ofReal (2 ^ 23 * |t| * AVenhance.a β I.Λ m)
The exact inverse_regbounds field consumed by §2, obtained from the
previous-scale stream induction and the corrected equal-radius transport
estimate.