Scale bookkeeping for conditional uses of the stream-function and diffusivity bounds conclusions.

The hypotheses below deliberately retain the expressions in the conclusions. In particular, a * epsilon^(2 + gamma) is not silently replaced in an input hypothesis; its equivalent power form is proved here.

theorem AVenhance.Infra.Section4.theta_continuous_norm_le_of_eLpNorm_bound {f : Homogenization.Vec 2 → ℝ} {B : ℝ} (hf : Continuous f) (hB : 0 ≤ B) (hbound : MeasureTheory.eLpNorm f ⊤ MeasureTheory.volume ≤ ENNReal.ofReal B) (x : Homogenization.Vec 2) : ‖f x‖ ≤ B

For continuous scalar functions, an L∞ bound holds at every point, since Lebesgue measure on Vec 2 is positive on nonempty open sets.

theorem AVenhance.Infra.Section4.theta_prev_stream_admissible {β : ℝ} {m : ℕ} (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ) (hm : 2 ≤ m) : IsAdmissibleStream (Φ (m - 1))

The defining recursion for an admitted stream makes the preceding stream an admissible smooth periodic potential, which is the drift used by θ.

theorem AVenhance.Infra.Section4.barNorm_coordinate_eLpNorm_le {n : ℕ} {R B : ℝ} {f : Homogenization.Vec 2 → ℝ} (hR : 0 < R) (hbar : barNorm n R f ≤ ENNReal.ofReal B) (i : Fin n → Fin 2) : MeasureTheory.eLpNorm (fun (x : Homogenization.Vec 2) => (iteratedFDeriv ℝ n f x) fun (j : Fin n) => Homogenization.basisVec (i j)) ⊤ MeasureTheory.volume ≤ ENNReal.ofReal B / (ENNReal.ofReal ((↑n + 1) ^ 2 / ↑n.factorial) * (ENNReal.ofReal R)⁻¹ ^ n)

Unpack the iSup in barNorm one ordered coordinate derivative at a time. This is the L∞ coefficient input used by the differentiated energy argument.

theorem AVenhance.Infra.Section4.theta_stream_deriv_eLpNorm_of_A3 {β : ℝ} {m : ℕ} (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hm : 2 ≤ m) (hA3 : ∀ (j : ℕ), 1 ≤ j → ∀ (t : ℝ) (n : ℕ), 2 ≤ n → barNorm n (2 ^ 8 * (epsilon β I.Λ j)⁻¹) (Φ j t) ≤ ENNReal.ofReal (2 ^ 5 * AVenhance.a β I.Λ j * epsilon β I.Λ j ^ 2 * ((↑n + 2) ^ 2 / (↑n + 1) ^ 3))) (n : ℕ) : 2 ≤ n → ∀ (t : ℝ) (i : Fin n → Fin 2), MeasureTheory.eLpNorm (fun (x : Homogenization.Vec 2) => (iteratedFDeriv ℝ n (Φ (m - 1) t) x) fun (j : Fin n) => Homogenization.basisVec (i j)) ⊤ MeasureTheory.volume ≤ ENNReal.ofReal (2 ^ 5 * AVenhance.a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ 2 * ((↑n + 2) ^ 2 / (↑n + 1) ^ 3)) / (ENNReal.ofReal ((↑n + 1) ^ 2 / ↑n.factorial) * (ENNReal.ofReal (2 ^ 8 * (epsilon β I.Λ (m - 1))⁻¹))⁻¹ ^ n)

The high-order stream derivative conclusion of the stream-function estimates, copied at scale m - 1, supplies each coordinate derivative's L∞ seminorm.

theorem AVenhance.Infra.Section4.theta_stream_deriv_eLpNorm_numeric_of_A3 {β : ℝ} {m : ℕ} (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hm : 2 ≤ m) (hA3 : ∀ (j : ℕ), 1 ≤ j → ∀ (t : ℝ) (n : ℕ), 2 ≤ n → barNorm n (2 ^ 8 * (epsilon β I.Λ j)⁻¹) (Φ j t) ≤ ENNReal.ofReal (2 ^ 5 * AVenhance.a β I.Λ j * epsilon β I.Λ j ^ 2 * ((↑n + 2) ^ 2 / (↑n + 1) ^ 3))) (n : ℕ) : 2 ≤ n → ∀ (t : ℝ) (i : Fin n → Fin 2), MeasureTheory.eLpNorm (fun (x : Homogenization.Vec 2) => (iteratedFDeriv ℝ n (Φ (m - 1) t) x) fun (j : Fin n) => Homogenization.basisVec (i j)) ⊤ MeasureTheory.volume ≤ ENNReal.ofReal (2 ^ 5 * AVenhance.a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ 2 * ((↑n + 2) ^ 2 / (↑n + 1) ^ 3) * (↑n.factorial / (↑n + 1) ^ 2) * (2 ^ 8 * (epsilon β I.Λ (m - 1))⁻¹) ^ n)

