RpowOpt

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Corridor-width optimization (rpow algebra)

This file isolates the pure real-analysis optimization that turns the two-error bound Var[F] ≤ C₀·(Θ³·(ℓ/L)^{d-2} + Θ/ℓ)·Msq² (4 ≤ ℓ ≤ L)

together with the deterministic bound Var[F] ≤ 4·Msq² into the min-form of the scalar block variance estimate e.scalar.block.variance: Var[F] ≤ C·Msq²·min{1, Θ²·L^{-(d-2)/(d-1)}}.

The optimal corridor width is ℓ₀ = (L^{d-2}/Θ²)^{1/(d-1)}, put here in the resolved normal form ℓ₀ = L^β·Θ^{-2/(d-1)} with β = (d-2)/(d-1). The two balancing identities and the bound Θ^{1+2/(d-1)} ≤ Θ² are the whole content.

The rpow algebra (exists_optimal_width) is separated from the numeric regime combination (scalar_opt) so each declaration elaborates at default heartbeats. No probability appears.

theorem HCPolySupport.exists_optimal_width {d : ℕ} (hd : 3 ≤ d) {Θ L : ℝ} (hΘ : 1 ≤ Θ) (hL : 1 ≤ L) : ∃ (ℓ₀ : ℝ), 0 < ℓ₀ ∧ ℓ₀ ≤ L ∧ Θ ^ 3 * (ℓ₀ / L) ^ (d - 2) ≤ Θ ^ 2 * L ^ (-(↑d - 2) / (↑d - 1)) ∧ Θ * ℓ₀⁻¹ ≤ Θ ^ 2 * L ^ (-(↑d - 2) / (↑d - 1))

Optimal corridor width. For Θ, L ≥ 1 there is a width ℓ₀ ∈ (0, L] whose two corridor error terms are both bounded by X := Θ²·L^{-(d-2)/(d-1)}. This packages all of the rpow balance algebra.

theorem HCPolySupport.scalar_opt {d : ℕ} (hd : 3 ≤ d) {Θ L Msq V C₀ : ℝ} (hΘ : 1 ≤ Θ) (hL : 1 ≤ L) (hC₀ : 0 ≤ C₀) (hdet : V ≤ 4 * Msq ^ 2) (htwo : ∀ (ℓ : ℝ), 4 ≤ ℓ → ℓ ≤ L → V ≤ C₀ * (Θ ^ 3 * (ℓ / L) ^ (d - 2) + Θ * ℓ⁻¹) * Msq ^ 2) : V ≤ (16 + 2 * C₀) * Msq ^ 2 * min 1 (Θ ^ 2 * L ^ (-(↑d - 2) / (↑d - 1)))

Corridor-width optimization. From the deterministic bound and the two-error bound (free ℓ ∈ [4, L]), the scalar block variance obeys the min-form with β = (d-2)/(d-1) and a Θ² upper factor.