TriangleLaw.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.samplingWeight_triangular_order line 12
Source documentation
The actual triangular phase weight is precisely the order indicator of the rotated endpoint, on the Haar representatives.
```
theorem samplingWeight_triangular_order (h α s t : ℝ)
    (hs : s ∈ Set.Ico (0 : ℝ) 1) (ht : t ∈ Set.Ico (0 : ℝ) 1) :
    samplingWeight true h α s t = if s < Int.fract (s+t) then 1 else 0 := by
…
```
Mentions: OAI.FiniteFactor.samplingWeight
theorem OAI.FiniteFactor.samplingTestedFirstDensity_triangular_section line 30
Source documentation
The first tested triangular density is its actual vertical section of Lebesgue measure on 0≤x<y<1. No triangular marginal identity is assumed.
```
theorem samplingTestedFirstDensity_triangular_section (h α s : ℝ) (E G : Set ℝ)
    (hG : MeasurableSet G) (hs : s ∈ Set.Ico (0 : ℝ) 1) :
    samplingTestedFirstDensity true h α E G s =
      ∫ y, (if s ∈ E ∧ y ∈ G ∧ s < y then (1 : ℝ) else 0) ∂unitIntervalMeasure := by
…
```
Mentions: OAI.FiniteFactor.samplingTestedFirstDensity, OAI.FiniteFactor.unitIntervalMeasure

theorem OAI.FiniteFactor.samplingTestedFirstDensity_triangular_mass line 55

Source documentation

The two-dimensional tested source integral equals the genuine triangular restriction of product Lebesgue measure.

theorem samplingTestedFirstDensity_triangular_mass (h α : ℝ) (E G : Set ℝ)
    (hE : MeasurableSet E) (hG : MeasurableSet G) :
    (∫ s, samplingTestedFirstDensity true h α E G s ∂unitIntervalMeasure) =
      ((unitIntervalMeasure.prod unitIntervalMeasure)
        {p : ℝ × ℝ | p.1 ∈ E ∧ p.2 ∈ G ∧ p.1 < p.2}).toReal := by
…

Mentions: OAI.FiniteFactor.samplingTestedFirstDensity, OAI.FiniteFactor.unitIntervalMeasure