Coarse-graining support: Support.Geometry.BoundedMeasurableDomain

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

Bounded measurable domains with normalized volume

This module packages the minimum geometric data needed to use volume-normalized integrals on a bounded measurable domain of strictly positive Lebesgue volume. The normalization is an ENNReal rescaling of restricted Lebesgue measure, so it has no zero-volume fallback and does not use ENNReal.toReal to define a measure.

structure HCPolySupport.BoundedMeasurableDomain (d : ℕ) : Type

A bounded measurable subset of R^d with strictly positive Lebesgue volume.

• carrier : Set (Vec d)

  The underlying measurable subset of R^d.

• measurableSet : MeasurableSet self.carrier
• isBoundedDomain : IsBoundedDomain self.carrier
• volume_pos : 0 < MeasureTheory.volume self.carrier

@[instance_reducible]

instance HCPolySupport.BoundedMeasurableDomain.instSetLikeVec {d : ℕ} : SetLike (BoundedMeasurableDomain d) (Vec d)

Equations

• HCPolySupport.BoundedMeasurableDomain.instSetLikeVec = { coe := fun (U : HCPolySupport.BoundedMeasurableDomain d) => U.carrier, coe_injective := ⋯ }

@[simp]

theorem HCPolySupport.BoundedMeasurableDomain.coe_mk {d : ℕ} (U : Set (Vec d)) (hU_meas : MeasurableSet U) (hU_bounded : IsBoundedDomain U) (hU_pos : 0 < MeasureTheory.volume U) : ↑{ carrier := U, measurableSet := hU_meas, isBoundedDomain := hU_bounded, volume_pos := hU_pos } = U

theorem HCPolySupport.BoundedMeasurableDomain.isBounded {d : ℕ} (U : BoundedMeasurableDomain d) : Bornology.IsBounded ↑U

The bounded-domain witness gives a bounded set in the ambient norm.

theorem HCPolySupport.BoundedMeasurableDomain.volume_lt_top {d : ℕ} (U : BoundedMeasurableDomain d) : MeasureTheory.volume ↑U < ⊤

Lebesgue measure of a bounded measurable domain is finite.

theorem HCPolySupport.BoundedMeasurableDomain.volume_ne_zero {d : ℕ} (U : BoundedMeasurableDomain d) : MeasureTheory.volume ↑U ≠ 0

theorem HCPolySupport.BoundedMeasurableDomain.volume_ne_top {d : ℕ} (U : BoundedMeasurableDomain d) : MeasureTheory.volume ↑U ≠ ⊤

noncomputable def HCPolySupport.BoundedMeasurableDomain.restrictedVolume {d : ℕ} (U : BoundedMeasurableDomain d) : MeasureTheory.Measure (Vec d)

Restricted Lebesgue measure on a bounded measurable domain.

Equations

• U.restrictedVolume = MeasureTheory.volume.restrict ↑U

@[simp]

theorem HCPolySupport.BoundedMeasurableDomain.restrictedVolume_apply_univ {d : ℕ} (U : BoundedMeasurableDomain d) : U.restrictedVolume Set.univ = MeasureTheory.volume ↑U

noncomputable def HCPolySupport.BoundedMeasurableDomain.normalizedVolume {d : ℕ} (U : BoundedMeasurableDomain d) : MeasureTheory.Measure (Vec d)

The probability measure obtained by normalizing restricted Lebesgue measure.

Equations

• U.normalizedVolume = (MeasureTheory.volume ↑U)⁻¹ • U.restrictedVolume

@[simp]

theorem HCPolySupport.BoundedMeasurableDomain.normalizedVolume_apply_univ {d : ℕ} (U : BoundedMeasurableDomain d) : U.normalizedVolume Set.univ = 1

theorem HCPolySupport.BoundedMeasurableDomain.normalizedVolume_ne_zero {d : ℕ} (U : BoundedMeasurableDomain d) : U.normalizedVolume ≠ 0

