The analytic induction behind the first stream-regularity increment estimate.

noncomputable def AVenhance.Infra.Construction.Section2JointInduction.section2Weight (n : ℕ) : ℝ

Rational weight used in the joint derivative induction.

Equations

• AVenhance.Infra.Construction.Section2JointInduction.section2Weight n = (↑n + 2) ^ 2 / (↑n + 1) ^ 3

theorem AVenhance.Infra.Construction.Section2JointInduction.nat_add_three_le_three_mul_two_pow (k : ℕ) : k + 3 ≤ 3 * 2 ^ k

theorem AVenhance.Infra.Construction.Section2JointInduction.section2_weight_half_power (n : ℕ) (hn : 2 ≤ n) : (1 / 2) ^ (n - 2) ≤ 3 * section2Weight n

theorem AVenhance.Infra.Construction.Section2JointInduction.section2_stream_slice_smooth {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (m : ℕ) (t : ℝ) : ContDiff ℝ (↑⊤) (Φ m t)

theorem AVenhance.Infra.Construction.Section2JointInduction.section2_amplitude_increment_budget {β : ℝ} {I : Ingredients β} {R M : ℕ → ℝ} (hscales : Section2Scales I R M) (m : ℕ) (hm : 1 ≤ m) : 30 * a β I.Λ m * epsilon β I.Λ m ^ 2 * (9 / 8 * R (m - 1) + 20 * Real.pi / epsilon β I.Λ m) ^ 2 ≤ M m - M (m - 1)

theorem AVenhance.Infra.Construction.section2_stream_induction_step {β : ℝ} {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)) : Section2StreamInductionHypothesis R M m

One induction step for e.indyhyp. The App. B.2 inverse estimate is applied only after the previous-scale hypothesis has been established.

theorem AVenhance.Infra.Construction.section2_stream_induction {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} {R M : ℕ → ℝ} (hscales : Section2Scales I R M) (happB2 : AppB2InverseFlowData I Φ hseq R M) (m : ℕ) : Section2StreamInductionHypothesis R M m

The joint e.indyhyp induction over every Section 2 scale.

structure AVenhance.Infra.Construction.Section2FlowBoundsAtScale {β : ℝ} (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hseq : IsStreamSeq I Φ) (Cmat : ℝ) (m : ℕ) : Prop

One scale of the source-form flow data used by §2 and Appendix B. The fields retain the displayed bounds; only the scale index is fixed.

• inverse_regbounds (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)
• flow_close (s t : ℝ) : |t| ≤ 2 ^ (-25) * (a β I.Λ m)⁻¹ → ∀ (x : Homogenization.Vec 2), ‖constructionFlowJacobian hseq m t s x - ContinuousLinearMap.id ℝ (Homogenization.Vec 2)‖ ≤ 2 ^ 23 * |t| * AVenhance.a β I.Λ m ∧ 2 ^ 23 * |t| * AVenhance.a β I.Λ m ≤ 1 / 4
• flow_jacobian_composed (s t : ℝ) : |t| ≤ 2 ^ (-25) * (a β I.Λ m)⁻¹ → ∀ (n : ℕ), (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
• composed_jacobian_smooth (s t : ℝ) : |t| ≤ 2 ^ (-25) * (a β I.Λ m)⁻¹ → ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => constructionComposedFlowJacobian hseq m s t x
• flow_jacobian (s t : ℝ) : |t| ≤ 2 ^ (-25) * (a β I.Λ m)⁻¹ → ∀ (n : ℕ), 1 ≤ n → flowJacobianBarNorm n (2 ^ 14 * (epsilon β I.Λ m)⁻¹) (constructionFlowJacobian hseq m t s) ≤ ENNReal.ofReal 12
• flow_higher_derivative (s t : ℝ) : |t| ≤ 2 ^ (-25) * (a β I.Λ m)⁻¹ → ∀ (n : ℕ), 1 ≤ n → ∀ (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)
• material_jacobian (s t : ℝ) : |t| ≤ 2 ^ (-25) * (a β I.Λ m)⁻¹ → ∀ (n ell : ℕ), n + ell ≤ Nstar β → ∀ (i j : Fin 2) (x : Homogenization.Vec 2) (J : Fin n → Fin 2), ‖(iteratedFDeriv ℝ n (fun (y : Homogenization.Vec 2) => constructionMaterialIterate (fun (r : ℝ) (z : Homogenization.Vec 2) => streamVel (Φ m) (s + r) z) ell (fun (r : ℝ) (z : Homogenization.Vec 2) => (constructionComposedFlowJacobian hseq m s r z) (Homogenization.basisVec j) i) t y) x) fun (k : Fin n) => Homogenization.basisVec (J k)‖ ≤ Cmat * (epsilon β I.Λ m)⁻¹ ^ n * (epsilon β I.Λ m ^ (β - 2)) ^ ell
• material_jacobian_time_diff (s t : ℝ) : |t| ≤ 2 ^ (-25) * (a β I.Λ m)⁻¹ → ∀ (i j : Fin 2) (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (r : ℝ) => (constructionComposedFlowJacobian hseq m s r x) (Homogenization.basisVec j) i) t
• inverse_jacobian_time_diff (s t : ℝ) (x : Homogenization.Vec 2) : DifferentiableAt ℝ (fun (r : ℝ) => constructionFlowInvJacobian hseq m r s x) t

theorem AVenhance.Infra.Construction.section2_joint_induction {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} {R M : ℕ → ℝ} (hscales : Section2Scales I R M) (happB2 : AppB2InverseFlowData I Φ hseq R M) : (∀ (m : ℕ), Section2StreamInductionHypothesis R M m) ∧ StreamIncrementBounds I Φ

The §2 induction proves every e.indyhyp and the first stream-regularity increment display. Flow estimates are assembled separately from the preceding-scale induction hypothesis in Section2FlowBridge.