The factorial and radius weights in barNorm cancel to give a direct coordinate derivative bound. This is the coefficient form used in the differentiated energy estimate.

theorem AVenhance.Infra.Section4.ThetaScale.theta_A3_factorial_weight_le {n : ℕ} (hn : 2 ≤ n) : (↑n + 2) ^ 2 / (↑n + 1) ^ 3 * (↑n.factorial / (↑n + 1) ^ 2) ≤ ↑n.factorial

theorem AVenhance.Infra.Section4.theta_stream_deriv_eLpNorm_simple_of_A3 {β : ℝ} {m : ℕ} (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hm : 2 ≤ m) (hA3 : ∀ (j : ℕ), 1 ≤ j → ∀ (t : ℝ) (n : ℕ), 2 ≤ n → barNorm n (2 ^ 8 * (epsilon β I.Λ j)⁻¹) (Φ j t) ≤ ENNReal.ofReal (2 ^ 5 * AVenhance.a β I.Λ j * epsilon β I.Λ j ^ 2 * ((↑n + 2) ^ 2 / (↑n + 1) ^ 3))) (n : ℕ) : 2 ≤ n → ∀ (t : ℝ) (i : Fin n → Fin 2), MeasureTheory.eLpNorm (fun (x : Homogenization.Vec 2) => (iteratedFDeriv ℝ n (Φ (m - 1) t) x) fun (j : Fin n) => Homogenization.basisVec (i j)) ⊤ MeasureTheory.volume ≤ ENNReal.ofReal (2 ^ 5 * AVenhance.a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ 2 * ↑n.factorial * (2 ^ 8 * (epsilon β I.Λ (m - 1))⁻¹) ^ n)

The stream-function derivative estimate in the simple factorial-radius form used by the energy recursion.

theorem AVenhance.Infra.Section4.theta_stream_deriv_pointwise_of_A3 {β : ℝ} {m : ℕ} (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ) (hm : 2 ≤ m) (hA3 : ∀ (j : ℕ), 1 ≤ j → ∀ (t : ℝ) (n : ℕ), 2 ≤ n → barNorm n (2 ^ 8 * (epsilon β I.Λ j)⁻¹) (Φ j t) ≤ ENNReal.ofReal (2 ^ 5 * AVenhance.a β I.Λ j * epsilon β I.Λ j ^ 2 * ((↑n + 2) ^ 2 / (↑n + 1) ^ 3))) (n : ℕ) : 2 ≤ n → ∀ (t : ℝ) (i : Fin n → Fin 2) (x : Homogenization.Vec 2), ‖(iteratedFDeriv ℝ n (Φ (m - 1) t) x) fun (j : Fin n) => Homogenization.basisVec (i j)‖ ≤ 2 ^ 5 * AVenhance.a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ 2 * ↑n.factorial * (2 ^ 8 * (epsilon β I.Λ (m - 1))⁻¹) ^ n

The stream-function coordinate bound is pointwise for the smooth stream potential, not merely an essential-supremum statement.

theorem AVenhance.Infra.Section4.theta_kappa_power_identity {β : ℝ} {Λ m : ℕ} (hε : 0 < epsilon β Λ m) : a β Λ m * epsilon β Λ m ^ (2 + gamma β) = epsilon β Λ m ^ (β + gamma β)

theorem AVenhance.Infra.Section4.theta_second_stream_derivative_over_kappa {β c κ : ℝ} {m : ℕ} (I : Ingredients β) (hc : 0 < c) (hκ : c * (a β I.Λ m * epsilon β I.Λ m ^ (2 + gamma β)) ≤ κ) : epsilon β I.Λ m ^ (β - 2) / κ ≤ c⁻¹ * epsilon β I.Λ m ^ (-2 - gamma β)

The diffusivity bounds control the coefficient ratio generated by the twice differentiated stream potential. This is the epsilon^(-2-gamma) scale before the analytic radius normalization.