Coarse-graining support: Support.Probability.RegCoeffField.Sigma

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

The carrier σ-algebra, its additive structure, and the layered builder

This file equips the carrier RegCoeffField d (see RegCoeffField.lean) with a measurable structure and proves the facts that make it usable as a probability carrier for the homogenization development.

• IsProbeR — the enriched probe class (bounded, measurable, compactly supported scalar test functions), adapted from the raw-CoeffField IsProbe of the salvage branch; the closure lemmas of_smooth, indicator, comp_homeomorph are carried over.
• entryTestR i j φ a = ∫ a(x)_{ij} · φ(x) dx — the linear single-entry generator, which is genuinely additive on the carrier (entryTestR_add): the integrand a(·)_{ij} · φ is honestly integrable because a(·)_{ij} is locally integrable and φ is a probe.
• pointwiseSigmaR, entryTestSigmaR, and the canonical instance instMeasurableSpaceRegCoeffField = pointwiseSigmaR ⊔ entryTestSigmaR.
• the builder criterion measurable_into_regCoeffField', and the crux instMeasurableAdd₂: addition is genuinely measurable at the join.
• measurable_layeredBuilder: base plus a finite sum of measurable layer maps is a genuinely measurable carrier-valued map — the acceptance theorem.
• endomorphism transport (adjointReg, measurable_adjointReg, and the general measurable_of_entryTestR_transport), and RegCoeffLaw d = Measure ....

The raw CoeffField's ambient σ-algebra is deliberately kept out of scope here, so the pi structure on Vec d → Mat d is the one used throughout (the paper, Armstrong–Kuusi–Loher, to appear).

@[instance_reducible]

instance HCPolySupport.instMatMeasurableSpace (d : ℕ) : MeasurableSpace (Mat d)

The entrywise (pi) measurable space on Mat d. Declared here — rather than importing the raw-CoeffField layer — so that the raw ambient σ-algebra on Vec d → Mat d stays out of scope and coordinate evaluation is governed by the pi structure.

Equations

• HCPolySupport.instMatMeasurableSpace d = id inferInstance

Probes

structure HCPolySupport.IsProbeR {d : ℕ} (φ : Vec d → ℝ) : Prop

The enriched probe class: bounded, measurable, compactly supported scalar test functions on Vec d. Bounded measurability (rather than continuity) is what keeps the class closed under multiplication by indicators, and is exactly enough to make the entry generator additive on the carrier (the paper, Armstrong–Kuusi–Loher, to appear).

• measurable : Measurable φ

  The probe is Borel measurable.

• bounded : ∃ (C : ℝ), ∀ (x : Vec d), |φ x| ≤ C

  The probe is uniformly bounded.

• hasCompactSupport : HasCompactSupport φ

  The probe has compact support.

theorem HCPolySupport.IsProbeR.of_smooth {d : ℕ} {φ : Vec d → ℝ} (hcont : ContDiff ℝ (↑⊤) φ) (hcs : HasCompactSupport φ) : IsProbeR φ

Smooth compactly-supported probes are enriched probes.

theorem HCPolySupport.IsProbeR.indicator {d : ℕ} {φ : Vec d → ℝ} (hφ : IsProbeR φ) {U : Set (Vec d)} (hU : MeasurableSet U) : IsProbeR (U.indicator φ)

The enriched probe class is closed under multiplication by the indicator of a measurable set.

theorem HCPolySupport.IsProbeR.comp_homeomorph {d : ℕ} {φ : Vec d → ℝ} (hφ : IsProbeR φ) (h : Vec d ≃ₜ Vec d) : IsProbeR (φ ∘ ⇑h)

The enriched probe class is closed under precomposition with a homeomorphism of the base space (translation/signed-permutation/rescaling transport).

The linear entry generator and its additivity

noncomputable def HCPolySupport.entryTestR {d : ℕ} (i j : Fin d) (φ : Vec d → ℝ) (a : RegCoeffField d) : ℝ

The linear single-entry generator on the carrier: ∫ a(x)_{ij} · φ(x) dx.

Equations

• HCPolySupport.entryTestR i j φ a = ∫ (x : HCPolySupport.Vec d), a.toFun x i j * φ x

theorem HCPolySupport.integrable_entry_mul_probe {d : ℕ} (i j : Fin d) {φ : Vec d → ℝ} (hφ : IsProbeR φ) (a : RegCoeffField d) : MeasureTheory.Integrable (fun (x : Vec d) => a.toFun x i j * φ x) MeasureTheory.volume

On the carrier, the integrand a(·)_{ij} · φ of a probe is genuinely integrable: a(·)_{ij} is locally integrable and φ is bounded, measurable and compactly supported, so the product is integrable on the (compact) support of φ and vanishes off it.

theorem HCPolySupport.entryTestR_add {d : ℕ} (i j : Fin d) {φ : Vec d → ℝ} (hφ : IsProbeR φ) (a b : RegCoeffField d) : entryTestR i j φ (a + b) = entryTestR i j φ a + entryTestR i j φ b

Genuine additivity of the entry generator on the carrier.

