OAI/Analysis/LipschitzHilbert/Estimates/HorizontalDilation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact product-measure dilation in the horizontal coordinate.

  1. def OAI.LipschitzHilbert.horizontalDilation line 13
  2. theorem OAI.LipschitzHilbert.horizontalDilation_apply line 25
  3. theorem OAI.LipschitzHilbert.map_horizontalDilation line 28
  4. theorem OAI.LipschitzHilbert.integral_horizontalDilation line 38
  5. theorem OAI.LipschitzHilbert.measure_horizontalDilation_preimage line 45
  6. def OAI.LipschitzHilbert.referenceHorizontalDilation line 53

    Source documentation

    The same horizontal scaling in the reference packet convention (y,x).

    def referenceHorizontalDilation (r : ℝ) (hr : r ≠ 0) : (ℝ × ℝ) ≃ᵐ (ℝ × ℝ) where
…
  7. theorem OAI.LipschitzHilbert.map_referenceHorizontalDilation line 65
  8. theorem OAI.LipschitzHilbert.integral_referenceHorizontalDilation line 75