Conditional hypotheses for the limit-field argument in §2.

StreamRegularityBounds is exactly the three estimates in the first part of the stream-regularity estimates: the increment estimate at every order, the estimate on Φ m for n ≥ 2, and the low-order estimate on Φ m for n ≤ 1. It is data, not an import of the draft theorem. StreamVelocityTimeIncrementBound isolates the one additional quantitative input used below for temporal Hölder continuity; it is the mean-value consequence of the estimate obtained by differentiating the recursion in (e.psi.recursion.partial.t).

def AVenhance.StreamRegularityBounds {β : ℝ} (C : ℝ) (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) : Prop

The explicit estimates supplied by the stream-regularity estimates (part (i)), with the same constant C in its low-order estimate. The order ranges match the corrected statement.

Equations

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

theorem AVenhance.LimitFieldBounds.epsilon_pos_for_ingredients {β : ℝ} (I : Ingredients β) (m : ℕ) : 0 < epsilon β I.Λ m

theorem AVenhance.LimitFieldBounds.continuous_norm_le_of_ae_le {f : Homogenization.Vec 2 → ℝ} {B : ℝ} (hf : Continuous f) (hB : 0 ≤ B) (h : ∀ᵐ (x : Homogenization.Vec 2), ‖f x‖ₑ ≤ ENNReal.ofReal B) (x : Homogenization.Vec 2) : ‖f x‖ ≤ B

theorem AVenhance.LimitFieldBounds.barNorm_zero_eq_eLpNorm (R : ℝ) (f : Homogenization.Vec 2 → ℝ) : barNorm 0 R f = MeasureTheory.eLpNorm f ⊤ MeasureTheory.volume

theorem AVenhance.barNorm_zero_pointwise {R B : ℝ} {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) (hB : 0 ≤ B) (h : barNorm 0 R f ≤ ENNReal.ofReal B) (x : Homogenization.Vec 2) : ‖f x‖ ≤ B

The zero-order stream-regularity seminorm controls the pointwise size of a continuous function, since Lebesgue measure has positive measure on every nonempty open set.

theorem AVenhance.LimitFieldBounds.barNorm_iterated_pointwise {n : ℕ} {R B : ℝ} {f : Homogenization.Vec 2 → ℝ} (i : Fin n → Fin 2) (hf : Continuous fun (x : Homogenization.Vec 2) => (iteratedFDeriv ℝ n f x) fun (j : Fin n) => Homogenization.basisVec (i j)) (hR : 0 < R) (hB : 0 ≤ B) (h : barNorm n R f ≤ ENNReal.ofReal B) (x : Homogenization.Vec 2) : ‖(iteratedFDeriv ℝ n f x) fun (j : Fin n) => Homogenization.basisVec (i j)‖ ≤ B / ((↑n + 1) ^ 2 / ↑n.factorial * R⁻¹ ^ n)

theorem AVenhance.LimitFieldBounds.continuous_iteratedCoordinate {n : ℕ} {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (i : Fin n → Fin 2) : Continuous fun (x : Homogenization.Vec 2) => (iteratedFDeriv ℝ n f x) fun (j : Fin n) => Homogenization.basisVec (i j)

theorem AVenhance.streamSeq_isAdmissible {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (m : ℕ) : IsAdmissibleStream (Φ m)

Every member of an IsStreamSeq is admissible. The positive indices follow from the defining previous-index witness; index zero is the zero stream.

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

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

Pointwise order-zero increment estimate extracted from the stream-regularity seminorm. This is the summable bound used for convergence of Φ m.

theorem AVenhance.streamIncrement_deriv_coordinate_le {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) (x : Homogenization.Vec 2) (i : Fin 2) : ‖(fderiv ℝ (Φ m t - Φ (m - 1) t) x) (Homogenization.basisVec i)‖ ≤ 320 * epsilon β I.Λ m ^ (β - 1)

First spatial derivatives of a stream increment have the scale used in e.C1beta.phi.m.m-1.

theorem AVenhance.streamIncrement_secondCoordinate_le {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) (x : Homogenization.Vec 2) (i : Fin 2 → Fin 2) : ‖(iteratedFDeriv ℝ 2 (Φ m t - Φ (m - 1) t) x) fun (j : Fin 2) => Homogenization.basisVec (i j)‖ ≤ 2 ^ 16 * epsilon β I.Λ m ^ (β - 2)

Second spatial derivatives of a stream increment are bounded at scale ε_m^(β-2). The displayed constant is deliberately rounded up.

def AVenhance.StreamVelocityTimeIncrementBound {β : ℝ} (A : ℝ) (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) : Prop

Minimal temporal input for the limit Holder estimate. The source obtains this from the differentiated recursion and the bound on ∂ₜ(b_m-b_{m-1}); the formulation below is precisely its mean-value consequence.

Equations

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