Coarse-graining support: Support.Book.Ch05.Theorems.Section57.LocalizedUnitEllipticityMinimal

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Minimal-scale envelope for localized unit ellipticity

This file packages the deterministic stopping-scale logic for the localized unit-ellipticity supremum. The stochastic tail estimate for the stopping scale is added after this deterministic layer.

noncomputable def HCPolySupport.Book.Ch05.Section57.unitEllipticityEnvelopeThreshold (t α : ℝ) (m N : ℕ) : ℝ

The clean collapsed square envelope at scale m, based at integer scale N.

Equations

• HCPolySupport.Book.Ch05.Section57.unitEllipticityEnvelopeThreshold t α m N = (Real.rpow 3 (t * ↑m) * √((3 ^ m / 3 ^ N) ^ (-α))) ^ 2

theorem HCPolySupport.Book.Ch05.Section57.unitEllipticityEnvelopeThreshold_eq_shift {t α : ℝ} {N r : ℕ} : unitEllipticityEnvelopeThreshold t α (N + r) N = Real.rpow 3 (2 * t * ↑N + (2 * t - α) * ↑r)

theorem HCPolySupport.Book.Ch05.Section57.unitEllipticity_tail_parameter_le_threshold_div {t α scale : ℝ} {N r : ℕ} : 3 ^ (2 * t * ↑N) / scale * (3 ^ (2 * t - α)) ^ r ≤ unitEllipticityEnvelopeThreshold t α (N + r) N / scale

