Measurability

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Per-phase measurability of the corridor observable

The coarse observable is only a.e.-measurable under a RestrictionLawCarrier (the C3 wrap aestronglyMeasurable_coarseBlockQuadratic_cubeSet), so comp_measurable cannot be applied against L directly. Instead:

1. The corridor modification is packaged as the carrier endomorphism corridorReg ℓ σ : RegCoeffField d → RegCoeffField d — the corridor indicator is a fixed spatial set, so each entry of the modified field is a Borel case-split between a constant and the original entry, preserving both carrier regularity conjuncts. The endomorphism is genuinely Measurable at the join (measurable_corridorReg): the pointwise lane is a case-split between a constant and an evaluation, and the entry-test lane is affine in the generators — entryTestR i j φ (corridorReg ℓ σ a) is a constant plus the entry test of a against the complementary-masked probe Set.indicator (corridorSet ℓ σ)ᶜ φ (the spatial case-split is a-independent, unlike the elliptic truncation, so both lanes are honest).
2. The pushforward L.map (corridorReg ℓ σ) is again a RestrictionLawCarrier (lawCarrier_map_corridorReg): probability is preserved by measurability, and a.e. local uniform ellipticity is preserved by the pointwise corridor modification (aeLocallyUniformlyEllipticField_corridorReg); the a.e. pushforward uses MeasureTheory.ae_map_iff, whose measurable-set side condition is measurableSet_aeLocallyUniformlyEllipticField (the countable ⋂_Q ⋃_k of the AEE quantitative-slice sets, each genuinely LocalSigmaR-measurable on the carrier).
3. The C3 wrap on the pushforward pulls back along the measurable corridor endomorphism via AEStronglyMeasurable.comp_measurable (aestronglyMeasurable_phaseObservable).

The corridor set is open, hence measurable

theorem HCPolySupport.isOpen_corridorSet {d : ℕ} (ℓ : ℝ) (σ : Vec d) : IsOpen (corridorSet ℓ σ)

The corridor set is open: it is a countable union over (i, n) of the open slabs {x | |x i − σ i − n·ℓ| < 1}.

theorem HCPolySupport.measurableSet_corridorSet {d : ℕ} (ℓ : ℝ) (σ : Vec d) : MeasurableSet (corridorSet ℓ σ)

The corridor set is measurable.

M1.1 — the corridor carrier endomorphism and its genuine measurability

noncomputable def HCPolySupport.corridorReg {d : ℕ} (ℓ : ℝ) (σ : Vec d) (a : RegCoeffField d) : RegCoeffField d

The corridor modification as a carrier endomorphism (identity matrix on the corridor set, the original field off it). Both regularity conjuncts are preserved: each entry is a Borel case-split between a constant and the original entry over the measurable corridor set.

Equations

• HCPolySupport.corridorReg ℓ σ a = { toFun := HCPolySupport.corridorField ℓ σ a.toFun, entry_measurable := ⋯, entry_locInt := ⋯ }

@[simp]

theorem HCPolySupport.corridorReg_toFun {d : ℕ} (ℓ : ℝ) (σ : Vec d) (a : RegCoeffField d) : (corridorReg ℓ σ a).toFun = corridorField ℓ σ a.toFun

@[simp]

theorem HCPolySupport.corridorReg_apply {d : ℕ} (ℓ : ℝ) (σ : Vec d) (a : RegCoeffField d) (x : Vec d) : (corridorReg ℓ σ a).toFun x = corridorField ℓ σ a.toFun x

theorem HCPolySupport.entryTestR_corridorReg {d : ℕ} (i j : Fin d) {φ : Vec d → ℝ} (hφ : IsProbeR φ) (ℓ : ℝ) (σ : Vec d) (a : RegCoeffField d) : entryTestR i j φ (corridorReg ℓ σ a) = (∫ (x : Vec d), (corridorSet ℓ σ).indicator (fun (x : Vec d) => 1 i j * φ x) x) + entryTestR i j ((corridorSet ℓ σ)ᶜ.indicator φ) a

Affine generator transport for the corridor endomorphism: the entry test of the modified field is a constant plus the entry test of the original field against the complementary-masked probe.

theorem HCPolySupport.measurable_corridorReg {d : ℕ} (ℓ : ℝ) (σ : Vec d) : Measurable (corridorReg ℓ σ)

The corridor endomorphism is genuinely measurable at the join. The pointwise lane is a case-split between a constant and an evaluation; the entry-test lane is affine in the carrier generators (the spatial case-split is independent of the field, unlike the elliptic truncation).

M1.2 — ellipticity transport through the corridor

theorem HCPolySupport.aeLocallyUniformlyEllipticField_corridorReg {d : ℕ} {ℓ : ℝ} {σ : Vec d} {a : RegCoeffField d} (ha : Book.Ch04.AELocallyUniformlyEllipticField a) : Book.Ch04.AELocallyUniformlyEllipticField (corridorReg ℓ σ a)

The corridor modification preserves a.e. local uniform ellipticity. On the corridor set the field is the identity, elliptic with any constants lam'' ≤ 1 ≤ Lam''; off it the field is unchanged. On each triadic cube, with original constants (lam, Lam), the modified field is a.e. (min lam 1, max Lam 1)-elliptic; its spatial a.e.-strong measurability is the piecewise combination of the original coordinate map and a constant, gated by the measurable corridorSet.

M1.4 — pushforward RestrictionLawCarrier transport

theorem HCPolySupport.lawCarrier_map_corridorReg {d : ℕ} {L : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier L) (ℓ : ℝ) (σ : Vec d) : Book.Ch04.RestrictionLawCarrier (MeasureTheory.Measure.map (corridorReg ℓ σ) L)

The pushforward of a RestrictionLawCarrier law along the corridor endomorphism is again a RestrictionLawCarrier law.

M1 — the per-phase measurability theorem

theorem HCPolySupport.aestronglyMeasurable_phaseObservable {d : ℕ} {L : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier L) (m : ℤ) (ℓ : ℝ) (σ : Vec d) (P : BlockVec d) : MeasureTheory.AEStronglyMeasurable (fun (a : RegCoeffField d) => blockVecDot P (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d m)) (corridorField ℓ σ a.toFun)) P)) L

M1 (per-phase measurability). For a fixed grid phase σ, the coarse observable at the corridor-modified coefficient is a.e.-strongly-measurable under any RestrictionLawCarrier law.