The first stream-regularity increment estimate from the finite-overlap stream recursion.

The only analytic input left explicit here is the source-form App. B.2 estimate for the inverse flow, applied after the induction bound at the previous scale.

structure AVenhance.Infra.Construction.Section2Scales {β : ℝ} (I : Ingredients β) (R M : ℕ → ℝ) : Prop

The Section 2 scalar recurrences e.recurrence, including their initial values.

• radius_zero : R 0 = 1
• amplitude_zero : M 0 = 1
• radius_step (m : ℕ) : R (m + 1) = 9 / 4 * R m + 2 ^ 7 * (epsilon β I.Λ (m + 1))⁻¹
• amplitude_step (m : ℕ) : M (m + 1) = M m + 2 ^ 7 * a β I.Λ (m + 1) * epsilon β I.Λ (m + 1) ^ 2 * R m ^ 2 + 2 ^ 18 * a β I.Λ (m + 1)

def AVenhance.Infra.Construction.Section2StreamInductionHypothesis {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (R M : ℕ → ℝ) (m : ℕ) : Prop

The source induction hypothesis e.indyhyp at one scale.

Equations

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

structure AVenhance.Infra.Construction.AppB2InverseFlowData {β : ℝ} (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hseq : IsStreamSeq I Φ) (R M : ℕ → ℝ) : Prop

App. B.2 in the source seminorm, specialized to the inverse flow in the stream recursion. Its input is exactly e.indyhyp; its output is the e.flowinv2 bound on the radius 9 R_{m-1}/8.

• inverse_spatial_smooth (m : ℕ) : 1 ≤ m → ∀ (s u : ℝ), ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => constructionFlowInv hseq (m - 1) (s + u) x s
• inverse_transport_estimate (m : ℕ) : 1 ≤ m → Section2StreamInductionHypothesis R M (m - 1) → ∀ (s u : ℝ), |u| ≤ 2 ^ (-6) * (M (m - 1))⁻¹ → ∀ (n : ℕ), 1 ≤ n → FaaDiBruno.snorm (fun (x : Homogenization.Vec 2) => constructionFlowInv hseq (m - 1) (s + u) x s) n (9 / 8 * R (m - 1)) ≤ ENNReal.ofReal (5 * (8 / 9) * (R (m - 1))⁻¹)

noncomputable def AVenhance.Infra.Construction.RecursionIncrement.streamRecursionCutoff {β : ℝ} (I : Ingredients β) (m : ℕ) (k : ℤ) (t : ℝ) : ℝ

Time cutoff multiplying a stream recursion increment.

Equations

• AVenhance.Infra.Construction.RecursionIncrement.streamRecursionCutoff I m k t = I.hatZetaML m (AVenhance.lIdx β I.Λ m k) t * I.zetaMK m k t

theorem AVenhance.Infra.Construction.RecursionIncrement.zetaMK_nonzero_distance {β : ℝ} {I : Ingredients β} (m : ℕ) (k : ℤ) (t : ℝ) (hne : I.zetaMK m k t ≠ 0) : |t - ↑k * tau β I.Λ m| ≤ 2 / 3 * tau β I.Λ m

theorem AVenhance.Infra.Construction.RecursionIncrement.active_recursion_index {β : ℝ} {I : Ingredients β} (m : ℕ) (k : ℤ) (r t : ℝ) (hclose : |r - t| < tau β I.Λ m / 6) (hactive : streamRecursionCutoff I m k r ≠ 0) : k ∈ Set.Icc ⌊t / tau β I.Λ m⌋ (⌊t / tau β I.Λ m⌋ + 1)

theorem AVenhance.Infra.Construction.section2_radius_nonneg {β : ℝ} {I : Ingredients β} {R M : ℕ → ℝ} (hscales : Section2Scales I R M) (m : ℕ) : 0 ≤ R m

theorem AVenhance.Infra.Construction.section2_radius_pos {β : ℝ} {I : Ingredients β} {R M : ℕ → ℝ} (hscales : Section2Scales I R M) (m : ℕ) : 0 < R m

theorem AVenhance.Infra.Construction.section2_amplitude_pos {β : ℝ} {I : Ingredients β} {R M : ℕ → ℝ} (hscales : Section2Scales I R M) (m : ℕ) : 0 < M m

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

theorem AVenhance.Infra.Construction.RecursionIncrement.composition_radius_identity {R e : ℝ} (hR : 0 < R) (he : 0 < e) : 9 / 8 * R * (1 + 2 * (5 * (8 / 9) * R⁻¹) * (2 * Real.pi / e)) = 9 / 8 * R + 20 * Real.pi / e

theorem AVenhance.Infra.Construction.section2_composed_profile_barNorm_bound {β : ℝ} {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 u : ℝ) (hu : |u| ≤ 2 ^ (-6) * (M (m - 1))⁻¹) (k : ℤ) (n : ℕ) : (barNorm n (9 / 8 * R (m - 1) + 20 * Real.pi / epsilon β I.Λ m) fun (x : Homogenization.Vec 2) => psi β I.Λ m k (constructionFlowInv hseq (m - 1) (s + u) x s)) ≤ ENNReal.ofReal (5 * a β I.Λ m * epsilon β I.Λ m ^ 2)

The App. B.2 inverse estimate and App. B.3 composition estimate bound one profile term at the radius used by the induction.

theorem AVenhance.Infra.Construction.RecursionIncrement.barNorm_mul_const_Icc_le {f : Homogenization.Vec 2 → ℝ} {n : ℕ} {R c : ℝ} (hf : ContDiff ℝ (↑n) f) (hc : c ∈ Set.Icc 0 1) : (barNorm n R fun (x : Homogenization.Vec 2) => c * f x) ≤ barNorm n R f

Multiplication by a spatially constant cutoff in [0,1] does not increase the seminorm.

theorem AVenhance.Infra.Construction.RecursionIncrement.barNorm_radius_monotone {f : Homogenization.Vec 2 → ℝ} {n : ℕ} {R S : ℝ} (hf : ContDiff ℝ (↑n) f) (hR : 0 < R) (hRS : R ≤ S) : barNorm n S f ≤ barNorm n R f

theorem AVenhance.Infra.Construction.RecursionIncrement.hatZeta_nonzero_distance {β : ℝ} {I : Ingredients β} {m : ℕ} (hm : 1 ≤ m) (l : ℤ) (t : ℝ) (hne : I.hatZetaML m l t ≠ 0) : |t - ↑l * tauPP β I.Λ m| ≤ tauPP β I.Λ m / 2

theorem AVenhance.Infra.Construction.stream_increment_bounds_at_scale {β : ℝ} {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)) (t : ℝ) (n : ℕ) : barNorm n (9 / 8 * R (m - 1) + 20 * Real.pi / epsilon β I.Λ m) (Φ m t - Φ (m - 1) t) ≤ ENNReal.ofReal (10 * a β I.Λ m * epsilon β I.Λ m ^ 2) ∧ barNorm n (2 ^ 7 * (epsilon β I.Λ m)⁻¹) (Φ m t - Φ (m - 1) t) ≤ ENNReal.ofReal (10 * epsilon β I.Λ m ^ β)

The finite-overlap nextStream recursion gives both the raw composition radius estimate needed by the induction and the first stream-regularity increment display.

theorem AVenhance.Infra.Construction.stream_increment_bound_at_scale {β : ℝ} {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)) (t : ℝ) (n : ℕ) : barNorm n (2 ^ 7 * (epsilon β I.Λ m)⁻¹) (Φ m t - Φ (m - 1) t) ≤ ENNReal.ofReal (10 * epsilon β I.Λ m ^ β)

The first stream-regularity increment display at its radius, extracted from the stronger composition-radius estimate.