High-contrast homogenization: Provider.Response.DiagonalWeakNormPartition

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

Equal-weight averages on an aligned subdivision

The aligned children of an adapted cell have equal volume and cover their parent up to a null set. Consequently the average over the parent is the ordinary normalized finite average of the child averages. This is the partition identity used before the finite variance estimate in the weak-norm estimate for the optimizer state.

theorem HCPolySupport.HighContrast.Response.avsum_volumeAverage_adaptedCellAt_eq {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) {g : Vec d → ℝ} (hg : MeasureTheory.IntegrableOn g (adaptedCell q t) MeasureTheory.volume) : (avsum (alignedIndex q k t) fun (w : Fin d → ℤ) => volumeAverage (adaptedCellAt q k w) g) = volumeAverage (adaptedCell q t) g

The average over an adapted parent is the normalized average of the child averages.

theorem HCPolySupport.HighContrast.Response.blockCellAverage_adaptedCell_eq_avsum {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) {F : Vec d → BlockVec d} (hF₁ : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (x : Vec d) => (F x).1 i) (adaptedCell q t) MeasureTheory.volume) (hF₂ : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (x : Vec d) => (F x).2 i) (adaptedCell q t) MeasureTheory.volume) : blockCellAverage (adaptedCell q t) F = (fun (i : Fin d) => avsum (alignedIndex q k t) fun (w : Fin d → ℤ) => (blockCellAverage (adaptedCellAt q k w) F).1 i, fun (i : Fin d) => avsum (alignedIndex q k t) fun (w : Fin d → ℤ) => (blockCellAverage (adaptedCellAt q k w) F).2 i)

The doubled parent average is the normalized sum of the child averages.