High-contrast homogenization: Provider.Recurrence.AdaptedPartitionAverage

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Averages over a partition up to a null set

e.fixed.geometry.parent.child weights the cells of a partition of U by |U_i| / |U|, and the aligned subdivision of the coarse block is a partition only up to a null set — the adapted cubes are open, so their union omits the interior faces. This file records what that costs: nothing.

The integral of an integrable function over the parent is the sum of the integrals over the cells, because the parent and the union of the cells differ by a null set and the cells are pairwise disjoint measurable sets; the same argument with the constant function one gives |U| = Σ |U_i|, so the weights |U_i| / |U| sum to one and the average over the parent is the weighted average of the averages over the cells.

Integrals over a partition up to a null set

theorem HCPolySupport.HighContrast.Recurrence.ae_eq_iUnion_of_aePartition {d : ℕ} {ι : Type u_1} {U : Set (Vec d)} {Z : Finset ι} {c : ι → Set (Vec d)} (hsub : ∀ i ∈ Z, c i ⊆ U) (hnull : MeasureTheory.volume (U \ ⋃ i ∈ ↑Z, c i) = 0) : U =ᵐ[MeasureTheory.volume] ⋃ i ∈ ↑Z, c i

The parent set and the union of the cells of a partition up to a null set agree almost everywhere.

theorem HCPolySupport.HighContrast.Recurrence.setIntegral_eq_sum_of_aePartition {d : ℕ} {ι : Type u_1} {U : Set (Vec d)} {Z : Finset ι} {c : ι → Set (Vec d)} {g : Vec d → ℝ} (hmeas : ∀ i ∈ Z, MeasurableSet (c i)) (hsub : ∀ i ∈ Z, c i ⊆ U) (hdisj : (↑Z).PairwiseDisjoint c) (hnull : MeasureTheory.volume (U \ ⋃ i ∈ ↑Z, c i) = 0) (hint : MeasureTheory.IntegrableOn g U MeasureTheory.volume) : ∫ (x : Vec d) in U, g x = ∑ i ∈ Z, ∫ (x : Vec d) in c i, g x

The integral over the parent is the sum of the integrals over the cells, for a finite family of pairwise disjoint measurable subsets covering the parent up to a null set.

theorem HCPolySupport.HighContrast.Recurrence.measure_eq_sum_of_aePartition {d : ℕ} {ι : Type u_1} {U : Set (Vec d)} {Z : Finset ι} {c : ι → Set (Vec d)} (hmeas : ∀ i ∈ Z, MeasurableSet (c i)) (hsub : ∀ i ∈ Z, c i ⊆ U) (hdisj : (↑Z).PairwiseDisjoint c) (hnull : MeasureTheory.volume (U \ ⋃ i ∈ ↑Z, c i) = 0) : MeasureTheory.volume U = ∑ i ∈ Z, MeasureTheory.volume (c i)

The volume of the parent is the sum of the volumes of the cells.

Averages over a partition

theorem HCPolySupport.HighContrast.Recurrence.measure_cell_ne_top_of_subset {d : ℕ} {U V : Set (Vec d)} (hUtop : MeasureTheory.volume U ≠ ⊤) (hsub : V ⊆ U) : MeasureTheory.volume V ≠ ⊤

The cells of a partition of a set of finite volume have finite volume.

theorem HCPolySupport.HighContrast.Recurrence.sum_weight_eq_one_of_aePartition {d : ℕ} {ι : Type u_1} {U : Set (Vec d)} {Z : Finset ι} {c : ι → Set (Vec d)} (hmeas : ∀ i ∈ Z, MeasurableSet (c i)) (hsub : ∀ i ∈ Z, c i ⊆ U) (hdisj : (↑Z).PairwiseDisjoint c) (hnull : MeasureTheory.volume (U \ ⋃ i ∈ ↑Z, c i) = 0) (hU0 : MeasureTheory.volume U ≠ 0) (hUtop : MeasureTheory.volume U ≠ ⊤) : ∑ i ∈ Z, (MeasureTheory.volume (c i)).toReal / (MeasureTheory.volume U).toReal = 1

The weights |U_i| / |U| of e.fixed.geometry.parent.child sum to one.

theorem HCPolySupport.HighContrast.Recurrence.volumeAverage_eq_sum_weight_of_aePartition {d : ℕ} {ι : Type u_1} {U : Set (Vec d)} {Z : Finset ι} {c : ι → Set (Vec d)} {g : Vec d → ℝ} (hmeas : ∀ i ∈ Z, MeasurableSet (c i)) (hsub : ∀ i ∈ Z, c i ⊆ U) (hdisj : (↑Z).PairwiseDisjoint c) (hnull : MeasureTheory.volume (U \ ⋃ i ∈ ↑Z, c i) = 0) (hint : MeasureTheory.IntegrableOn g U MeasureTheory.volume) (hcell0 : ∀ i ∈ Z, MeasureTheory.volume (c i) ≠ 0) (hUtop : MeasureTheory.volume U ≠ ⊤) : volumeAverage U g = ∑ i ∈ Z, (MeasureTheory.volume (c i)).toReal / (MeasureTheory.volume U).toReal * volumeAverage (c i) g

The average over the parent is the weighted average of the averages over the cells, with the weights |U_i| / |U| of e.fixed.geometry.parent.child.