Coarse-graining support: Support.Book.Ch04.RestrictionLaw

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

Chapter 4 restriction-engineering law assumptions (carrier re-type, Packet P3)

This file owns the separate pointwise-restriction/sup-metric engineering assumptions used by the restriction lane of Chapter 4 and later chapters. Following the carrier redesign, the single restriction-lane law carrier RestrictionCoeffLaw d is a measure on the honest-fields carrier RegCoeffField d (see HCPolySupport.Probability.RegCoeffField), on which entrywise regularity is free by type. The structural predicates re-base onto the carrier endomorphisms of RegCoeffField/Laws.lean; the ellipticity/slice predicates apply the raw IsAEEllipticFieldOn/AEEQuantitativeEllipticSlice vocabulary to the honest sample a.toFun (least-churn encoding: the a.e.-strong-measurability conjunct is kept in the predicate but is always satisfiable on a carrier element, and the downstream L² slice machinery still consumes it).

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

theorem HCPolySupport.Book.Ch04.ae_forall_mem_finset {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] {P : MeasureTheory.Measure α} (s : Finset ι) {p : ι → α → Prop} (h : ∀ i ∈ s, ∀ᵐ (a : α) ∂P, p i a) : ∀ᵐ (a : α) ∂P, ∀ i ∈ s, p i a

Combine finitely many almost-everywhere statements into one statement over all members of a finset.

theorem HCPolySupport.Book.Ch04.ae_forall_mem_finset_nested {α : Type u_1} {ι : Type u_2} {κ : Type u_3} [MeasurableSpace α] {P : MeasureTheory.Measure α} (s : Finset ι) (t : ι → Finset κ) {p : ι → κ → α → Prop} (h : ∀ i ∈ s, ∀ j ∈ t i, ∀ᵐ (a : α) ∂P, p i j a) : ∀ᵐ (a : α) ∂P, ∀ i ∈ s, ∀ j ∈ t i, p i j a

Nested finite version of ae_forall_mem_finset.

@[reducible, inline]

abbrev HCPolySupport.Book.Ch04.RestrictionCoeffLaw (d : ℕ) : Type

A Chapter 4 law on global coefficient fields, carried by the honest-fields carrier RegCoeffField d (regularity free by type).

Equations

• HCPolySupport.Book.Ch04.RestrictionCoeffLaw d = MeasureTheory.Measure (HCPolySupport.RegCoeffField d)

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch04.restrictionSigma {d : ℕ} (U : Set (Vec d)) (hU : MeasurableSet U) : MeasurableSpace (RegCoeffField d)

The measurable restriction-local coefficient-field sigma algebra on a measurable observation set (carrier version).

Equations

• HCPolySupport.Book.Ch04.restrictionSigma U hU = HCPolySupport.RestrictionSigmaR U hU

def HCPolySupport.Book.Ch04.AEEllipticOn {d : ℕ} (lam Lam : ℝ) (U : Set (Vec d)) (a : RegCoeffField d) : Prop

Spatial a.e. ellipticity of a carrier coefficient field on an observation set, evaluated on the honest sample.

Equations

• HCPolySupport.Book.Ch04.AEEllipticOn lam Lam U a = HCPolySupport.IsAEEllipticFieldOn lam Lam U a.toFun

def HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticField {d : ℕ} (a : RegCoeffField d) : Prop

Public locally a.e.-uniform ellipticity: every triadic cube has deterministic spatial a.e. ellipticity constants.

Equations

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

def HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticLaw {d : ℕ} (P : RestrictionCoeffLaw d) : Prop

A law is supported on locally a.e.-uniformly elliptic fields.

Equations

• HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticLaw P = ∀ᵐ (a : HCPolySupport.RegCoeffField d) ∂P, HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticField a

theorem HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticField.exists_aeeEllipticOn_cubeSet {d : ℕ} {a : RegCoeffField d} (h : AELocallyUniformlyEllipticField a) (Q : TriadicCube d) : ∃ (lam : ℝ) (Lam : ℝ), 0 < lam ∧ lam ≤ Lam ∧ AEEllipticOn lam Lam (cubeSet Q) a

A locally a.e.-uniformly elliptic field is a.e.-elliptic on each half-open cube as well as on its open core.

theorem HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticField.exists_aeeQuantitativeEllipticSlice_cubeSet {d : ℕ} {a : RegCoeffField d} (h : AELocallyUniformlyEllipticField a) (Q : TriadicCube d) : ∃ (k : ℕ), AEEQuantitativeEllipticSlice (cubeSet Q) k a.toFun

A locally a.e.-uniformly elliptic field lies in some countable AEE quantitative slice on each half-open triadic cube.

theorem HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticLaw.ae_exists_aeeQuantitativeEllipticSlice_cubeSet {d : ℕ} {P : RestrictionCoeffLaw d} (hP : AELocallyUniformlyEllipticLaw P) (Q : TriadicCube d) : ∀ᵐ (a : RegCoeffField d) ∂P, ∃ (k : ℕ), AEEQuantitativeEllipticSlice (cubeSet Q) k a.toFun

A locally a.e.-elliptic law gives an a.s. countable AEE quantitative-slice cover for each deterministic triadic cube.

