Documentation

LeanPool.HighContrastHomogenization.Support.Probability.RegCoeffField.SliceMeasurability

Coarse-graining support: Support.Probability.RegCoeffField.SliceMeasurability #

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

Genuine LocalSigmaR-measurability of the AEE quantitative-slice event #

This file completes the honest slice-measurability route (Packet P4b). Using the rational-ball characterization of spatial a.e. ellipticity (RegCoeffField/Differentiation.lean), it proves that the carrier slice event

{a : RegCoeffField d | AEEQuantitativeEllipticSlice (cubeSet Q) k a.toFun}

is genuinely measurable for the local entry-test carrier σ-algebra LocalSigmaR (cubeSet Q) — not merely null-measurable, and with no hypothesis on any law. This is the P4 report's honest replacement for the comap slice field, which could not descend to null-measurability.

The event is written as a countable intersection, over rational balls inside the open core openCubeSet Q, of preimages of the closed elliptic matrix locus under the LocalSigmaR-measurable ball-average maps avgMat B (measurable_avgMat). The two free conjuncts of the raw IsAEEllipticFieldOn predicate (measurability of the domain and a.e.-strong measurability of the coefficient entries) hold for every carrier element, by type (aeeQuantitativeEllipticSlice_carrier_iff); the boundary of the half-open cube is Lebesgue-null, so rational balls in the open core suffice, and LocalSigmaR (openCubeSet Q) ≤ LocalSigmaR (cubeSet Q) upgrades the result to the consumer's cube.

Reference: the paper (Armstrong–Kuusi–Loher, to appear).

LocalSigmaR generators and monotonicity #

source
theorem HCPolySupport.measurable_entryTestR_localSigmaR {d : ℕ} {U : Set (Vec d)} (i j : Fin d) {φ : Vec d → ℝ} (hφ : IsProbeR φ) (hsupp : Function.support φ ⊆ U) :
Measurable (entryTestR i j φ)

A localized entry-test generator is LocalSigmaR U-measurable when its probe is supported in U.

source
theorem HCPolySupport.localSigmaR_mono {d : ℕ} {U V : Set (Vec d)} (hUV : U ⊆ V) :
LocalSigmaR U ≤ LocalSigmaR V

Monotonicity of the local entry-test σ-algebra under set inclusion.

LocalSigmaR-measurability of the ball averages #

source
theorem HCPolySupport.measurable_avgMat {d : ℕ} {U B : Set (Vec d)} (hBcpt : IsCompact B) (hBmeas : MeasurableSet B) (hBU : B ⊆ U) :
Measurable (avgMat B)

The ball average is a LocalSigmaR U-measurable function of the carrier field whenever the (compact measurable) ball lies in U. Each entry is a scalar multiple of a localized entry-test generator (avgMat_entry_eq_smul_entryTestR). This is the measurable-average half of Packet P4b's deliverable 1.

The rational-ball intersection #

source
def HCPolySupport.slicePart {d : ℕ} (U : Set (Vec d)) (lam Lam : ℝ) :
Set (RegCoeffField d)

The rational-ball intersection: over all rational balls inside U, the carrier fields whose ball average is elliptic. This is the countable LocalSigmaR U-measurable presentation of the a.e.-ellipticity event.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.measurableSet_slicePart {d : ℕ} {U : Set (Vec d)} (lam Lam : ℝ) :
    MeasurableSet (slicePart U lam Lam)

    The rational-ball intersection is LocalSigmaR U-measurable: a countable intersection of preimages of the closed elliptic locus under the measurable ball-average maps.

    source
    theorem HCPolySupport.setOf_aeRestrict_isEllipticMatrix_eq_slicePart {d : ℕ} {U : Set (Vec d)} (hUopen : IsOpen U) (lam Lam : ℝ) :
    {a : RegCoeffField d | ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict U, IsEllipticMatrix lam Lam (a.toFun x)} = slicePart U lam Lam

    The a.e.-ellipticity event on an open set equals the rational-ball intersection (the characterization of Differentiation.lean, as a set).

    The free conjuncts of the AEE slice on the carrier #

    source
    theorem HCPolySupport.aestronglyMeasurable_restrictCoeffField_carrier {d : ℕ} (U : Set (Vec d)) (hU : MeasurableSet U) (a : RegCoeffField d) (i j : Fin d) :
    MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => restrictCoeffField U a.toFun x i j) (volumeMeasureOn U)

    The restricted coefficient entry of a carrier field is a.e.-strongly measurable — free from the carrier type (entrywise Borel measurability).

    source
    theorem HCPolySupport.aeeQuantitativeEllipticSlice_carrier_iff {d : ℕ} (U : Set (Vec d)) (hU : MeasurableSet U) (k : ℕ) (a : RegCoeffField d) :
    AEEQuantitativeEllipticSlice U k a.toFun ↔ ∀ᵐ (x : Vec d) ∂volumeMeasureOn U, IsEllipticMatrix (↑k + 1)⁻¹ (↑k + 1) (a.toFun x)

    The AEE quantitative-slice predicate on a carrier field reduces to its a.e. ellipticity conjunct. The two measurability conjuncts of IsAEEllipticFieldOn are free by the carrier type.

    The main theorem #

    source
    theorem HCPolySupport.measurableSet_localSigmaR_aeeSlice {d : ℕ} (Q : TriadicCube d) (k : ℕ) :
    MeasurableSet {a : RegCoeffField d | AEEQuantitativeEllipticSlice (cubeSet Q) k a.toFun}

    Genuine LocalSigmaR (cubeSet Q)-measurability of the AEE quantitative-slice event. No law hypothesis: the event is a countable intersection of LocalSigmaR-measurable rational-ball average preimages. This is Packet P4b's deliverable 3, replacing the P4 comap slice field.