Uniform velocity bound and Lemma-U hypotheses for the stream drifts (Lemma r.LeBron, step (b))

‖streamVel (Φ j) t x‖ ≤ B(β) uniformly in j, t, x and in the ingredients (only Λ ≥ 2^7 is used), from stream-regularity (stream_regularity) and the geometric decay of ε_j^{β-1}.

noncomputable def AVenhance.Infra.FullTheorem.velBound (β : ℝ) : ℝ

The uniform velocity bound B(β) = 320 / (1 - 128^{-(β-1)}).

Equations

• AVenhance.Infra.FullTheorem.velBound β = 320 / (1 - 128 ^ (-(β - 1)))

theorem AVenhance.Infra.FullTheorem.velBound_nonneg {β : ℝ} (hβ : 1 < β) : 0 ≤ velBound β

theorem AVenhance.Infra.FullTheorem.VelocityBounds.norm_sigma_mulVec_le (v : Homogenization.Vec 2) : ‖sigmaMat.mulVec v‖ ≤ ‖v‖

Components of σ v are ∓ components of v.

theorem AVenhance.Infra.FullTheorem.VelocityBounds.streamSlice_contDiff {Ψ : ℝ → Homogenization.Vec 2 → ℝ} (hΨ : IsAdmissibleStream Ψ) (t : ℝ) : ContDiff ℝ (↑⊤) (Ψ t)

theorem AVenhance.Infra.FullTheorem.VelocityBounds.spaceGrad_increment_le {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) (x : Homogenization.Vec 2) : ‖spaceGrad (Φ m t) x - spaceGrad (Φ (m - 1) t) x‖ ≤ 320 * epsilon β I.Λ m ^ (β - 1)

Increment of the gradient of consecutive streams.

theorem AVenhance.Infra.FullTheorem.VelocityBounds.spaceGrad_partial_le {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (t : ℝ) (x : Homogenization.Vec 2) (j : ℕ) : ‖spaceGrad (Φ j t) x‖ ≤ 320 * ∑ k ∈ Finset.range j, epsilon β I.Λ (1 + k) ^ (β - 1)

Partial sums of the gradient.

theorem AVenhance.Infra.FullTheorem.streamVel_norm_le {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (j : ℕ) (t : ℝ) (x : Homogenization.Vec 2) : ‖streamVel (Φ j) t x‖ ≤ velBound β

Uniform bound on the stream velocities.

theorem AVenhance.Infra.FullTheorem.streamVel_isZ2Periodic {Ψ : ℝ → Homogenization.Vec 2 → ℝ} (hΨ : IsAdmissibleStream Ψ) (t : ℝ) : IsZ2Periodic (streamVel Ψ t)

Spatial periodicity of the finite stream velocities.