Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch04.Internal.FixedCompetitorEnergyMeasurability.LipschitzBounds

Coarse-graining support: #

Support.Book.Ch04.Internal.FixedCompetitorEnergyMeasurability.LipschitzBounds

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

Audit tag (Ch4 rebuild contract CH04_REBUILD_SURFACE_2026-05-16.md) #

Internal claim: Borel/Lipschitz measurability of fixed-coefficient maps HilbertMat d → block-coefficient entry — the finite-dimensional nonlinear atoms behind the bounded-elliptic Nemytskii step used to lift local scalar atoms into measurable energy approximants.

Consumed by (within Internal/FixedCompetitorEnergyMeasurability/): Integrals.lean. Upstream chain continues to Theorems/Mu.lean :: aemeasurable_Mu_cubeSet.

If the single-claim summary above grows into three or more distinct claims, split or refactor per the rebuild contract.

source
theorem HCPolySupport.measurable_fullBlockCoeffEntry_hilbertMat {d : ℕ} (α β : BlockCoord d) :
Measurable fun (A : HilbertMat d) => toFullBlockMat (blockMatrixOfCoeff A.toMat) α β

A single full-block coefficient entry is a Borel function of the finite Hilbert-matrix coefficient value. This is the finite-dimensional nonlinear atom behind the later bounded elliptic Nemytskii step.

source
def HCPolySupport.quantitativeEllipticHilbertMatSet (d k : ℕ) :
Set (HilbertMat d)

The quantitative ellipticity value set for Hilbert-matrix representatives on the k-th slice. A coefficient field in QuantitativeEllipticSlice U k takes values in this set for volumeMeasureOn U-almost every point.

Equations
Instances For
    source
    noncomputable def HCPolySupport.quantitativeSymmPartInvEntryLipschitzConstant (d k : ℕ) :
    NNReal

    The nonnegative constant d²(k + 1)² controlling entries of the inverse symmetric part on the quantitative ellipticity slice.

    Equations
    Instances For
      source
      noncomputable def HCPolySupport.quantitativeInvSkewProductEntryLipschitzConstant (d k : ℕ) :
      NNReal

      The nonnegative constant d(d²(k + 1)³ + k + 1) controlling entries of the inverse-symmetric-part times skew-part product.

      Equations
      Instances For
        source
        noncomputable def HCPolySupport.quantitativeUpperLeftEntryLipschitzConstant (d k : ℕ) :
        NNReal

        The explicit nonnegative Lipschitz constant for upper-left block coefficient entries on the quantitative ellipticity slice.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem HCPolySupport.lipschitzOnWith_fullBlockCoeffEntry_hilbertMat_lowerRight_quantitative {d k : ℕ} (i j : Fin d) :
          LipschitzOnWith (quantitativeSymmPartInvEntryLipschitzConstant d k) (fun (A : HilbertMat d) => toFullBlockMat (blockMatrixOfCoeff A.toMat) (Sum.inr i) (Sum.inr j)) (quantitativeEllipticHilbertMatSet d k)
          source
          theorem HCPolySupport.lipschitzOnWith_fullBlockCoeffEntry_hilbertMat_lowerLeft_quantitative {d k : ℕ} (i j : Fin d) :
          LipschitzOnWith (quantitativeInvSkewProductEntryLipschitzConstant d k) (fun (A : HilbertMat d) => toFullBlockMat (blockMatrixOfCoeff A.toMat) (Sum.inr i) (Sum.inl j)) (quantitativeEllipticHilbertMatSet d k)
          source
          theorem HCPolySupport.lipschitzOnWith_fullBlockCoeffEntry_hilbertMat_upperRight_quantitative {d k : ℕ} (i j : Fin d) :
          LipschitzOnWith (quantitativeInvSkewProductEntryLipschitzConstant d k) (fun (A : HilbertMat d) => toFullBlockMat (blockMatrixOfCoeff A.toMat) (Sum.inl i) (Sum.inr j)) (quantitativeEllipticHilbertMatSet d k)
          source
          theorem HCPolySupport.lipschitzOnWith_fullBlockCoeffEntry_hilbertMat_upperLeft_quantitative {d k : ℕ} (i j : Fin d) :
          LipschitzOnWith (quantitativeUpperLeftEntryLipschitzConstant d k) (fun (A : HilbertMat d) => toFullBlockMat (blockMatrixOfCoeff A.toMat) (Sum.inl i) (Sum.inl j)) (quantitativeEllipticHilbertMatSet d k)
          source
          noncomputable def HCPolySupport.quantitativeFullBlockCoeffEntryLipschitzConstant (d k : ℕ) (α β : BlockCoord d) :
          NNReal

          The Lipschitz constant for a full block coefficient entry, selected according to its upper-left, off-diagonal, or lower-right block.

          Equations
          Instances For
            source
            theorem HCPolySupport.lipschitzOnWith_fullBlockCoeffEntry_hilbertMat_quantitative {d k : ℕ} (α β : BlockCoord d) :
            LipschitzOnWith (quantitativeFullBlockCoeffEntryLipschitzConstant d k α β) (fun (A : HilbertMat d) => toFullBlockMat (blockMatrixOfCoeff A.toMat) α β) (quantitativeEllipticHilbertMatSet d k)