CellMeasure.lean`

40 declarations, 0 contain sorry, 0 declared as axioms

Coordinate assembly and source normalization for genuine vector cell moments. The scalar moving-cell calculus is an explicit input; no differentiability of a cell or of its coefficients is assumed implicitly.

def OAI.Problem358.NormalizedCell.measure line 15
Source documentation
The probability law obtained by normalizing the restriction to a positive finite cell.
```
def measure (ρ : Measure X) (P : Set X) : Measure X :=
…
```
theorem OAI.Problem358.NormalizedCell.real_mass_pos line 21
Source documentation
Positive finite extended mass is positive in the real-mass convention.
```
theorem real_mass_pos (hpos : 0 < ρ P) (hfinite : ρ P ≠ ∞) :
    0 < ρ.real P :=
…
```
theorem OAI.Problem358.NormalizedCell.probability line 26
Source documentation
Normalization is a probability whenever the cell has positive finite mass.
```
theorem probability (hpos : 0 < ρ P) (hfinite : ρ P ≠ ∞) :
    IsProbabilityMeasure (measure ρ P) := by
…
```
Mentions: OAI.Problem358.NormalizedCell.measure
theorem OAI.Problem358.NormalizedCell.mass_smul line 33
Source documentation
Multiplying the normalized law by its cell mass recovers the raw restriction.
```
theorem mass_smul (hpos : 0 < ρ P) (hfinite : ρ P ≠ ∞) :
    (ρ P) • measure ρ P = ρ.restrict P := by
…
```
Mentions: OAI.Problem358.NormalizedCell.measure
theorem OAI.Problem358.NormalizedCell.ofReal_mass_smul line 38
Source documentation
The same cancellation in the real-mass notation used by cell derivatives.
```
theorem ofReal_mass_smul (hpos : 0 < ρ P) (hfinite : ρ P ≠ ∞) :
    ENNReal.ofReal (ρ.real P) • measure ρ P = ρ.restrict P := by
…
```
Mentions: OAI.Problem358.NormalizedCell.measure
theorem OAI.Problem358.NormalizedCell.ae_mem line 44
Source documentation
The normalized restriction remains almost surely inside its measurable cell.
```
theorem ae_mem (hP : MeasurableSet P) : ∀ᵐ x ∂measure ρ P, x ∈ P := by
…
```
Mentions: OAI.Problem358.NormalizedCell.measure
theorem OAI.Problem358.NormalizedCell.integrable_iff line 50
Source documentation
No integrability is lost or gained by a positive finite cell normalization.
```
theorem integrable_iff {V : Type*} [NormedAddCommGroup V] {f : X → V}
    (hpos : 0 < ρ P) (hfinite : ρ P ≠ ∞) :
    Integrable f (measure ρ P) ↔ IntegrableOn f P ρ := by