@[simp]

theorem HCPolySupport.entryTestR_zero {d : ℕ} (i j : Fin d) (φ : Vec d → ℝ) : entryTestR i j φ 0 = 0

theorem HCPolySupport.entryTestR_smul {d : ℕ} (i j : Fin d) {φ : Vec d → ℝ} (c : ℝ) (a : RegCoeffField d) : entryTestR i j φ (c • a) = c * entryTestR i j φ a

theorem HCPolySupport.entryTestR_finsetSum {d : ℕ} {ι : Type u_1} (i j : Fin d) {φ : Vec d → ℝ} (hφ : IsProbeR φ) (s : Finset ι) (g : ι → RegCoeffField d) : entryTestR i j φ (∑ l ∈ s, g l) = ∑ l ∈ s, entryTestR i j φ (g l)

entryTestR distributes over finite sums on the carrier.

The carrier σ-algebra

@[reducible, inline]

abbrev HCPolySupport.pointwiseSigmaR (d : ℕ) : MeasurableSpace (RegCoeffField d)

The pointwise (product) σ-algebra: the comap of the underlying map into the pi σ-algebra on Vec d → Mat d.

Equations

• HCPolySupport.pointwiseSigmaR d = MeasurableSpace.comap HCPolySupport.RegCoeffField.toFun MeasurableSpace.pi

@[reducible, inline]

abbrev HCPolySupport.entryTestSigmaR (d : ℕ) : MeasurableSpace (RegCoeffField d)

The entry-test σ-algebra: generated by the preimages of the linear entry generators over the enriched probe class.

Equations

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

@[instance_reducible]

instance HCPolySupport.instMeasurableSpaceRegCoeffField (d : ℕ) : MeasurableSpace (RegCoeffField d)

The canonical measurable structure on the carrier: the join of the pointwise and entry-test σ-algebras. Both generating families are additive, so this join supports a genuine MeasurableAdd₂ (see instMeasurableAdd₂).

Equations

• HCPolySupport.instMeasurableSpaceRegCoeffField d = HCPolySupport.pointwiseSigmaR d ⊔ HCPolySupport.entryTestSigmaR d

theorem HCPolySupport.pointwiseSigmaR_le (d : ℕ) : pointwiseSigmaR d ≤ instMeasurableSpaceRegCoeffField d

theorem HCPolySupport.entryTestSigmaR_le (d : ℕ) : entryTestSigmaR d ≤ instMeasurableSpaceRegCoeffField d

@[reducible, inline]

abbrev HCPolySupport.LocalSigmaR {d : ℕ} (U : Set (Vec d)) : MeasurableSpace (RegCoeffField d)

The local carrier σ-algebra on an observation set U: generated by the entry-test preimages using only probes supported in U. This is the honest carrier analog of the raw-CoeffField PointwiseLocalSigma U: it records exactly the information about a field carried by linear entry tests localized to U. Unlike the raw fine PointwiseLocalSigma, it is coarser than the canonical carrier σ-algebra (LocalSigmaR_le), so bounded local events are genuinely measurable — the carrier win over the powerset-fine raw local σ-algebra (the paper, Armstrong–Kuusi–Loher, to appear).

Equations

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

Measurability infrastructure

theorem HCPolySupport.measurable_into_sup {α : Type u_1} {β : Type u_2} {dom : MeasurableSpace α} {m1 m2 : MeasurableSpace β} {f : α → β} (h1 : Measurable f) (h2 : Measurable f) : Measurable f

Measurability into a join reduces to measurability into each summand.

theorem HCPolySupport.measurable_matrix_of_entries {d : ℕ} {α : Type u_1} [MeasurableSpace α] {h : α → Mat d} (H : ∀ (i j : Fin d), Measurable fun (a : α) => h a i j) : Measurable h

A map into Mat d is measurable iff every scalar entry is measurable.

theorem HCPolySupport.measurable_toFun_of_entries {d : ℕ} {α : Type u_1} [MeasurableSpace α] {F : α → RegCoeffField d} (H : ∀ (y : Vec d) (i j : Fin d), Measurable fun (a : α) => (F a).toFun y i j) : Measurable fun (a : α) => (F a).toFun

A carrier-valued map is pointwise (pi-)measurable iff every scalar entry evaluation is measurable.

theorem HCPolySupport.measurable_into_pointwiseSigmaR {d : ℕ} {α : Type u_1} [MeasurableSpace α] {F : α → RegCoeffField d} (h : Measurable fun (a : α) => (F a).toFun) : Measurable F

Builder for the pointwise lane.

theorem HCPolySupport.measurable_into_entryTestSigmaR {d : ℕ} {α : Type u_1} [MeasurableSpace α] {F : α → RegCoeffField d} (h : ∀ (i j : Fin d) (φ : Vec d → ℝ), IsProbeR φ → Measurable fun (a : α) => entryTestR i j φ (F a)) : Measurable F

Builder for the entry-test lane: measurable into entryTestSigmaR iff every generator functional is measurable after the map.

