High-contrast homogenization: Entry.Geometry.AffineGridDistortion

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

Relative distortion of two adapted grids

For two invertible adapted grids with gridRatio q q' ≤ K₀, the relative matrices q⁻¹*q' and q'⁻¹*q have operator norm at most K₀; this yields two-sided determinant and adapted-cell volume comparison, a relative inverse-norm bound used for the flat-face strips, and exact cancellation of the affine Jacobian in ratios, with no absolute norm bound on either grid. These are the relative cell-volume and inverse-norm estimates behind l.two.grid.whitney and the relative operator-norm control in the fixed old-coordinate enlargement of p.two.grid.transport.

theorem HCPolySupport.HighContrast.Geometry.norm_inv_mul_le_gridRatio_of_le {d : ℕ} {q q' : Mat d} {K₀ : ℝ} (hd : 2 ≤ d) (hK : gridRatio q q' ≤ K₀) : ‖q⁻¹ * q'‖ ≤ K₀

theorem HCPolySupport.HighContrast.Geometry.norm_inv_mul_comm_le_gridRatio_of_le {d : ℕ} {q q' : Mat d} {K₀ : ℝ} (hd : 2 ≤ d) (hK : gridRatio q q' ≤ K₀) : ‖q'⁻¹ * q‖ ≤ K₀

