Coarse-graining support: Support.Probability.RegCoeffField

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

The regular-coefficient-field carrier

This file introduces RegCoeffField d, the carrier of honest coefficient fields on which the probabilistic layer of the homogenization development is based. A RegCoeffField d is a map Vec d → Mat d whose entries are Borel measurable and locally integrable — the minimal regularity level at which the linear entry-test integral (see RegCoeffField/Sigma.lean) is genuinely additive and at which a.e.-regularity hypotheses become free by type.

The deterministic layers (Sobolev/PDE/coarse-graining algebra) continue to work with the raw CoeffField d = Vec d → Mat d; they receive a.toFun through the coercion RegCoeffField.toCoeffField.

The carrier is a commutative monoid under pointwise addition, is closed under real scaling and finite sums, and contains the constant fields (constRegCoeffField, including 1); each closure property is witnessed by the corresponding closure of measurability and local integrability.

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

structure HCPolySupport.RegCoeffField (d : ℕ) : Type

The regular-fields carrier: entrywise-Borel-measurable, locally-integrable coefficient fields. Regularity is now free by type: every element carries a proof that each of its scalar entries is measurable and locally integrable (the paper, Armstrong–Kuusi–Loher, to appear).

• toFun : Vec d → Mat d

  The underlying raw coefficient field.

• entry_measurable (i j : Fin d) : Measurable fun (x : Vec d) => self.toFun x i j

  Each scalar entry is Borel measurable.

• entry_locInt (i j : Fin d) : MeasureTheory.LocallyIntegrable (fun (x : Vec d) => self.toFun x i j) MeasureTheory.volume

  Each scalar entry is locally integrable for the Lebesgue measure.

@[instance_reducible]

instance HCPolySupport.RegCoeffField.instCoeFunForallVecMat {d : ℕ} : CoeFun (RegCoeffField d) fun (x : RegCoeffField d) => Vec d → Mat d

Equations

• HCPolySupport.RegCoeffField.instCoeFunForallVecMat = { coe := HCPolySupport.RegCoeffField.toFun }

@[simp]

theorem HCPolySupport.RegCoeffField.coe_mk {d : ℕ} (f : Vec d → Mat d) (h₁ : ∀ (i j : Fin d), Measurable fun (x : Vec d) => f x i j) (h₂ : ∀ (i j : Fin d), MeasureTheory.LocallyIntegrable (fun (x : Vec d) => f x i j) MeasureTheory.volume) (x : Vec d) : { toFun := f, entry_measurable := h₁, entry_locInt := h₂ }.toFun x = f x

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

Coercion back to the raw deterministic carrier CoeffField d. Deterministic layers receive a.toCoeffField = a.toFun and are untouched by the carrier.

Equations

• a.toCoeffField = a.toFun

theorem HCPolySupport.RegCoeffField.toFun_eq_coe {d : ℕ} (a : RegCoeffField d) : a.toFun = a.toCoeffField

The existing raw-carrier projection agrees with the stored coefficient function.

@[simp]

theorem HCPolySupport.RegCoeffField.toCoeffField_apply {d : ℕ} (a : RegCoeffField d) (x : Vec d) : a.toCoeffField x = a.toFun x

theorem HCPolySupport.RegCoeffField.ext {d : ℕ} {a b : RegCoeffField d} (h : ∀ (x : Vec d), a.toFun x = b.toFun x) : a = b

theorem HCPolySupport.RegCoeffField.ext_iff {d : ℕ} {a b : RegCoeffField d} : a = b ↔ ∀ (x : Vec d), a.toFun x = b.toFun x

Zero

@[instance_reducible]

instance HCPolySupport.RegCoeffField.instZero {d : ℕ} : Zero (RegCoeffField d)

Equations

• HCPolySupport.RegCoeffField.instZero = { zero := { toFun := 0, entry_measurable := ⋯, entry_locInt := ⋯ } }

@[simp]

theorem HCPolySupport.RegCoeffField.zero_toFun {d : ℕ} : toFun 0 = 0

@[simp]

theorem HCPolySupport.RegCoeffField.zero_apply {d : ℕ} (x : Vec d) : toFun 0 x = 0

Addition

@[instance_reducible]

instance HCPolySupport.RegCoeffField.instAdd {d : ℕ} : Add (RegCoeffField d)

Equations

