Pointwise construction of the limit stream from the explicit stream-regularity increment estimate, with the tail bound used in §5.4.

noncomputable def AVenhance.Infra.Construction.streamLimitTailConstant {β : ℝ} (I : Ingredients β) : ℝ

The geometric constant in the tail estimate, depending only on the exponent and scale parameter.

Equations

• AVenhance.Infra.Construction.streamLimitTailConstant I = 10 / (1 - ↑I.Λ ^ (-β))

theorem AVenhance.Infra.Construction.LimitFieldConvergence.streamLimitTailConstant_pos {β : ℝ} (I : Ingredients β) : 0 < streamLimitTailConstant I

theorem AVenhance.Infra.Construction.LimitFieldConvergence.streamLimitTailConstant_ge_one {β : ℝ} (I : Ingredients β) : 1 ≤ streamLimitTailConstant I

theorem AVenhance.Infra.Construction.LimitFieldConvergence.streamLimitTailConstant_le_eleven {β : ℝ} (I : Ingredients β) : streamLimitTailConstant I ≤ 11

theorem AVenhance.Infra.Construction.LimitFieldConvergence.streamIncrement_telescope {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (m k : ℕ) (t : ℝ) (x : Homogenization.Vec 2) : Φ (m + k) t x - Φ m t x = ∑ j ∈ Finset.range k, (Φ (m + j + 1) t x - Φ (m + j) t x)

theorem AVenhance.Infra.Construction.streamIncrement_tail_le {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (m k : ℕ) (t : ℝ) (x : Homogenization.Vec 2) : |Φ (m + k) t x - Φ m t x| ≤ streamLimitTailConstant I * epsilon β I.Λ (m + 1) ^ β

A finite tail of the sequence is bounded by the infinite geometric tail from its first omitted scale.

theorem AVenhance.Infra.Construction.streamField_cauchySeq {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (t : ℝ) (x : Homogenization.Vec 2) : CauchySeq fun (m : ℕ) => Φ m t x

The pointwise sequence of stream fields is Cauchy, uniformly in the space-time point.

theorem AVenhance.Infra.Construction.exists_streamLimit {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) : ∃ (φ : ℝ → Homogenization.Vec 2 → ℝ), ∀ (t : ℝ) (x : Homogenization.Vec 2), Filter.Tendsto (fun (M : ℕ) => Φ M t x) Filter.atTop (nhds (φ t x))

The explicit stream-regularity bounds produce a pointwise limit stream.

theorem AVenhance.Infra.Construction.streamLimit_tail_bound {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {φ : ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (hlim : ∀ (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| ≤ streamLimitTailConstant I * epsilon β I.Λ (m + 1) ^ β

The pointwise limit has the geometric tail estimate from (e.def.b).

theorem AVenhance.Infra.Construction.streamLimit_tail_bound_uniform {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {φ : ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (hlim : ∀ (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) ^ β

A uniform version of the pointwise tail estimate, with a constant that does not depend on the chosen Ingredients object.