Joint regularity lemmas for the per-scale §2 flow displays.

theorem AVenhance.Infra.Construction.Section2FlowRegularityCore.derivativeSup_postCLM_le {n : ℕ} {F : Type u_1} {G : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (L : F →L[ℝ] G) (f : Homogenization.Vec 2 → F) (hf : ContDiff ℝ (↑n) f) (hL : ‖L‖ ≤ 1) : (FaaDiBruno.derivativeSup n fun (x : Homogenization.Vec 2) => L (f x)) ≤ FaaDiBruno.derivativeSup n f

theorem AVenhance.Infra.Construction.Section2FlowRegularityCore.snorm_postCLM_le {n : ℕ} {R : ℝ} {F : Type u_1} {G : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (L : F →L[ℝ] G) (f : Homogenization.Vec 2 → F) (hf : ContDiff ℝ (↑n) f) (hL : ‖L‖ ≤ 1) : FaaDiBruno.snorm (fun (x : Homogenization.Vec 2) => L (f x)) n R ≤ FaaDiBruno.snorm f n R

theorem AVenhance.Infra.Construction.snorm_neg_eq_vec {n : ℕ} {R : ℝ} (f : Homogenization.Vec 2 → Homogenization.Vec 2) : FaaDiBruno.snorm (fun (x : Homogenization.Vec 2) => -f x) n R = FaaDiBruno.snorm f n R

Negation preserves the coordinate derivative seminorm of a vector field.

noncomputable def AVenhance.Infra.Construction.Section2FlowRegularityCore.flowMatrixEntryCLM (i j : Fin 2) : FaaDiBruno.FlowMatrix →L[ℝ] ℝ

Extract a matrix entry as a continuous linear functional.

Equations

• AVenhance.Infra.Construction.Section2FlowRegularityCore.flowMatrixEntryCLM i j = { toFun := fun (A : AVenhance.FaaDiBruno.FlowMatrix) => A i j, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

theorem AVenhance.Infra.Construction.Section2FlowRegularityCore.flowMatrixEntryCLM_norm_le (i j : Fin 2) : ‖flowMatrixEntryCLM i j‖ ≤ 1

theorem AVenhance.Infra.Construction.Section2FlowRegularityCore.flowMatrixBarNorm_le_snorm (F : Homogenization.Vec 2 → FaaDiBruno.FlowMatrix) (n : ℕ) (R B : ℝ) (hF : ContDiff ℝ (↑n) F) (hbound : FaaDiBruno.snorm F n R ≤ ENNReal.ofReal B) : (⨆ (i : Fin 2), ⨆ (j : Fin 2), barNorm n R fun (x : Homogenization.Vec 2) => F x i j) ≤ ENNReal.ofReal B

theorem AVenhance.Infra.Construction.flowJacobianBarNorm_le_spatialGradient_snorm (f : Homogenization.Vec 2 → Homogenization.Vec 2) (n : ℕ) (R B : ℝ) (hGrad : ContDiff ℝ (↑n) (FaaDiBruno.spatialGradientMatrix f)) (hbound : FaaDiBruno.snorm (FaaDiBruno.spatialGradientMatrix f) n R ≤ ENNReal.ofReal B) : (flowJacobianBarNorm n R fun (x : Homogenization.Vec 2) => fderiv ℝ f x) ≤ ENNReal.ofReal B

Componentwise flow-Jacobian seminorms are controlled by the matrix gradient seminorm.

theorem AVenhance.Infra.Construction.Section2FlowRegularityCore.partialFDeriv_joint_contDiff {P : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (G : P × E → F) (hG : ContDiff ℝ (↑⊤) G) : ContDiff ℝ ↑⊤ fun (z : P × E) => fderiv ℝ (fun (y : E) => G (z.1, y)) z.2

theorem AVenhance.Infra.Construction.constructionFlow_joint_smooth {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (m : ℕ) : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2 × ℝ) => constructionFlow hseq m p.1 p.2.1 p.2.2

Joint all-orders smoothness of a constructed §2 flow.

theorem AVenhance.Infra.Construction.constructionFlowInv_joint_smooth {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (m : ℕ) : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2 × ℝ) => constructionFlowInv hseq m p.1 p.2.1 p.2.2

Joint all-orders smoothness of the inverse of a constructed §2 flow.

theorem AVenhance.Infra.Construction.Section2FlowRegularityCore.constructionFlowJacobian_joint_smooth {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (m : ℕ) : ContDiff ℝ ↑⊤ fun (p : (ℝ × ℝ) × Homogenization.Vec 2) => constructionFlowJacobian hseq m p.1.2 p.1.1 p.2

The forward spatial Jacobian is jointly smooth in its start time, increment, and evaluation point.

theorem AVenhance.Infra.Construction.Section2FlowRegularityCore.constructionFlowInvJacobian_joint_smooth {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (m : ℕ) : ContDiff ℝ ↑⊤ fun (p : (ℝ × ℝ) × Homogenization.Vec 2) => constructionFlowInvJacobian hseq m p.1.2 p.1.1 p.2

theorem AVenhance.Infra.Construction.constructionFlow_shift_isFlow {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (s : ℝ) : IsFlow (fun (t : ℝ) (x : Homogenization.Vec 2) => b (s + t) x) fun (t : ℝ) (x : Homogenization.Vec 2) (r : ℝ) => X (s + t) x (s + r)

Time-translate a flow and its vector field by the same base time.

theorem AVenhance.Infra.Construction.Section2FlowRegularityCore.constructionComposedFlowJacobian_joint_smooth {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} (m : ℕ) : ContDiff ℝ ↑⊤ fun (p : (ℝ × ℝ) × Homogenization.Vec 2) => constructionComposedFlowJacobian hseq m p.1.1 p.1.2 p.2

The composed Jacobian is jointly smooth in the two flow times and space.

theorem AVenhance.Infra.Construction.section2_composed_jacobian_smooth {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} (m : ℕ) (s t : ℝ) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => constructionComposedFlowJacobian hseq m s t x

Smooth spatial representative required when evaluating the composed Jacobian seminorm.

theorem AVenhance.Infra.Construction.section2_material_jacobian_time_diff {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} (m : ℕ) (s t : ℝ) (i j : Fin 2) (x : Homogenization.Vec 2) : DifferentiableAt ℝ (fun (r : ℝ) => (constructionComposedFlowJacobian hseq m s r x) (Homogenization.basisVec j) i) t

The entries in the composed Jacobian are differentiable in target time.

theorem AVenhance.Infra.Construction.section2_inverse_jacobian_time_diff {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} (m : ℕ) (t s : ℝ) (x : Homogenization.Vec 2) : DifferentiableAt ℝ (fun (r : ℝ) => constructionFlowInvJacobian hseq m r s x) t

The inverse-flow spatial Jacobian is differentiable in target time.

theorem AVenhance.Infra.Construction.Section2FlowRegularityCore.section2_flow_close_from_current_induction {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} {R M : ℕ → ℝ} (hscales : Section2Scales I R M) (m : ℕ) (hcurrent : Section2StreamInductionHypothesis R M m) (s t : ℝ) (ht : |t| ≤ 2 ^ (-25) * (a β I.Λ m)⁻¹) (x : Homogenization.Vec 2) : ‖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

The paper's first-derivative flow closeness estimate follows from the current scale's induction bound. The previous-scale adapter below obtains that bound through the already-proved Section 2 induction step.

theorem AVenhance.Infra.Construction.section2_flow_close_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 : ℝ) (ht : |t| ≤ 2 ^ (-25) * (a β I.Λ m)⁻¹) (x : Homogenization.Vec 2) : ‖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

flow_close in Section2FlowBoundsAtScale, derived from the preceding induction hypothesis and the Section 2 recursion.

theorem AVenhance.Infra.Construction.Section2FlowRegularityCore.flowMatrixCofactor_add_identity_local (A : FaaDiBruno.FlowMatrix) : (FaaDiBruno.flowMatrixCofactorTranspose fun (i j : Fin 2) => (if i = j then 1 else 0) + A i j) = fun (i j : Fin 2) => (if i = j then 1 else 0) + FaaDiBruno.flowMatrixCofactorTranspose A i j

theorem AVenhance.Infra.Construction.Section2FlowRegularityCore.section2_flow_jacobian_composed_from_current_induction {β : ℝ} {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 ^ 10 * (epsilon β I.Λ m)⁻¹) fun (x : Homogenization.Vec 2) => constructionComposedFlowJacobian hseq m s t x - ContinuousLinearMap.id ℝ (Homogenization.Vec 2)) ≤ ENNReal.ofReal 40

The composed Jacobian minus identity is the cofactor of the inverse-flow displacement gradient. The corrected equal-radius transport estimate therefore gives the consumed flow_jacobian_composed display.

theorem AVenhance.Infra.Construction.section2_flow_jacobian_composed_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 : ℕ) (hprev : Section2StreamInductionHypothesis R M (m - 1)) (s t : ℝ) (ht : |t| ≤ 2 ^ (-25) * (a β I.Λ m)⁻¹) : (flowJacobianBarNorm n (2 ^ 10 * (epsilon β I.Λ m)⁻¹) fun (x : Homogenization.Vec 2) => constructionComposedFlowJacobian hseq m s t x - ContinuousLinearMap.id ℝ (Homogenization.Vec 2)) ≤ ENNReal.ofReal 40

flow_jacobian_composed in Section2FlowBoundsAtScale, derived from the previous scale by first advancing the Section 2 stream induction.

theorem AVenhance.Infra.Construction.Section2FlowRegularityCore.section2_flow_jacobian_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)⁻¹) : flowJacobianBarNorm n (2 ^ 14 * (epsilon β I.Λ m)⁻¹) (constructionFlowJacobian hseq m t s) ≤ ENNReal.ofReal 12

theorem AVenhance.Infra.Construction.section2_flow_jacobian_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)⁻¹) : flowJacobianBarNorm n (2 ^ 14 * (epsilon β I.Λ m)⁻¹) (constructionFlowJacobian hseq m t s) ≤ ENNReal.ofReal 12

flow_jacobian in Section2FlowBoundsAtScale, derived from the previous scale by first proving its current e.indyhyp step.