theorem HCPolySupport.HighContrast.Geometry.vecNormSq_relative_comm_le_gridRatio {d : ℕ} {q q' : Mat d} {K₀ : ℝ} (hd : 2 ≤ d) (hK : gridRatio q q' ≤ K₀) (v : Vec d) : vecNormSq ((q'⁻¹ * q).mulVec v) ≤ K₀ ^ 2 * vecNormSq v

theorem HCPolySupport.HighContrast.Geometry.abs_entry_le_opNorm {d : ℕ} (A : Mat d) (i j : Fin d) : |A i j| ≤ ‖A‖

theorem HCPolySupport.HighContrast.Geometry.abs_det_le_factorial_mul_opNorm_pow {d : ℕ} (A : Mat d) : |Matrix.det A| ≤ ↑d.factorial * ‖A‖ ^ d

theorem HCPolySupport.HighContrast.Geometry.abs_det_inv_mul_le_gridRatio_of_le {d : ℕ} {q q' : Mat d} {K₀ : ℝ} (hd : 2 ≤ d) (hK : gridRatio q q' ≤ K₀) : |(q⁻¹ * q').det| ≤ ↑d.factorial * K₀ ^ d

theorem HCPolySupport.HighContrast.Geometry.abs_det_inv_mul_comm_le_gridRatio_of_le {d : ℕ} {q q' : Mat d} {K₀ : ℝ} (hd : 2 ≤ d) (hK : gridRatio q q' ≤ K₀) : |(q'⁻¹ * q).det| ≤ ↑d.factorial * K₀ ^ d

theorem HCPolySupport.HighContrast.Geometry.abs_det_div_eq_abs_det_inv_mul_left {d : ℕ} {q q' : Mat d} (hq : IsUnit q) : |Matrix.det q'| / |Matrix.det q| = |(q⁻¹ * q').det|

theorem HCPolySupport.HighContrast.Geometry.abs_det_div_eq_abs_det_inv_mul_right {d : ℕ} {q q' : Mat d} (hq' : IsUnit q') : |Matrix.det q| / |Matrix.det q'| = |(q'⁻¹ * q).det|

theorem HCPolySupport.HighContrast.Geometry.abs_det_ratio_le_gridRatio_of_le_left {d : ℕ} {q q' : Mat d} {K₀ : ℝ} (hd : 2 ≤ d) (hq : IsUnit q) (hK : gridRatio q q' ≤ K₀) : |Matrix.det q'| / |Matrix.det q| ≤ ↑d.factorial * K₀ ^ d

theorem HCPolySupport.HighContrast.Geometry.abs_det_ratio_le_gridRatio_of_le_right {d : ℕ} {q q' : Mat d} {K₀ : ℝ} (hd : 2 ≤ d) (hq' : IsUnit q') (hK : gridRatio q q' ≤ K₀) : |Matrix.det q| / |Matrix.det q'| ≤ ↑d.factorial * K₀ ^ d

theorem HCPolySupport.HighContrast.Geometry.volume_adaptedCell {d : ℕ} (q : Mat d) (r : ℤ) : MeasureTheory.volume (adaptedCell q r) = ENNReal.ofReal |Matrix.det q| * ENNReal.ofReal (3 ^ r) ^ d

theorem HCPolySupport.HighContrast.Geometry.volume_adaptedCell_toReal {d : ℕ} (q : Mat d) (r : ℤ) : (MeasureTheory.volume (adaptedCell q r)).toReal = |Matrix.det q| * (3 ^ r) ^ d

theorem HCPolySupport.HighContrast.Geometry.volume_adaptedCellTranslate_toReal {d : ℕ} (q : Mat d) (j : ℤ) (y : Vec d) : (MeasureTheory.volume (adaptedCellTranslate q j y)).toReal = |Matrix.det q| * (3 ^ j) ^ d

theorem HCPolySupport.HighContrast.Geometry.triadic_volume_scale_ratio (d : ℕ) (j r : ℤ) : (3 ^ r) ^ d / (3 ^ j) ^ d = 3 ^ (-↑d * (↑j - ↑r))

theorem HCPolySupport.HighContrast.Geometry.adaptedCell_volume_ratio_eq {d : ℕ} {q q' : Mat d} (hq' : IsUnit q') (j r : ℤ) (y : Vec d) : (MeasureTheory.volume (adaptedCell q r)).toReal / (MeasureTheory.volume (adaptedCellTranslate q' j y)).toReal = |Matrix.det q| / |Matrix.det q'| * 3 ^ (-↑d * (↑j - ↑r))

theorem HCPolySupport.HighContrast.Geometry.adaptedCell_volume_ratio_two_sided_of_gridRatio {d : ℕ} {q q' : Mat d} {K₀ : ℝ} (hd : 2 ≤ d) (hK₀ : 1 ≤ K₀) (hq : IsUnit q) (hq' : IsUnit q') (hK : gridRatio q q' ≤ K₀) (j r : ℤ) (y : Vec d) : have Cdet := ↑d.factorial * K₀ ^ d; Cdet⁻¹ * 3 ^ (-↑d * (↑j - ↑r)) ≤ (MeasureTheory.volume (adaptedCell q r)).toReal / (MeasureTheory.volume (adaptedCellTranslate q' j y)).toReal ∧ (MeasureTheory.volume (adaptedCell q r)).toReal / (MeasureTheory.volume (adaptedCellTranslate q' j y)).toReal ≤ Cdet * 3 ^ (-↑d * (↑j - ↑r))

theorem HCPolySupport.HighContrast.Geometry.inverseNormLE_relative_of_gridRatio {d : ℕ} {q q' : Mat d} {K₀ : ℝ} (hd : 2 ≤ d) (hq : IsUnit q) (hq' : IsUnit q') (hK : gridRatio q q' ≤ K₀) : InverseNormLE (q⁻¹ * q') K₀

Relative inverse control in the squared Euclidean norm used by the strip theorem.

theorem HCPolySupport.HighContrast.Geometry.adaptedCell_relVolume_eq_standard_preimage {d : ℕ} {q q' : Mat d} (hq : IsUnit q) (hq' : IsUnit q') (j r : ℤ) (y : Vec d) (w : Fin d → ℤ) : (MeasureTheory.volume (adaptedCell q r)).toReal / (MeasureTheory.volume (adaptedCellTranslate q' j y)).toReal = (MeasureTheory.volume (standardCell d r w)).toReal / (MeasureTheory.volume (adaptedCellTranslate (q⁻¹ * q') j (matVecMul q⁻¹ y))).toReal

The Jacobian cancels in the relative volume of a cell and the affine target.