Proofs of the Section 2 stream-function stream estimates.

The stream-function estimates statement is constructed from App. B.2. The Section 2 bridge derives the flow/material displays from the same recursive induction.

theorem AVenhance.Proofs.stream_regularity_of_increment_bounds (β : ℝ) (hIncrement : ∀ (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ), IsStreamSeq I Φ → Infra.Construction.StreamIncrementBounds I Φ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ), IsStreamSeq I Φ → ∀ (m : ℕ), 1 ≤ m → ∀ (t : ℝ), (∀ (n : ℕ), barNorm n (2 ^ 7 * (epsilon β I.Λ m)⁻¹) (Φ m t - Φ (m - 1) t) ≤ ENNReal.ofReal (10 * epsilon β I.Λ m ^ β)) ∧ (∀ (n : ℕ), 2 ≤ n → barNorm n (2 ^ 8 * (epsilon β I.Λ m)⁻¹) (Φ m t) ≤ ENNReal.ofReal (2 ^ 5 * AVenhance.a β I.Λ m * epsilon β I.Λ m ^ 2 * ((↑n + 2) ^ 2 / (↑n + 1) ^ 3))) ∧ ∀ n ≤ 1, barNorm n (C * (epsilon β I.Λ m)⁻¹) (Φ m t) ≤ ENNReal.ofReal (C * epsilon β I.Λ m ^ n)

Conditional form of the stream-function estimates statement from its first display. The conclusion has the quantifiers and all three estimates; the hypothesis is exactly the increment bound copied from that statement file.

theorem AVenhance.Proofs.stream_regularity_of_appB2 (β : ℝ) (hAppB2 : ∀ (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hseq : IsStreamSeq I Φ), Infra.Construction.AppB2InverseFlowData I Φ hseq (Infra.Construction.section2Radius I) (Infra.Construction.section2Amplitude I)) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ), IsStreamSeq I Φ → ∀ (m : ℕ), 1 ≤ m → ∀ (t : ℝ), (∀ (n : ℕ), barNorm n (2 ^ 7 * (epsilon β I.Λ m)⁻¹) (Φ m t - Φ (m - 1) t) ≤ ENNReal.ofReal (10 * epsilon β I.Λ m ^ β)) ∧ (∀ (n : ℕ), 2 ≤ n → barNorm n (2 ^ 8 * (epsilon β I.Λ m)⁻¹) (Φ m t) ≤ ENNReal.ofReal (2 ^ 5 * AVenhance.a β I.Λ m * epsilon β I.Λ m ^ 2 * ((↑n + 2) ^ 2 / (↑n + 1) ^ 3))) ∧ ∀ n ≤ 1, barNorm n (C * (epsilon β I.Λ m)⁻¹) (Φ m t) ≤ ENNReal.ofReal (C * epsilon β I.Λ m ^ n)

The explicit source recurrence for R_m and M_m, together with the App. B.2 inverse-flow estimate, proves the increment display and hence all three stream-function estimates spatial bounds. The only analytic input left at this boundary is AppB2InverseFlowData; it is not replaced by an assumed increment bound.

theorem AVenhance.Proofs.stream_regularity (β : ℝ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ), IsStreamSeq I Φ → ∀ (m : ℕ), 1 ≤ m → ∀ (t : ℝ), (∀ (n : ℕ), barNorm n (2 ^ 7 * (epsilon β I.Λ m)⁻¹) (Φ m t - Φ (m - 1) t) ≤ ENNReal.ofReal (10 * epsilon β I.Λ m ^ β)) ∧ (∀ (n : ℕ), 2 ≤ n → barNorm n (2 ^ 8 * (epsilon β I.Λ m)⁻¹) (Φ m t) ≤ ENNReal.ofReal (2 ^ 5 * AVenhance.a β I.Λ m * epsilon β I.Λ m ^ 2 * ((↑n + 2) ^ 2 / (↑n + 1) ^ 3))) ∧ ∀ n ≤ 1, barNorm n (C * (epsilon β I.Λ m)⁻¹) (Φ m t) ≤ ENNReal.ofReal (C * epsilon β I.Λ m ^ n)

Stream-function estimates proof. The canonical Section 2 scales and the smooth-periodic flow theorem construct the consumed App. B.2 data, which yields the exact three displays and quantifiers of the statement.

theorem AVenhance.Proofs.section2_induction_outputs_from_source_data {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} {R M : ℕ → ℝ} (hscales : Infra.Construction.Section2Scales I R M) (happB2 : Infra.Construction.AppB2InverseFlowData I Φ hseq R M) : StreamRegularityBounds (11 + 768 / (β - 1)) I Φ ∧ ∃ (Cmat : ℝ), 1 ≤ Cmat ∧ FlowBoundsData I Φ hseq Cmat

The recursive proof of the first stream-function estimates display also derives every per-scale flow/material field, then assembles the global source-form package.

theorem AVenhance.Proofs.limit_field_regular_of_section2_induction {β α : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hα : 0 < α) (hαβ : α < β - 1) : ∃ (φ : ℝ → Homogenization.Vec 2 → ℝ), (∀ (t : ℝ) (x : Homogenization.Vec 2), Filter.Tendsto (fun (M : ℕ) => Φ M t x) Filter.atTop (nhds (φ t x))) ∧ (∀ (M : ℕ) (t : ℝ) (x : Homogenization.Vec 2), |φ t x - Φ M t x| ≤ 11 * epsilon β I.Λ (M + 1) ^ β) ∧ (∀ (t : ℝ), Differentiable ℝ (φ t)) ∧ TendstoUniformlyOn (fun (M : ℕ) (p : ℝ × Homogenization.Vec 2) => streamVel (Φ M) p.1 p.2) (fun (p : ℝ × Homogenization.Vec 2) => streamVel φ p.1 p.2) Filter.atTop (Set.Icc 0 1 ×ˢ Set.univ) ∧ IsHolderClass α (streamVel φ) ∧ IsDivFree (streamVel φ)

Stream-function estimates limit-field package following the same §2 induction that proves the first stream-function estimates increment estimate and derives the per-scale flow bounds.