• HCPolySupport.RegCoeffField.instAdd = { add := fun (a b : HCPolySupport.RegCoeffField d) => { toFun := a.toFun + b.toFun, entry_measurable := ⋯, entry_locInt := ⋯ } }

@[simp]

theorem HCPolySupport.RegCoeffField.add_toFun {d : ℕ} (a b : RegCoeffField d) : (a + b).toFun = a.toFun + b.toFun

@[simp]

theorem HCPolySupport.RegCoeffField.add_apply {d : ℕ} (a b : RegCoeffField d) (x : Vec d) : (a + b).toFun x = a.toFun x + b.toFun x

@[simp]

theorem HCPolySupport.RegCoeffField.coe_add {d : ℕ} (a b : RegCoeffField d) : (a + b).toFun = a.toFun + b.toFun

Real scaling

@[instance_reducible]

instance HCPolySupport.RegCoeffField.instSMulReal {d : ℕ} : SMul ℝ (RegCoeffField d)

Equations

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

@[simp]

theorem HCPolySupport.RegCoeffField.smul_toFun {d : ℕ} (c : ℝ) (a : RegCoeffField d) : (c • a).toFun = fun (x : Vec d) => c • a.toFun x

@[simp]

theorem HCPolySupport.RegCoeffField.smul_apply {d : ℕ} (c : ℝ) (a : RegCoeffField d) (x : Vec d) : (c • a).toFun x = c • a.toFun x

Commutative monoid structure

@[instance_reducible]

instance HCPolySupport.RegCoeffField.instAddCommMonoid {d : ℕ} : AddCommMonoid (RegCoeffField d)

Equations

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

@[simp]

theorem HCPolySupport.RegCoeffField.finset_sum_apply {d : ℕ} {ι : Type u_1} (s : Finset ι) (g : ι → RegCoeffField d) (x : Vec d) : (∑ l ∈ s, g l).toFun x = ∑ l ∈ s, (g l).toFun x

Evaluation of a finite sum of carrier elements is the finite sum of the evaluations.

theorem HCPolySupport.RegCoeffField.finset_sum_toFun {d : ℕ} {ι : Type u_1} (s : Finset ι) (g : ι → RegCoeffField d) : (∑ l ∈ s, g l).toFun = ∑ l ∈ s, (g l).toFun

Constant fields

def HCPolySupport.RegCoeffField.constRegCoeffField {d : ℕ} (M : Mat d) : RegCoeffField d

The constant regular field with value the matrix M. Constant maps are measurable and locally integrable, so this is a genuine carrier element.

Equations

• HCPolySupport.RegCoeffField.constRegCoeffField M = { toFun := fun (x : HCPolySupport.Vec d) => M, entry_measurable := ⋯, entry_locInt := ⋯ }

@[simp]

theorem HCPolySupport.RegCoeffField.constRegCoeffField_apply {d : ℕ} (M : Mat d) (x : Vec d) : (constRegCoeffField M).toFun x = M

@[simp]

theorem HCPolySupport.RegCoeffField.constRegCoeffField_zero {d : ℕ} : constRegCoeffField 0 = 0

@[instance_reducible]

instance HCPolySupport.RegCoeffField.instOne {d : ℕ} : One (RegCoeffField d)

The constant identity-matrix field.

Equations

• HCPolySupport.RegCoeffField.instOne = { one := HCPolySupport.RegCoeffField.constRegCoeffField 1 }

@[simp]

theorem HCPolySupport.RegCoeffField.one_apply {d : ℕ} (x : Vec d) : toFun 1 x = 1

@[simp]

theorem HCPolySupport.RegCoeffField.one_toFun {d : ℕ} : toFun 1 = fun (x : Vec d) => 1

A regularity utility: bounded measurable ⟹ locally integrable

theorem HCPolySupport.RegCoeffField.locallyIntegrable_of_bounded_measurable {d : ℕ} {f : Vec d → ℝ} (hf : Measurable f) {C : ℝ} (hC : ∀ (x : Vec d), |f x| ≤ C) : MeasureTheory.LocallyIntegrable f MeasureTheory.volume

A bounded measurable scalar field on Vec d is locally integrable for the Lebesgue measure. This discharges the local-integrability obligation for carriers built from bounded data (e.g. the checkerboard). The Lebesgue measure on Vec d = Fin d → ℝ is finite on compacts and the space is locally compact, so integrability on every compact set follows from the uniform bound.