Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.Root.Dirichlet.OutputFactorEccentricityBound

High-contrast homogenization: #

Provider.PolynomialHomogenization.Root.Dirichlet.OutputFactorEccentricityBound

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

(β): the output factor, and the correction to classified #

outputFactor = √(hsAffineFactor (matSqrt (symmPart abar))⁻¹ s ‖matSqrt (symmPart abar)‖)

as "none — it CANCELS". corrected that: the factor cancels on the left of the terminal bound, but it also occurs inside hRate's left-hand side, where that module carries it into its own C₀. A law-free C₀ therefore needs it bounded.

It cannot be bounded by a law-free constant times an eccentricity power alone. hsAffineFactor is homogeneous of degree s in the absolute scale of symmPart abar, while the witness eccentricity is scale invariant: at abar = t • 1 the eccentricity is 1 for every t > 0 while the factor is t ^ s. The dispatch's (β) is false as literally stated.

The correct form, proved here. The frozen inner-ellipsoid normalization ties the gauge cube side to that same absolute scale from both sides (witnessCubeScale_two_sided), and the ball sandwich's inner radius ρ is below the gauge scale. So the cube side is bounded below by 2ρ/(3√d), and dividing the energy's paired estimate

hsAffineFactor L⁻¹ s ‖L‖ * ell ^ (2 s) ≤ gaugeFrameConstant d s * ecc ^ (d + 2 s)

by that lower bound leaves a head depending on (d, s, ρ) only — which is exactly C₀ s₀ ρ Rad's permitted dependence — times ecc ^ (d + 2 s). The s-dependence of the eccentricity exponent is then trimmed away by s < 1/2 and the monotonicity of the fold factor, leaving the (d)-level exponent (d + 1) / 2 that the pEcc slot can carry.

The law-free head #

source
noncomputable def HCPolySupport.HighContrast.RowSupply.gaugeOutputLawFreeSq (d : ℕ) (s rho : ℝ) :
ℝ

The square of the output factor's law-free head: (d, s, ρ)-level, which is C₀ s₀ ρ Rad's permitted dependence.

Equations
Instances For
    source
    noncomputable def HCPolySupport.HighContrast.RowSupply.gaugeOutputLawFree (d : ℕ) (s rho : ℝ) :
    ℝ

    The output factor's law-free head.

    Equations
    Instances For
      source
      theorem HCPolySupport.HighContrast.RowSupply.gaugeOutputLawFreeSq_nonneg (d : ℕ) {s rho : ℝ} (hrho : 0 ≤ rho) :
      0 ≤ gaugeOutputLawFreeSq d s rho
      source
      theorem HCPolySupport.HighContrast.RowSupply.gaugeOutputLawFree_nonneg (d : ℕ) (s rho : ℝ) :
      0 ≤ gaugeOutputLawFree d s rho

      The bound #

      source
      theorem HCPolySupport.HighContrast.RowSupply.hsAffineFactor_le_gaugeOutputLawFreeSq_mul_eccentricityPow {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {U : Set (Vec d)} {j : ℤ} {z : Vec d} {rho Rad s : ℝ} (hs : 0 < s) (hsHalf : s < 1 / 2) (hU : U = (fun (x : Vec d) => z + matVecMul (matSqrt (symmPart abar)) x) '' openCubeSet (originCube d j)) (hUsub : U ⊆ ellipsoid abar 1) (hinner : ellipsoid abar (1 / (3 * √↑d)) ⊆ U) (hsandwich : HasBallSandwich (matImage (matSqrt (symmPart abar))⁻¹ U) rho Rad) :
      hsAffineFactor (matSqrt (symmPart abar))⁻¹ s ‖matSqrt (symmPart abar)‖ ≤ gaugeOutputLawFreeSq d s rho * witnessEccentricity (symmPart abar) ^ (↑d + 2 * s)

      (β), the corrected form. The affine distortion factor of the gauge frame change is below a (d, s, ρ)-level head times the (d + 2 s)-power of the witness eccentricity. The inner sandwich radius ρ is what pays the absolute scale that the eccentricity cannot see.

      source
      theorem HCPolySupport.HighContrast.RowSupply.outputFactor_le_gaugeOutputLawFree_mul_fold {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {U : Set (Vec d)} {j : ℤ} {z : Vec d} {rho Rad s : ℝ} (hs : 0 < s) (hsHalf : s < 1 / 2) (hU : U = (fun (x : Vec d) => z + matVecMul (matSqrt (symmPart abar)) x) '' openCubeSet (originCube d j)) (hUsub : U ⊆ ellipsoid abar 1) (hinner : ellipsoid abar (1 / (3 * √↑d)) ⊆ U) (hsandwich : HasBallSandwich (matImage (matSqrt (symmPart abar))⁻¹ U) rho Rad) :
      √(hsAffineFactor (matSqrt (symmPart abar))⁻¹ s ‖matSqrt (symmPart abar)‖) ≤ gaugeOutputLawFree d s rho * eccentricityFoldFactor abar ((↑d + 1) / 2)

      (β) in the fold slot. The output factor itself is below the law-free head times the fold factor at the (d)-level exponent (d + 1) / 2; the s-dependence of the exponent is trimmed by s < 1/2, exactly as that module trims the geometric factor's order dependence.