CoordinateMass.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.unitIntervalMeasure_right_tail line 12
Source documentation
Endpoint tails of the original Haar representative have at most their interval length; the endpoint singleton conventions cause no extra mass.
```
theorem unitIntervalMeasure_right_tail (a : ℝ) :
    unitIntervalMeasure (Set.Ici (1-a)) ≤ ENNReal.ofReal a := by
…
```
Mentions: OAI.FiniteFactor.unitIntervalMeasure
theorem OAI.FiniteFactor.unitIntervalMeasure_left_tail line 19
theorem OAI.FiniteFactor.CouplingParameters.labelledCoupling_label line 28
theorem OAI.FiniteFactor.CouplingParameters.labelledEndpoint_set_le_ten line 42
Source documentation
The actual one-coordinate endpoint law is dominated by ten times Haar.
```
theorem labelledEndpoint_set_le_ten (p : CouplingParameters) (b : Bool)
    (A : Set ℝ) (hA : MeasurableSet A) :
    p.labelledCoupling ((fun z => endpoint b z.2) ⁻¹' A) ≤ 10*unitIntervalMeasure A := by
…
```
Mentions: OAI.FiniteFactor.CouplingParameters, OAI.FiniteFactor.CouplingParameters.endpoint, OAI.FiniteFactor.unitIntervalMeasure
theorem OAI.FiniteFactor.CouplingParameters.labelledCoupling_right_tail line 54
theorem OAI.FiniteFactor.CouplingParameters.labelledCoupling_left_tail line 61