The telescoping part of the Section 2 stream induction.

def AVenhance.Infra.Construction.StreamIncrementBounds {β : ℝ} (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) : Prop

The first display of p.SAMS.regularity, isolated as an explicit conditional input to the higher-order induction.

Equations

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

theorem AVenhance.Infra.Construction.barNorm_radius_change {n : ℕ} {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑n) f) {R S : ℝ} (hR : 0 < R) (hS : 0 < S) : barNorm n S f = barNorm n R f * ENNReal.ofReal (R / S) ^ n

Changing the radius multiplies the order-n seminorm by the nth power of the radius ratio.

theorem AVenhance.Infra.Construction.Section2Induction.stream_slice_sum_increments {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (m : ℕ) (t : ℝ) : Φ m t = ∑ j ∈ Finset.range m, (Φ (j + 1) t - Φ j t)

theorem AVenhance.Infra.Construction.Section2Induction.epsilon_gap_ratio {β : ℝ} {I : Ingredients β} (m j : ℕ) (hjm : j ≤ m) : epsilon β I.Λ m / epsilon β I.Λ j ≤ (1 / 128) ^ (m - j)

theorem AVenhance.Infra.Construction.Section2Induction.nat_succ_le_two_pow (n : ℕ) : n + 1 ≤ 2 ^ n

theorem AVenhance.Infra.Construction.Section2Induction.rpow_increment_scale_identity {a b β : ℝ} (ha : 0 < a) (hb : 0 < b) (n : ℕ) : a ^ β * (b / (2 * a)) ^ n = b ^ β * 2 ^ (-↑n) * (b / a) ^ (↑n - β)

theorem AVenhance.Infra.Construction.Section2Induction.epsilon_gap_power_bound {β : ℝ} {I : Ingredients β} {m j n : ℕ} (hjm : j ≤ m) (hn : 2 ≤ n) : (epsilon β I.Λ m / epsilon β I.Λ j) ^ (↑n - β) ≤ (1 / 2) ^ (m - j)

theorem AVenhance.Infra.Construction.Section2Induction.rpow_two_neg_nat (n : ℕ) : 2 ^ (-↑n) = (1 / 2) ^ n

theorem AVenhance.Infra.Construction.Section2Induction.epsilon_step_le_of_minsep {β : ℝ} {I : Ingredients β} (k : ℕ) : epsilon β I.Λ (k + 1) ≤ epsilon β I.Λ k

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

theorem AVenhance.Infra.Construction.Section2Induction.stream_increment_bar_radius_bound {f : Homogenization.Vec 2 → ℝ} {n : ℕ} {R S K : ℝ} (hf : ContDiff ℝ (↑⊤) f) (hR : 0 < R) (hS : 0 < S) (hK : 0 ≤ K) (hbar : barNorm n R f ≤ ENNReal.ofReal K) : barNorm n S f ≤ ENNReal.ofReal (K * (R / S) ^ n)

theorem AVenhance.Infra.Construction.Section2Induction.increment_scale_ratio {β : ℝ} {I : Ingredients β} {m j : ℕ} (hC : 0 < 11 + 768 / (β - 1)) : 2 ^ 7 * (epsilon β I.Λ (j + 1))⁻¹ / ((11 + 768 / (β - 1)) * (epsilon β I.Λ m)⁻¹) = 2 ^ 7 * epsilon β I.Λ m / ((11 + 768 / (β - 1)) * epsilon β I.Λ (j + 1))

theorem AVenhance.Infra.Construction.Section2Induction.high_increment_scale_ratio {β : ℝ} {I : Ingredients β} {m j : ℕ} : 2 ^ 7 * (epsilon β I.Λ (j + 1))⁻¹ / (2 ^ 8 * (epsilon β I.Λ m)⁻¹) = epsilon β I.Λ m / (2 * epsilon β I.Λ (j + 1))

theorem AVenhance.Infra.Construction.high_order_stream_bound_of_increment_bounds {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hinc : StreamIncrementBounds I Φ) (m : ℕ) (t : ℝ) (n : ℕ) (hn : 2 ≤ n) : barNorm n (2 ^ 8 * (epsilon β I.Λ m)⁻¹) (Φ m t) ≤ ENNReal.ofReal (2 ^ 5 * a β I.Λ m * epsilon β I.Λ m ^ 2 * ((↑n + 2) ^ 2 / (↑n + 1) ^ 3))

The sum of normalized increment bounds closes the high-order e.phimbounds.subbed estimate. The only Section 2 induction input here is the first stream-regularity display.

theorem AVenhance.Infra.Construction.Section2Induction.barNorm_stream_increment_sum_bound {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hinc : StreamIncrementBounds I Φ) (m : ℕ) (t : ℝ) (n : ℕ) {S : ℝ} (hS : 0 < S) : barNorm n S (Φ m t) ≤ ENNReal.ofReal (∑ j ∈ Finset.range m, 10 * epsilon β I.Λ (j + 1) ^ β * (2 ^ 7 * (epsilon β I.Λ (j + 1))⁻¹ / S) ^ n)

theorem AVenhance.Infra.Construction.low_order_stream_bounds_of_increment_bounds {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hinc : StreamIncrementBounds I Φ) (m : ℕ) (t : ℝ) : have C := 11 + 768 / (β - 1); ∀ n ≤ 1, barNorm n (C * (epsilon β I.Λ m)⁻¹) (Φ m t) ≤ ENNReal.ofReal (C * epsilon β I.Λ m ^ n)

Zeroth and first order stream bounds obtained by summing the stream-regularity increment scales. The constant is explicit and depends only on β.

theorem AVenhance.Infra.Construction.stream_regularity_bounds_of_increment_bounds {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hinc : StreamIncrementBounds I Φ) : StreamRegularityBounds (11 + 768 / (β - 1)) I Φ

The full three-part stream-regularity spatial package follows from its first (increment) display. This is the scale induction used in the existence of the stream sequence.