High-contrast homogenization: Provider.Response.CutoffAdaptedMean

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

Mean normalization after adapted linear transport

The determinant factor in the integral and the volume of the adapted cell is the same, so the normalized mean is unchanged by the grid transformation.

theorem HCPolySupport.HighContrast.Response.setIntegral_adaptedCell_comp_inv {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (ψ : Vec d → ℝ) : ∫ (x : Vec d) in adaptedCell q t, ψ (matVecMul q⁻¹ x) = |Matrix.det q| * ∫ (y : Vec d) in centeredCube d t, ψ y

Linear change of variables from the centered cube to its adapted image.

theorem HCPolySupport.HighContrast.Response.volume_adaptedCell_toReal {d : ℕ} {q : Mat d} (t : ℤ) : (MeasureTheory.volume (adaptedCell q t)).toReal = |Matrix.det q| * (MeasureTheory.volume (centeredCube d t)).toReal

The real volume of an adapted cell is the determinant times that of its centered reference cube.

theorem HCPolySupport.HighContrast.Response.setIntegral_adaptedCellAt_eq_det_mul {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) (w : Fin d → ℤ) (φ : Vec d → ℝ) : ∫ (x : Vec d) in adaptedCellAt q k w, φ x = |Matrix.det q| * ∫ (y : Vec d) in standardCell d k w, φ (matVecMul q y)

Linear change of variables from a standard aligned cube to its physical adapted image.

theorem HCPolySupport.HighContrast.Response.volume_adaptedCellAt_toReal {d : ℕ} (q : Mat d) (k : ℤ) (w : Fin d → ℤ) : (MeasureTheory.volume (adaptedCellAt q k w)).toReal = |Matrix.det q| * (MeasureTheory.volume (standardCell d k w)).toReal

The real volume of an aligned adapted cell is the determinant times the volume of its standard reference cube.

theorem HCPolySupport.HighContrast.Response.volumeAverage_adaptedCellAt_eq_cubeAverage_pullback {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) (w : Fin d → ℤ) (φ : Vec d → ℝ) : volumeAverage (adaptedCellAt q k w) φ = cubeAverage (translateCube w (originCube d k)) fun (y : Vec d) => φ (matVecMul q y)

Normalized physical averages on aligned adapted cells equal ordinary cube averages after pullback by the grid matrix.

theorem HCPolySupport.HighContrast.Response.volumeAverage_adaptedPreYoungCutoff_eq_one {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) : volumeAverage (adaptedCell q t) (adaptedPreYoungCutoff q hq t) = 1

The adapted cutoff has normalized mean one on the physical adapted cell.