ReferenceChart.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Area-preserving reference-line coordinates for a top.

def OAI.LipschitzHilbert.SlopeBox.referenceChart line 14
theorem OAI.LipschitzHilbert.SlopeBox.referenceChart_measurePreserving line 26
theorem OAI.LipschitzHilbert.SlopeBox.referenceChart_image_measure line 32
theorem OAI.LipschitzHilbert.SlopeBox.referenceChart_inverse_transverse line 38
theorem OAI.LipschitzHilbert.SlopeBox.referenceChart_linePoint line 47
Source documentation
A horizontal line in reference coordinates is the actual line through the physical evaluation point in the reference direction.
```
theorem referenceChart_linePoint (T : SlopeBox) (z : ℝ × ℝ) (x : ℝ) :
    T.referenceChart (x, (T.referenceChart.symm z).2) =
      LipschitzHilbert.linePoint T.slope z x := by
…
```
Mentions: OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.linePoint
def OAI.LipschitzHilbert.SlopeBox.referenceRectangle line 56
theorem OAI.LipschitzHilbert.SlopeBox.significant_mem_referenceRectangle line 60
Source documentation
Every significant point lies in the fixed reference rectangle.
```
theorem significant_mem_referenceRectangle (T : SlopeBox) {K : ℝ} {z : ℝ × ℝ}
    (hz : T.radius z ≤ K) : T.referenceChart.symm z ∈ T.referenceRectangle K := by
…
```
Mentions: OAI.LipschitzHilbert.SlopeBox