The Section 2 induction bound controls all positive spatial seminorms of the stream velocity.

theorem AVenhance.Infra.Construction.AppB2FieldBounds.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

noncomputable def AVenhance.Infra.Construction.AppB2FieldBounds.scalarStreamEmbedding : ℝ →L[ℝ] Homogenization.Vec 2

Embed a scalar into the first coordinate of the stream vector.

Equations

• AVenhance.Infra.Construction.AppB2FieldBounds.scalarStreamEmbedding = ContinuousLinearMap.toSpanSingleton ℝ (Homogenization.basisVec 0)

theorem AVenhance.Infra.Construction.AppB2FieldBounds.scalarStreamEmbedding_norm_le : ‖scalarStreamEmbedding‖ ≤ 1

noncomputable def AVenhance.Infra.Construction.AppB2FieldBounds.streamGradientExtraction : FaaDiBruno.FlowMatrix →L[ℝ] Homogenization.Vec 2

Extract the rotated stream gradient from the first row of a flow matrix.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Construction.AppB2FieldBounds.streamGradientExtraction_norm_le (A : FaaDiBruno.FlowMatrix) : ‖streamGradientExtraction A‖ ≤ ‖A‖

theorem AVenhance.Infra.Construction.AppB2FieldBounds.streamGradientExtraction_opNorm_le : ‖streamGradientExtraction‖ ≤ 1

theorem AVenhance.Infra.Construction.AppB2FieldBounds.streamVel_eq_extractedGradient (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφsmooth : ContDiff ℝ (↑⊤) (Function.uncurry φ)) (t : ℝ) : streamVel φ t = fun (x : Homogenization.Vec 2) => streamGradientExtraction (FaaDiBruno.spatialGradientMatrix (fun (y : Homogenization.Vec 2) => scalarStreamEmbedding (φ t y)) x)

theorem AVenhance.Infra.Construction.streamVel_derivativeSup_le_next (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : ContDiff ℝ (↑⊤) (Function.uncurry φ)) (t : ℝ) (n : ℕ) : FaaDiBruno.derivativeSup n (streamVel φ t) ≤ FaaDiBruno.derivativeSup (n + 1) (φ t)

theorem AVenhance.Infra.Construction.streamVel_snorm_le_from_induction (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : ContDiff ℝ (↑⊤) (Function.uncurry φ)) (t : ℝ) (n : ℕ) {R M : ℝ} (hR : 0 < R) (hM : 0 < M) (hprev : FaaDiBruno.snorm (φ t) (n + 1) R ≤ ENNReal.ofReal (M * R⁻¹ ^ 2 * ((↑n + 3) ^ 2 / (↑n + 2) ^ 3))) : FaaDiBruno.snorm (streamVel φ t) n R ≤ ENNReal.ofReal (M / R)

theorem AVenhance.Infra.Construction.section2_streamVel_snorm_bound {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) {R M : ℕ → ℝ} {m n : ℕ} (hprev : Section2StreamInductionHypothesis R M m) (hn : 1 ≤ n) (hR : 0 < R m) (hM : 0 < M m) (t : ℝ) : FaaDiBruno.snorm (streamVel (Φ m) t) n (R m) ≤ ENNReal.ofReal (M m / R m)