def HCPolySupport.Book.Ch05.Section57.unitEllipticityBadScaleEvent {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (params : QuantitativeCoarseGrainedEllipticityParams d) (t α : ℝ) (N : ℕ) : Set (RegCoeffField d)

Bad scale for the localized limiting-normalized unit ellipticity supremum: above the base scale N, the supremum exceeds the collapsed envelope.

Equations

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

theorem HCPolySupport.Book.Ch05.Section57.unitEllipticityBadScaleEvent_antitone {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (params : QuantitativeCoarseGrainedEllipticityParams d) {t α : ℝ} (hα : 0 ≤ α) {N K : ℕ} (hNK : N ≤ K) : unitEllipticityBadScaleEvent hP hStruct params t α K ⊆ unitEllipticityBadScaleEvent hP hStruct params t α N

theorem HCPolySupport.Book.Ch05.Section57.badTailEvent_unitEllipticityBadScaleEvent_subset {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (params : QuantitativeCoarseGrainedEllipticityParams d) {t α : ℝ} (hα : 0 ≤ α) {N : ℕ} : badTailEvent (unitEllipticityBadScaleEvent hP hStruct params t α) N ⊆ unitEllipticityBadScaleEvent hP hStruct params t α N

theorem HCPolySupport.Book.Ch05.Section57.unitEllipticityBadScaleEvent_subset_rows {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (params : QuantitativeCoarseGrainedEllipticityParams d) {t α : ℝ} {N : ℕ} : unitEllipticityBadScaleEvent hP hStruct params t α N ⊆ ⋃ (r : ℕ), {a : RegCoeffField d | unitEllipticityEnvelopeThreshold t α (N + r) N < localizedLimitWeightedUnitEllipticitySup hP hStruct params (N + r) a}

theorem HCPolySupport.Book.Ch05.Section57.measureReal_unitEllipticityBadScaleRow_le_weighted {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) {t α : ℝ} {N r : ℕ} : have scale := thetaAtScale hP hStruct 0 * hΓ.thetaHat; have w := ↑(3 ^ d); have A := 3 ^ (2 * t * ↑N) / scale; have ρ := 3 ^ (2 * t - α); 0 < t → α < t → 1 ≤ A → MeasureTheory.Measure.real P {a : RegCoeffField d | unitEllipticityEnvelopeThreshold t α (N + r) N < localizedLimitWeightedUnitEllipticitySup hP hStruct hΓ.params (N + r) a} ≤ w ^ N * (w ^ r * Real.exp (-(A * ρ ^ r) ^ hΓ.sigma))

theorem HCPolySupport.Book.Ch05.Section57.measureReal_unitEllipticityBadScaleEvent_le_weighted_kernel {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) {t α : ℝ} {N : ℕ} : have scale := thetaAtScale hP hStruct 0 * hΓ.thetaHat; have w := ↑(3 ^ d); have A := 3 ^ (2 * t * ↑N) / scale; have ρ := 3 ^ (2 * t - α); 0 < t → α < t → 1 ≤ A → MeasureTheory.Measure.real P (unitEllipticityBadScaleEvent hP hStruct hΓ.params t α N) ≤ w ^ N * (Real.exp (-A ^ hΓ.sigma) * weightedGeometricExpKernelConst w (ρ ^ hΓ.sigma))

theorem HCPolySupport.Book.Ch05.Section57.measureReal_badTailEvent_unitEllipticityBadScaleEvent_le_weighted_kernel {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) {t α : ℝ} {N : ℕ} : have scale := thetaAtScale hP hStruct 0 * hΓ.thetaHat; have w := ↑(3 ^ d); have A := 3 ^ (2 * t * ↑N) / scale; have ρ := 3 ^ (2 * t - α); 0 < t → 0 ≤ α → α < t → 1 ≤ A → MeasureTheory.Measure.real P (badTailEvent (unitEllipticityBadScaleEvent hP hStruct hΓ.params t α) N) ≤ w ^ N * (Real.exp (-A ^ hΓ.sigma) * weightedGeometricExpKernelConst w (ρ ^ hΓ.sigma))

theorem HCPolySupport.Book.Ch05.Section57.exists_quantitative_threshold_unitEllipticityBadTail_le_interpolated_tail {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) {t α : ℝ} : have η := finiteQuenchedTailExponent d σ t; have w := ↑(3 ^ d); have W := max 1 w; have ρunit := 3 ^ (2 * t - α); have Kunit := weightedGeometricExpKernelConst w (ρunit ^ σ); have M := max 1 (max 0 Kunit); have ρgap := 3 ^ η; have C₀ := 2 + Real.log W; 0 < t → 0 ≤ α → α < t → ∃ (R : ℕ), (∀ (q : ℕ), R ≤ q → C₀ * ↑q ≤ Real.exp (Real.log ρgap / 2 * ↑q)) ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → have scale := thetaAtScale hP hStruct 0 * hΓ.thetaHat; have Blead := smallBottomTailDenominator scale η σ; have Btail := 2 * Blead; have cgap := Blead ^ (-η) - Btail ^ (-η); have Qpref := max ⌈max 0 (Real.log M)⌉₊ (max R ⌈2 * max 0 (-Real.log cgap) / Real.log ρgap⌉₊); have Qlead := ⌈Real.log Blead / Real.log 3⌉₊; have Q := max Qpref Qlead; ∀ (q : ℕ), Q ≤ q → MeasureTheory.Measure.real P (badTailEvent (unitEllipticityBadScaleEvent hP hStruct hΓ.params t α) q) ≤ Real.exp (-(3 ^ ↑q / Btail) ^ η)

theorem HCPolySupport.Book.Ch05.Section57.localizedLimitWeightedUnitEllipticitySup_le_of_not_mem_unitEllipticityBadScaleEvent {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (params : QuantitativeCoarseGrainedEllipticityParams d) {t α : ℝ} {N m : ℕ} {a : RegCoeffField d} (hnot : a ∉ unitEllipticityBadScaleEvent hP hStruct params t α N) (hNm : N ≤ m) : localizedLimitWeightedUnitEllipticitySup hP hStruct params m a ≤ unitEllipticityEnvelopeThreshold t α m N

theorem HCPolySupport.Book.Ch05.Section57.localizedLimitWeightedUnitEllipticitySup_le_above_quenchedMinimalScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (params : QuantitativeCoarseGrainedEllipticityParams d) {N0 m : ℕ} {t α : ℝ} {a : RegCoeffField d} (hgood : hasGoodTailFrom N0 (unitEllipticityBadScaleEvent hP hStruct params t α) a) (hscale : quenchedMinimalScale N0 (unitEllipticityBadScaleEvent hP hStruct params t α) a ≤ 3 ^ m) : localizedLimitWeightedUnitEllipticitySup hP hStruct params m a ≤ (Real.rpow 3 (t * ↑m) * √((3 ^ m / quenchedMinimalScale N0 (unitEllipticityBadScaleEvent hP hStruct params t α) a) ^ (-α))) ^ 2

Above the constructed stopping scale, absence of unit-ellipticity bad scales gives exactly the collapsed envelope with the random scale X.

theorem HCPolySupport.Book.Ch05.Section57.exists_unitEllipticityMinimalScale_interpolated {d : ℕ} [NeZero d] {σ : ℝ} (hσ_pos : 0 < σ) {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) (hσ_eq : hΓ.sigma = σ) {t α : ℝ} : have η := finiteQuenchedTailExponent d σ t; 0 < t → 0 ≤ α → α < t → ∃ (X : RegCoeffField d → ℝ) (C : ℝ), 0 < C ∧ IndependentSums.IsBigO P (IndependentSums.gammaSigma η) X C ∧ (∀ (aω : RegCoeffField d), 1 ≤ X aω) ∧ ∀ᵐ (aω : RegCoeffField d) ∂P, ∀ {m : ℕ}, X aω ≤ 3 ^ m → localizedLimitWeightedUnitEllipticitySup hP hStruct hΓ.params m aω ≤ (Real.rpow 3 (t * ↑m) * √((3 ^ m / X aω) ^ (-α))) ^ 2