…
```
Mentions: OAI.Problem358.NormalizedCell.measure
theorem OAI.Problem358.NormalizedCell.mass_smul_integral line 58
Source documentation
Weighted averages under the normalized cell law recover raw cell integrals. The identity is valid for real or vector valued functions, even without integrability.
```
theorem mass_smul_integral {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
    (hpos : 0 < ρ P) (hfinite : ρ P ≠ ∞) (f : X → V) :
    ρ.real P • (∫ x, f x ∂measure ρ P) = ∫ x in P, f x ∂ρ := by
…
```
Mentions: OAI.Problem358.NormalizedCell.measure
theorem OAI.Problem358.NormalizedCell.mass_mul_integral line 65
Source documentation
Scalar form of the weighted-average identity.
```
theorem mass_mul_integral (hpos : 0 < ρ P) (hfinite : ρ P ≠ ∞) (f : X → ℝ) :
    ρ.real P * (∫ x, f x ∂measure ρ P) = ∫ x in P, f x ∂ρ :=
…
```
Mentions: OAI.Problem358.NormalizedCell.measure

theorem OAI.Problem358.NormalizedCell.mass_smul_integral_of_map_eq line 70

Source documentation

Any random variable with the normalized cell law has the same weighted moments.

theorem mass_smul_integral_of_map_eq
    {Z : Type*} [MeasurableSpace Z] {π : Measure Z} {g : Z → X}
    {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
    (hpos : 0 < ρ P) (hfinite : ρ P ≠ ∞) (hg : Measurable g)
    (hmap : Measure.map g π = measure ρ P) {f : X → V}
    (hf : AEStronglyMeasurable f (measure ρ P)) :
    ρ.real P • (∫ z, f (g z) ∂π) = ∫ x in P, f x ∂ρ := by
…

Mentions: OAI.Problem358.NormalizedCell.measure

theorem OAI.Problem358.NormalizedCell.measure_smul line 82
Source documentation
Normalizing a cell removes any positive finite scalar prefactor in the source.
```
theorem measure_smul (c : ℝ≥0∞) (hc0 : c ≠ 0) (hctop : c ≠ ∞) :
    measure (c • ρ) P = measure ρ P := by
…
```
Mentions: OAI.Problem358.NormalizedCell.measure
theorem OAI.Problem358.NormalizedCell.measure_restrict line 90
Source documentation
Restricting the source to a larger set does not change the normalized cell law.
```
theorem measure_restrict {K : Set X} (hP : MeasurableSet P) (hPK : P ⊆ K) :
    measure (ρ.restrict K) P = measure ρ P := by
…
```
Mentions: OAI.Problem358.NormalizedCell.measure
def OAI.Problem358.normalizedCellLaw line 101
Source documentation
The probability law obtained by conditioning a measure on a positive finite cell.
```
def normalizedCellLaw {X : Type*} [MeasurableSpace X]
    (ρ : Measure X) (P : Set X) : Measure X :=
…
```
lemma OAI.Problem358.normalizedCellLaw_isProbabilityMeasure line 109
lemma OAI.Problem358.normalizedCellLaw_ae_mem line 115
lemma OAI.Problem358.mass_smul_normalizedCellLaw line 120
Source documentation
Multiplying a normalized cell law by its original mass recovers the restricted measure.
```
lemma mass_smul_normalizedCellLaw (hpos : ρ P ≠ 0) (hfin : ρ P ≠ ∞) :
    ENNReal.ofReal (ρ.real P) • normalizedCellLaw ρ P = ρ.restrict P := by
…
```
Mentions: OAI.Problem358.normalizedCellLaw
lemma OAI.Problem358.integral_normalizedCellLaw line 125
lemma OAI.Problem358.mass_smul_integral_normalizedCellLaw line 130
Source documentation
Raw scalar moments and vector barycentres are the mass times their normalized integrals.
```
lemma mass_smul_integral_normalizedCellLaw (f : X → V)
    (hpos : ρ P ≠ 0) (hfin : ρ P ≠ ∞) :
    (ρ.real P) • (∫ x, f x ∂normalizedCellLaw ρ P) = ∫ x in P, f x ∂ρ := by
…
```
Mentions: OAI.Problem358.normalizedCellLaw
lemma OAI.Problem358.integrable_normalizedCellLaw_iff line 137
lemma OAI.Problem358.lintegral_normalizedCellLaw line 142

lemma OAI.Problem358.mass_smul_integral_fst_of_normalizedCellLaw line 147

Source documentation

A first marginal equal to a normalized cell law recovers the cell's raw moment.

lemma mass_smul_integral_fst_of_normalizedCellLaw
    {Y : Type*} [MeasurableSpace Y] (π : Measure (X × Y)) (f : X → V)
    (hpos : ρ P ≠ 0) (hfin : ρ P ≠ ∞)
    (hmarg : Measure.map Prod.fst π = normalizedCellLaw ρ P)
    (hf : IntegrableOn f P ρ) :
    (ρ.real P) • (∫ p, f p.1 ∂π) = ∫ x in P, f x ∂ρ := by
…

Mentions: OAI.Problem358.normalizedCellLaw

lemma OAI.Problem358.mass_smul_integral_snd_of_normalizedCellLaw line 160

Source documentation

The corresponding second-marginal formula, used for the other coupled cell.

lemma mass_smul_integral_snd_of_normalizedCellLaw
    {Y : Type*} [MeasurableSpace Y] (π : Measure (Y × X)) (f : X → V)
    (hpos : ρ P ≠ 0) (hfin : ρ P ≠ ∞)
    (hmarg : Measure.map Prod.snd π = normalizedCellLaw ρ P)
    (hf : IntegrableOn f P ρ) :
    (ρ.real P) • (∫ p, f p.2 ∂π) = ∫ x in P, f x ∂ρ := by
…

Mentions: OAI.Problem358.normalizedCellLaw

lemma OAI.Problem358.sum_mass_smul_normalizedCellLaw line 173

Source documentation

Normalized laws of a finite almost-everywhere partition reconstruct the source.

lemma sum_mass_smul_normalizedCellLaw {ι : Type*} [Fintype ι]
    (P : ι → Set X) (hP : ∀ i, MeasurableSet (P i))
    (hdis : Pairwise (fun i j => AEDisjoint ρ (P i) (P j)))
    (hcover : ∀ᵐ x ∂ρ, x ∈ ⋃ i, P i)
    (hpos : ∀ i, ρ (P i) ≠ 0) (hfin : ∀ i, ρ (P i) ≠ ∞) :
    (∑ i, ENNReal.ofReal (ρ.real (P i)) • normalizedCellLaw ρ (P i)) = ρ := by
…

Mentions: OAI.Problem358.normalizedCellLaw

lemma OAI.Problem358.sum_mass_smul_integral_normalizedCellLaw line 185

Source documentation

Scalar moments and vector barycentres sum over normalized cell laws with raw masses.

lemma sum_mass_smul_integral_normalizedCellLaw {ι : Type*} [Fintype ι]
    (P : ι → Set X) (hP : ∀ i, MeasurableSet (P i))
    (hdis : Pairwise (fun i j => AEDisjoint ρ (P i) (P j)))
    (hcover : ∀ᵐ x ∂ρ, x ∈ ⋃ i, P i)
    (hpos : ∀ i, ρ (P i) ≠ 0) (hfin : ∀ i, ρ (P i) ≠ ∞)
    (f : X → V) (hf : Integrable f ρ) :
    (∑ i, (ρ.real (P i)) • ∫ x, f x ∂normalizedCellLaw ρ (P i)) = ∫ x, f x ∂ρ := by
…

Mentions: OAI.Problem358.normalizedCellLaw

theorem OAI.Problem358.normalizedCell_uniformMeasure line 203
Source documentation
The normalized restriction of a uniform source to a cell is exactly the uniform law of that cell; this identifies the laws used by midpoint couplings.
```
theorem normalizedCell_uniformMeasure {d : ℕ} {K P : Set (E d)}
    (hKpos : 0 < volume K) (hKfinite : volume K ≠ ∞)
    (hP : MeasurableSet P) (hPK : P ⊆ K) :
    NormalizedCell.measure (uniformMeasure K) P = uniformMeasure P := by
…
```
Mentions: OAI.Problem358.NormalizedCell.measure

theorem OAI.Problem358.uniformMeasure_real_cell line 213

Source documentation

Cell mass for a uniform source is the ratio of cell and source volume.

theorem uniformMeasure_real_cell {d : ℕ} {K P : Set (E d)}
    (hP : MeasurableSet P) (hPK : P ⊆ K) :
    (uniformMeasure K).real P = (volume P).toReal / (volume K).toReal := by
…

theorem OAI.Problem358.CellGeometry.uniformMass_eq_normalized_integral_one line 236
Source documentation
A closed-cell mass is the normalized scalar volume integral used by the moving-cut calculus. No positivity or distinct-site hypothesis is needed.
```
theorem uniformMass_eq_normalized_integral_one
    {K : Set (E d)} (hK : IsClosed K)
    (y : ι → E d) (c : ι → ℝ) (i : ι) :
    (uniformMeasure K).real (closedCell K y c i) =
      (volume K).toReal⁻¹ * ∫ _x in closedCell K y c i, (1 : ℝ) := by
…
```
Mentions: OAI.Problem358.CellGeometry.closedCell

theorem OAI.Problem358.CellGeometry.integral_uniform_closedCell line 249

Source documentation

The uniform restriction on a cell rescales its volume integral. This also holds for nonscalar moments and for degenerate source volume.

theorem integral_uniform_closedCell
    {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
    (K : Set (E d)) (y : ι → E d) (c : ι → ℝ) (i : ι)
    (f : E d → V) :
    (∫ x in closedCell K y c i, f x ∂uniformMeasure K) =
      (volume K).toReal⁻¹ • ∫ x in closedCell K y c i, f x := by
…

Mentions: OAI.Problem358.CellGeometry.closedCell

theorem OAI.Problem358.CellGeometry.hasDerivAt_uniformMass_of_integral_one line 261

Source documentation

A scalar moving-volume derivative immediately gives the actual normalized real cell-mass derivative.

theorem hasDerivAt_uniformMass_of_integral_one
    {K : Set (E d)} (hK : IsClosed K)
    (y : ℝ → ι → E d) (c : ℝ → ι → ℝ) (i : ι) {t D : ℝ}
    (hD : HasDerivAt (fun s => ∫ _x in closedCell K (y s) (c s) i, (1 : ℝ)) D t) :
    HasDerivAt (fun s => (uniformMeasure K).real (closedCell K (y s) (c s) i))
      ((volume K).toReal⁻¹ * D) t := by
…

Mentions: OAI.Problem358.CellGeometry.closedCell

theorem OAI.Problem358.CellGeometry.hasFDerivAt_uniformMass_of_integral_one line 272

Source documentation

The same normalization bridge for a Fréchet derivative in an arbitrary real normed parameter space.

theorem hasFDerivAt_uniformMass_of_integral_one
    {P : Type*} [NormedAddCommGroup P] [NormedSpace ℝ P]
    {K : Set (E d)} (hK : IsClosed K)
    (y : P → ι → E d) (c : P → ι → ℝ) (i : ι) {p : P} {D : P →L[ℝ] ℝ}
    (hD : HasFDerivAt (fun q => ∫ _x in closedCell K (y q) (c q) i, (1 : ℝ)) D p) :
    HasFDerivAt (fun q => (uniformMeasure K).real (closedCell K (y q) (c q) i))
      ((volume K).toReal⁻¹ • D) p := by
…

Mentions: OAI.Problem358.CellGeometry.closedCell

theorem OAI.Problem358.CellGeometry.hasStrictFDerivAt_uniformMass_of_integral_one line 284

Source documentation

Strict differentiability is preserved by the fixed source normalization, as required by the implicit-function theorem.

theorem hasStrictFDerivAt_uniformMass_of_integral_one
    {P : Type*} [NormedAddCommGroup P] [NormedSpace ℝ P]
    {K : Set (E d)} (hK : IsClosed K)
    (y : P → ι → E d) (c : P → ι → ℝ) (i : ι) {p : P} {D : P →L[ℝ] ℝ}
    (hD : HasStrictFDerivAt
      (fun q => ∫ _x in closedCell K (y q) (c q) i, (1 : ℝ)) D p) :
    HasStrictFDerivAt
      (fun q => (uniformMeasure K).real (closedCell K (y q) (c q) i))
      ((volume K).toReal⁻¹ • D) p := by
…

Mentions: OAI.Problem358.CellGeometry.closedCell

theorem OAI.Problem358.CellVectorDerivative.integral_coordinate line 314

Source documentation

A coordinate of a Bochner integral in the problem's Euclidean space.

theorem integral_coordinate {X : Type*} [MeasurableSpace X]
    {μ : Measure X} {f : X → E d} (hf : Integrable f μ) (k : Fin d) :
    (∫ x, f x ∂μ) k = ∫ x, f x k ∂μ :=
…

theorem OAI.Problem358.CellVectorDerivative.hasDerivAt_of_coordinates line 320
Source documentation
Assemble scalar coordinate derivatives in the Euclidean, rather than sup, norm.
```
theorem hasDerivAt_of_coordinates {f : ℝ → E d} {b : E d} {t : ℝ}
    (h : ∀ k : Fin d, HasDerivAt (fun s => f s k) (b k) t) :
    HasDerivAt f b t := by
…
```

theorem OAI.Problem358.CellVectorDerivative.setIntegral_uniformMeasure line 330

Source documentation

Restriction to a subset of the source removes the extra source indicator. This identity is valid even in the zero-volume degenerate case.

theorem setIntegral_uniformMeasure {V : Type*} [NormedAddCommGroup V]
    [NormedSpace ℝ V] {K P : Set (E d)} (hPK : P ⊆ K) (f : E d → V) :
    (∫ x in P, f x ∂uniformMeasure K) =
      (volume K).toReal⁻¹ • ∫ x in P, f x ∂volume := by
…

theorem OAI.Problem358.CellVectorDerivative.hasDerivAt_uniform_cellMoment_of_coordinates line 339

Source documentation

Scalar volume derivatives of the coordinate weights give the actual uniform-source vector-moment derivative, with the source normalization explicit.

theorem hasDerivAt_uniform_cellMoment_of_coordinates
    {ι : Type*} {K : Set (E d)} (hK : IsCompact K)
    (y : ℝ → ι → E d) (c : ℝ → ι → ℝ) (i : ι) {t : ℝ} {b : E d}
    (h : ∀ k : Fin d, HasDerivAt
      (fun s => ∫ x in CellGeometry.closedCell K (y s) (c s) i, x k ∂volume)
      (b k) t) :
    HasDerivAt
      (fun s => ∫ x in CellGeometry.closedCell K (y s) (c s) i, x ∂uniformMeasure K)
      ((volume K).toReal⁻¹ • b) t := by
…

Mentions: OAI.Problem358.CellGeometry.closedCell

theorem OAI.Problem358.CellVectorDerivative.hasDerivAt_uniform_cellMass line 363

Source documentation

Normalize the scalar cell-mass derivative using the same source factor.

theorem hasDerivAt_uniform_cellMass
    {ι : Type*} {K : Set (E d)} (hK : IsCompact K)
    (y : ℝ → ι → E d) (c : ℝ → ι → ℝ) (i : ι) {t a : ℝ}
    (h : HasDerivAt
      (fun s => (volume (CellGeometry.closedCell K (y s) (c s) i)).toReal) a t) :
    HasDerivAt
      (fun s => (uniformMeasure K).real (CellGeometry.closedCell K (y s) (c s) i))
      (a / (volume K).toReal) t := by
…

Mentions: OAI.Problem358.CellGeometry.closedCell

theorem OAI.Problem358.CellVectorDerivative.coordinate_sum_integral_smul line 376

Source documentation

Coordinate formula for a finite sum of weighted vector surface moments.

theorem coordinate_sum_integral_smul {ι : Type*} [Fintype ι] {X : ι → Type*} [∀ j, MeasurableSpace (X j)]
    (μ : ∀ j, Measure (X j)) (z : ∀ j, X j → E d) (w : ∀ j, X j → ℝ)
    (hw : ∀ j, Integrable (fun x => w j x • z j x) (μ j)) (k : Fin d) :
    (∑ j, ∫ x, w j x • z j x ∂μ j) k =
      ∑ j, ∫ x, w j x * z j x k ∂μ j := by
…

theorem OAI.Problem358.CellVectorDerivative.hasDerivAt_uniform_cellMoment_of_faces line 389

Source documentation

The scalar face formulas for every coordinate assemble into the vector face formula; integrability of the actual surface integrands is the only extra input.

theorem hasDerivAt_uniform_cellMoment_of_faces
    {ι κ : Type*} [Fintype κ] {X : κ → Type*} [∀ j, MeasurableSpace (X j)]
    {K : Set (E d)} (hK : IsCompact K)
    (y : ℝ → ι → E d) (c : ℝ → ι → ℝ) (i : ι) {t : ℝ}
    (μ : ∀ j, Measure (X j)) (z : ∀ j, X j → E d) (w : ∀ j, X j → ℝ)
    (hw : ∀ j, Integrable (fun x => w j x • z j x) (μ j))
    (h : ∀ k : Fin d, HasDerivAt
      (fun s => ∫ x in CellGeometry.closedCell K (y s) (c s) i, x k ∂volume)
      (∑ j, ∫ x, w j x * z j x k ∂μ j) t) :
    HasDerivAt
      (fun s => ∫ x in CellGeometry.closedCell K (y s) (c s) i, x ∂uniformMeasure K)
      ((volume K).toReal⁻¹ • ∑ j, ∫ x, w j x • z j x ∂μ j) t := by
…

Mentions: OAI.Problem358.CellGeometry.closedCell

theorem OAI.Problem358.CellVectorDerivative.normalized_stationary_face_sum line 408

Source documentation

Separate the stationary intercept speed from normalized vector face moments. No nonzero denominator assumptions are needed for this algebraic identity.

theorem normalized_stationary_face_sum
    {κ : Type*} [Fintype κ] {X : κ → Type*} [∀ j, MeasurableSpace (X j)]
    (μ : ∀ j, Measure (X j)) (z : ∀ j, X j → E d)
    (M : ℝ) (a q : κ → ℝ) :
    M⁻¹ • (∑ j, ∫ x, (q j / a j) • z j x ∂μ j) =
      ∑ j, q j • ((M * a j)⁻¹ • ∫ x, z j x ∂μ j) := by
…

theorem OAI.Problem358.CellVectorDerivative.hasDerivAt_uniform_cellMoment_stationary line 423

Source documentation

Convenient stationary-direction form, ready for the canonical face coefficient b_ij = (volume(K) * normalLength_ij)⁻¹ • firstMoment_ij.

theorem hasDerivAt_uniform_cellMoment_stationary
    {ι κ : Type*} [Fintype κ] {X : κ → Type*} [∀ j, MeasurableSpace (X j)]
    {K : Set (E d)} (hK : IsCompact K)
    (y : ι → E d) (c q : ι → ℝ) (i : ι)
    (μ : ∀ j, Measure (X j)) (z : ∀ j, X j → E d)
    (a r : κ → ℝ) (hz : ∀ j, Integrable (z j) (μ j))
    (h : ∀ k : Fin d, HasDerivAt
      (fun s => ∫ x in CellGeometry.closedCell K y (fun j => c j + s * q j) i,
        x k ∂volume)
      (∑ j, ∫ x, (r j / a j) * z j x k ∂μ j) 0) :
    HasDerivAt
      (fun s => ∫ x in CellGeometry.closedCell K y (fun j => c j + s * q j) i,
…

Mentions: OAI.Problem358.CellGeometry.closedCell