theorem HCPolySupport.BoundedMeasurableDomain.restrictedVolume_isFiniteMeasure {d : ℕ} (U : BoundedMeasurableDomain d) : MeasureTheory.IsFiniteMeasure U.restrictedVolume

Restricted volume is finite on a bounded measurable domain.

theorem HCPolySupport.BoundedMeasurableDomain.normalizedVolume_isFiniteMeasure {d : ℕ} (U : BoundedMeasurableDomain d) : MeasureTheory.IsFiniteMeasure U.normalizedVolume

Normalized volume is a finite measure, without registering a global instance.

theorem HCPolySupport.BoundedMeasurableDomain.integrable_normalizedVolume_iff {d : ℕ} (U : BoundedMeasurableDomain d) {E : Type u_1} [NormedAddCommGroup E] (f : Vec d → E) : MeasureTheory.Integrable f U.normalizedVolume ↔ MeasureTheory.Integrable f U.restrictedVolume

Integrability is unchanged by the strictly positive finite normalization factor.

theorem HCPolySupport.BoundedMeasurableDomain.integrable_normalizedVolume {d : ℕ} (U : BoundedMeasurableDomain d) {E : Type u_1} [NormedAddCommGroup E] (f : Vec d → E) (hf : MeasureTheory.Integrable f U.restrictedVolume) : MeasureTheory.Integrable f U.normalizedVolume

The integrability witness required by average is valid for normalized volume.

noncomputable def HCPolySupport.BoundedMeasurableDomain.average {d : ℕ} (U : BoundedMeasurableDomain d) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : Vec d → E) (_hf : MeasureTheory.Integrable f U.restrictedVolume) : E

The volume-normalized Bochner average of an integrable function.

The explicit proof is transported to normalizedVolume by integrable_normalizedVolume; thus its integral body is integrable.

Equations

• U.average f _hf = ∫ (x : HCPolySupport.Vec d), f x ∂U.normalizedVolume

theorem HCPolySupport.BoundedMeasurableDomain.average_eq_volume_toReal_inv_smul_setIntegral {d : ℕ} (U : BoundedMeasurableDomain d) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : Vec d → E) (hf : MeasureTheory.Integrable f U.restrictedVolume) : U.average f hf = (MeasureTheory.volume ↑U).toReal⁻¹ • ∫ (x : Vec d) in ↑U, f x

The normalized Bochner average is inverse volume times the set integral.

theorem HCPolySupport.BoundedMeasurableDomain.average_eq_volume_toReal_inv_mul_setIntegral {d : ℕ} (U : BoundedMeasurableDomain d) (f : Vec d → ℝ) (hf : MeasureTheory.Integrable f U.restrictedVolume) : U.average f hf = (MeasureTheory.volume ↑U).toReal⁻¹ * ∫ (x : Vec d) in ↑U, f x

The source-style scalar average formula.

noncomputable def HCPolySupport.BoundedMeasurableDomain.pairing {d : ℕ} (U : BoundedMeasurableDomain d) (f g : Vec d → ℝ) (hfg : MeasureTheory.Integrable (fun (x : Vec d) => f x * g x) U.restrictedVolume) : ℝ

The volume-normalized scalar pairing of an integrable product.

Equations

• U.pairing f g hfg = U.average (fun (x : HCPolySupport.Vec d) => f x * g x) hfg

theorem HCPolySupport.BoundedMeasurableDomain.pairing_eq_volume_toReal_inv_mul_setIntegral {d : ℕ} (U : BoundedMeasurableDomain d) (f g : Vec d → ℝ) (hfg : MeasureTheory.Integrable (fun (x : Vec d) => f x * g x) U.restrictedVolume) : U.pairing f g hfg = (MeasureTheory.volume ↑U).toReal⁻¹ * ∫ (x : Vec d) in ↑U, f x * g x

The scalar pairing is the source-style normalized set integral.