theorem HCPolySupport.measurable_into_regCoeffField' {d : ℕ} {α : Type u_1} [MeasurableSpace α] {F : α → RegCoeffField d} (hpt : ∀ (y : Vec d) (i j : Fin d), Measurable fun (a : α) => (F a).toFun y i j) (hgen : ∀ (i j : Fin d) (φ : Vec d → ℝ), IsProbeR φ → Measurable fun (a : α) => entryTestR i j φ (F a)) : Measurable F

Builder criterion at the join. A map into the carrier is measurable for the canonical σ-algebra iff every scalar entry evaluation is measurable (pointwise lane) and every entry generator functional is measurable (entry-test lane).

theorem HCPolySupport.measurable_apply_entry {d : ℕ} (y : Vec d) (i j : Fin d) : Measurable fun (a : RegCoeffField d) => a.toFun y i j

Scalar entry evaluation is measurable for the canonical σ-algebra (pointwise information is recovered from the pointwise lane).

theorem HCPolySupport.measurable_entryTestR {d : ℕ} (i j : Fin d) {φ : Vec d → ℝ} (hφ : IsProbeR φ) : Measurable (entryTestR i j φ)

The entry generator functional is measurable for the canonical σ-algebra.

theorem HCPolySupport.LocalSigmaR_le {d : ℕ} (U : Set (Vec d)) : LocalSigmaR U ≤ instMeasurableSpaceRegCoeffField d

The local carrier σ-algebra is coarser than the canonical one. Each generator of LocalSigmaR U is an entry-test preimage of a measurable set, hence measurable for the canonical σ-algebra.

The crux: MeasurableAdd₂ at the join

instance HCPolySupport.instMeasurableAdd₂ {d : ℕ} : MeasurableAdd₂ (RegCoeffField d)

Addition is genuinely measurable at the join. Both lanes are handled by additivity of their generators: the pointwise lane by coordinatewise additivity of evaluations, the entry-test lane by entryTestR_add. This is exactly what fails on the raw junk-field space.

The layered builder (acceptance theorem)

theorem HCPolySupport.measurable_layeredBuilder {d : ℕ} {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] {s : Finset ι} {base : α → RegCoeffField d} {A : ι → α → RegCoeffField d} (hbase : Measurable base) (hA : ∀ l ∈ s, Measurable (A l)) : Measurable fun (ω : α) => base ω + ∑ l ∈ s, A l ω

The layered Superdiffusion builder is a genuinely measurable carrier-valued map. Once addition is measurable at the join, a base field-map plus a finite sum of measurable layer maps is measurable — no a.e. qualification needed.

Endomorphism transport

def HCPolySupport.adjointReg {d : ℕ} (a : RegCoeffField d) : RegCoeffField d

The adjoint (entrywise transpose) is a carrier endomorphism.

Equations

• HCPolySupport.adjointReg a = { toFun := fun (x : HCPolySupport.Vec d) => Matrix.transpose (a.toFun x), entry_measurable := ⋯, entry_locInt := ⋯ }

@[simp]

theorem HCPolySupport.adjointReg_apply {d : ℕ} (a : RegCoeffField d) (x : Vec d) : (adjointReg a).toFun x = Matrix.transpose (a.toFun x)

theorem HCPolySupport.entryTestR_adjointReg {d : ℕ} (i j : Fin d) (φ : Vec d → ℝ) (a : RegCoeffField d) : entryTestR i j φ (adjointReg a) = entryTestR j i φ a

Generator transport for the adjoint.

theorem HCPolySupport.measurable_adjointReg {d : ℕ} : Measurable adjointReg

The adjoint is genuinely measurable at the join — the model endomorphism, measurable by generator transport in both lanes.

theorem HCPolySupport.measurable_of_entryTestR_transport {d : ℕ} {T : RegCoeffField d → RegCoeffField d} (hpt : ∀ (y : Vec d) (i j : Fin d), Measurable fun (a : RegCoeffField d) => (T a).toFun y i j) (htrans : ∀ (i j : Fin d) (φ : Vec d → ℝ), IsProbeR φ → ∃ (c : ℝ) (i' : Fin d) (j' : Fin d) (ψ : Vec d → ℝ), IsProbeR ψ ∧ ∀ (a : RegCoeffField d), entryTestR i j φ (T a) = c * entryTestR i' j' ψ a) : Measurable T

General probe-transport criterion for endomorphisms. A self-map T of the carrier is measurable at the join if every scalar entry of T a is a measurable function of a, and each entry generator on T a equals a scalar multiple of a (possibly relabelled) entry generator on a. Translation, rotation, adjoint and dilation all fit this pattern (the paper, Armstrong–Kuusi–Loher, to appear).

Laws on the carrier

@[reducible, inline]

abbrev HCPolySupport.RegCoeffLaw (d : ℕ) : Type

A law on the carrier is a measure on RegCoeffField d (for the canonical σ-algebra). Packet P3 retargets RestrictionCoeffLaw to this type.

Equations

• HCPolySupport.RegCoeffLaw d = MeasureTheory.Measure (HCPolySupport.RegCoeffField d)