theorem HCPolySupport.Book.Ch04.nullMeasurableSet_of_localSigmaR {d : ℕ} (P : RestrictionCoeffLaw d) {U : Set (Vec d)} {s : Set (RegCoeffField d)} (hs : MeasurableSet s) : MeasureTheory.NullMeasurableSet s P

The honest carrier null-measurability bridge. Every event of the local entry-test carrier σ-algebra LocalSigmaR U is null-measurable for any carrier law P, because LocalSigmaR U is genuinely coarser than the canonical carrier σ-algebra (LocalSigmaR_le) — no hypothesis on P is required.

This is a free lemma, so it replaces the former LocalObservableLawCarrier hypothesis field of RestrictionLawCarrier (which asserted exactly this and was therefore always derivable — a vestigial hypothesis, removed as an R3-family strengthening). Consumers that need a local carrier event to be null-measurable (the Ch04 Mu/coarse-observable measurability handoff) call this directly.

Note (Packet P4b): the P4 report determined that the comap σ-algebra localSigma U = comap toFun (fine PointwiseLocalSigma U) is not ≤ the canonical carrier σ-algebra, so the AEE-slice event has no free null-measurability bridge along that route. The honest replacement is genuine LocalSigmaR (cubeSet Q) measurability of the slice event (measurableSet_localSigmaR_aeeQuantitativeEllipticSlice), which this bridge then promotes to null-measurability.

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

The AEE quantitative-slice event is genuinely LocalSigmaR-measurable, with no hypothesis on the law (Packet P4b). This is the honest core discovered by the P4 report: unlike the comap slice field, the entry-test-local LocalSigmaR event is genuinely below the canonical carrier σ-algebra, and its measurability is established directly by Lebesgue differentiation and the rational-ball average characterization (measurableSet_localSigmaR_aeeSlice). Being law-independent, it is a theorem, not a RestrictionLawCarrier field.

structure HCPolySupport.Book.Ch04.RestrictionLawCarrier {d : ℕ} (P : RestrictionCoeffLaw d) : Prop

The single public Chapter 4 law carrier. The former aee_quantitative_slice_measurable field was law-independent — its content is now the free theorem measurableSet_localSigmaR_aeeQuantitativeEllipticSlice (Packet P4b, an R3-family strengthening) — and has been removed.

• isProbability : MeasureTheory.IsProbabilityMeasure P
• ae_locally_uniformly_elliptic : AELocallyUniformlyEllipticLaw P

theorem HCPolySupport.Book.Ch04.lawCarrier_of_aeLocallyUniformlyElliptic {d : ℕ} {P : RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure P] (hP : AELocallyUniformlyEllipticLaw P) : RestrictionLawCarrier P

A probability law supported on locally a.e.-uniformly elliptic fields is a Chapter 4 law carrier. Both former measurability fields (the AEE-slice measurability and the earlier local-observable measurability) were vestigial — law-independent and derivable directly — and have been removed.

theorem HCPolySupport.Book.Ch04.RestrictionLawCarrier.ae_locallyUniformlyEllipticField {d : ℕ} {P : RestrictionCoeffLaw d} (hP : RestrictionLawCarrier P) : ∀ᵐ (a : RegCoeffField d) ∂P, AELocallyUniformlyEllipticField a

Canonical access to the a.s. locally a.e.-uniform ellipticity support of a Chapter 4 law carrier.

@[reducible, inline]

abbrev HCPolySupport.Book.Ch04.RestrictionStationaryLaw {d : ℕ} (P : RestrictionCoeffLaw d) : Prop

Public stationarity assumption (P1).

Equations

• HCPolySupport.Book.Ch04.RestrictionStationaryLaw P = HCPolySupport.IsStationaryR P

@[reducible, inline]

abbrev HCPolySupport.Book.Ch04.RestrictionUnitRangeDependentLaw {d : ℕ} (P : RestrictionCoeffLaw d) : Prop

The explicit restriction-unit-range dependence assumption: independence of the pointwise restriction σ-algebras of unit-separated measurable sets.

Equations

• HCPolySupport.Book.Ch04.RestrictionUnitRangeDependentLaw P = HCPolySupport.IsRestrictionUnitRangeDependentR P

@[reducible, inline]

abbrev HCPolySupport.Book.Ch04.RestrictionIsotropicLaw {d : ℕ} (P : RestrictionCoeffLaw d) : Prop

Public isotropy assumption (P3), restricted to signed permutations.

Equations

• HCPolySupport.Book.Ch04.RestrictionIsotropicLaw P = HCPolySupport.IsIsotropicInLawR P

@[reducible, inline]

abbrev HCPolySupport.Book.Ch04.RestrictionAdjointInvariantLaw {d : ℕ} (P : RestrictionCoeffLaw d) : Prop

Public adjoint-invariance assumption.

Equations

• HCPolySupport.Book.Ch04.RestrictionAdjointInvariantLaw P = HCPolySupport.IsAdjointInvariantInLawR P

structure HCPolySupport.Book.Ch04.RestrictionStructuralLaw {d : ℕ} (P : RestrictionCoeffLaw d) : Prop

The combined restriction-lane structural law assumptions, kept separate from measurability and ellipticity so downstream theorems request only what they use.

• stationary : RestrictionStationaryLaw P
• unit_range : RestrictionUnitRangeDependentLaw P
• isotropic : RestrictionIsotropicLaw P
• adjoint_invariant : RestrictionAdjointInvariantLaw P