Pointwise all-order spatial derivative bounds for the §2 flow.
theorem
AVenhance.Infra.Construction.Section2FlowHigherDerivative.continuous_orderedPartial
{n : ℕ}
{f : Homogenization.Vec 2 → Homogenization.Vec 2}
(hf : ContDiff ℝ (↑⊤) f)
(J : Fin n → Fin 2)
:
Continuous fun (x : Homogenization.Vec 2) => FaaDiBruno.orderedPartial n f x J
theorem
AVenhance.Infra.Construction.Section2FlowHigherDerivative.continuous_norm_le_of_ae_le_vecVolume
{E : Type u_1}
[NormedAddCommGroup E]
{f : Homogenization.Vec 2 → E}
{B : ℝ}
(hf : Continuous f)
(hB : 0 ≤ B)
(h : ∀ᵐ (x : Homogenization.Vec 2) ∂FaaDiBruno.vecVolume 2, ‖f x‖ₑ ≤ ENNReal.ofReal B)
(x : Homogenization.Vec 2)
:
theorem
AVenhance.Infra.Construction.Section2FlowHigherDerivative.continuousVector_norm_le_of_ae_le
{f : Homogenization.Vec 2 → Homogenization.Vec 2}
{B : ℝ}
(hf : Continuous f)
(hB : 0 ≤ B)
(h : ∀ᵐ (x : Homogenization.Vec 2) ∂FaaDiBruno.vecVolume 2, ‖f x‖ₑ ≤ ENNReal.ofReal B)
(x : Homogenization.Vec 2)
:
theorem
AVenhance.Infra.Construction.Section2FlowHigherDerivative.orderedPartial_pointwise_of_snorm
{n : ℕ}
{f : Homogenization.Vec 2 → Homogenization.Vec 2}
{R C : ℝ}
(hf : ContDiff ℝ (↑⊤) f)
(hR : 0 < R)
(hC : 0 ≤ C)
(hs : FaaDiBruno.snorm f n R ≤ ENNReal.ofReal C)
(J : Fin n → Fin 2)
(x : Homogenization.Vec 2)
:
theorem
AVenhance.Infra.Construction.Section2FlowHigherDerivative.orderedPartial_eq_iteratedFDeriv
{n : ℕ}
{f : Homogenization.Vec 2 → Homogenization.Vec 2}
(hf : ContDiff ℝ (↑⊤) f)
(x : Homogenization.Vec 2)
(J : Fin n → Fin 2)
:
FaaDiBruno.orderedPartial n f x J = (iteratedFDeriv ℝ n f x) fun (j : Fin n) => Homogenization.basisVec (J j)
theorem
AVenhance.Infra.Construction.Section2FlowHigherDerivative.section2_flow_higher_derivative_from_current_induction
{β : ℝ}
{I : Ingredients β}
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
{hseq : IsStreamSeq I Φ}
{R M : ℕ → ℝ}
(hscales : Section2Scales I R M)
(m n : ℕ)
(hm : 1 ≤ m)
(hn : 1 ≤ n)
(hcurrent : Section2StreamInductionHypothesis R M m)
(s t : ℝ)
(ht : |t| ≤ 2 ^ (-25) * (a β I.Λ m)⁻¹)
(x : Homogenization.Vec 2)
(J : Fin n → Fin 2)
(hclose :
‖constructionFlowJacobian hseq m t s x - ContinuousLinearMap.id ℝ (Homogenization.Vec 2)‖ ≤ 2 ^ 23 * |t| * a β I.Λ m ∧ 2 ^ 23 * |t| * a β I.Λ m ≤ 1 / 4)
:
‖(iteratedFDeriv ℝ n (fun (y : Homogenization.Vec 2) => constructionFlow hseq m (s + t) y s) x) fun (k : Fin n) =>
Homogenization.basisVec (J k)‖ ≤ 2 * ↑n.factorial * (2 ^ 14 * (epsilon β I.Λ m)⁻¹) ^ (n - 1)
theorem
AVenhance.Infra.Construction.section2_flow_higher_derivative_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)
(n : ℕ)
(hn : 1 ≤ n)
(hprev : Section2StreamInductionHypothesis R M (m - 1))
(s t : ℝ)
(ht : |t| ≤ 2 ^ (-25) * (a β I.Λ m)⁻¹)
(x : Homogenization.Vec 2)
(J : Fin n → Fin 2)
:
‖(iteratedFDeriv ℝ n (fun (y : Homogenization.Vec 2) => constructionFlow hseq m (s + t) y s) x) fun (k : Fin n) =>
Homogenization.basisVec (J k)‖ ≤ 2 * ↑n.factorial * (2 ^ 14 * (epsilon β I.Λ m)⁻¹) ^ (n - 1)
flow_higher_derivative in Section2FlowBoundsAtScale, derived from the
previous scale and the all-order signed-time p.ODE.flow.2 estimate.