Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.Root.Dirichlet.EccentricityFoldFactor

High-contrast homogenization: #

Provider.PolynomialHomogenization.Root.Dirichlet.EccentricityFoldFactor

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Folding the homogenized eccentricity into the homogenization length #

The reference text's homogenization length carries the aspect ratio of the homogenized matrix: the estimate with a law-free amplitude is read above a length that has been enlarged by the corresponding root. Replacing the homogenization length X by X * G, the polynomial length Lpoly by Lpoly * G and the length constant by a correspondingly larger one, for a common positive factor G determined by the homogenized matrix, leaves every clause of the statement valid: the exceedance event is literally unchanged because the common factor cancels on both sides of its threshold, the length bound survives because the factor is itself polynomial in the reference datum, and each remaining clause is weakened, its premise being harder to satisfy and its right-hand side larger.

This file proves those clause transfers, and the bound on the fold factor built from the eccentricity of the homogenized matrix.

The fold factor #

source
theorem HCPolySupport.HighContrast.RowSupply.witnessEccentricity_nonneg {d : ℕ} (m : Mat d) :
0 ≤ witnessEccentricity m

The witness eccentricity is a square root, hence nonnegative.

source
noncomputable def HCPolySupport.HighContrast.RowSupply.eccentricityFoldFactor {d : ℕ} (abar : Mat d) (p : ℝ) :
ℝ

The fold factor attached to a homogenized matrix: a power of its witness eccentricity, read at least one.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.RowSupply.one_le_eccentricityFoldFactor {d : ℕ} (abar : Mat d) (p : ℝ) :
    1 ≤ eccentricityFoldFactor abar p
    source
    theorem HCPolySupport.HighContrast.RowSupply.eccentricityFoldFactor_pos {d : ℕ} (abar : Mat d) (p : ℝ) :
    0 < eccentricityFoldFactor abar p
    source
    theorem HCPolySupport.HighContrast.RowSupply.rpow_le_eccentricityFoldFactor {d : ℕ} (abar : Mat d) (p : ℝ) :
    witnessEccentricity (symmPart abar) ^ p ≤ eccentricityFoldFactor abar p
    source
    theorem HCPolySupport.HighContrast.RowSupply.eccentricityFoldFactor_le_rpow {d : ℕ} {abar : Mat d} {base p : ℝ} (hbase : 1 ≤ base) (hp : 0 ≤ p) (hecc : witnessEccentricity (symmPart abar) ≤ base ^ 5) :
    eccentricityFoldFactor abar p ≤ base ^ (5 * p)

    The fold factor is polynomial in the reference datum. With the law-level eccentricity bound, the fold factor is below the printed polynomial length base raised to a law-free exponent.

    The polynomial length clause #

    source
    theorem HCPolySupport.HighContrast.RowSupply.mul_le_rpow_add {base Lpoly G C C' : ℝ} (hbase : 1 ≤ base) (hG : 0 ≤ G) (hLbound : Lpoly ≤ base ^ C) (hGbound : G ≤ base ^ C') :
    Lpoly * G ≤ base ^ (C + C')

    The polynomial length bound survives the fold: the product of a length below base ^ C and a factor below base ^ C' is below base ^ (C + C').

    The exceedance event #

    source
    theorem HCPolySupport.HighContrast.RowSupply.measureReal_foldedThreshold_le {Omega : Type u_1} [MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure P] {X : Omega → ℝ} {c c' L t G : ℝ} (hL : 0 ≤ L) (ht : 0 ≤ t) (hG : 0 < G) (hcc : c ≤ c') :
    P.real {a : Omega | c' * (L * G) * t ≤ X a * G} ≤ P.real {a : Omega | c * L * t ≤ X a}

    The exceedance event is unchanged by the fold. Multiplying both the polynomial length and the homogenization length by the same positive factor leaves the threshold event fixed, so the two-part tail bound transfers after the length constant is enlarged.

    The remaining clauses #

    source
    theorem HCPolySupport.HighContrast.RowSupply.corrector_factor_mono {r x x' kappa : ℝ} (hx : 0 < x) (hxx : x ≤ x') (hr : 0 < r) (hkappa : 0 < kappa) :
    (r / x) ^ (-kappa) ≤ (r / x') ^ (-kappa)

    The corrector decay factor is larger at the folded length. Its base is a ratio with the homogenization length in the denominator and a negative exponent, so enlarging the length enlarges the factor.

    source
    theorem HCPolySupport.HighContrast.RowSupply.Icc_foldedScale_subset {x x' R : ℝ} (hxx : x ≤ x') :
    Set.Icc x' R ⊆ Set.Icc x R

    The regularity radius window shrinks under the fold. The frozen Lipschitz and C¹ clauses quantify over radii above the homogenization length, so the folded window is contained in the unfolded one.

    The folded length itself #