Periodization.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.fract_interval_lower line 14
Source documentation
Lower counterpart to periodized interval domination; the floor-length subinterval contributes exact Haar measure.
```
theorem fract_interval_lower (a b : ℝ) (hab : a < b) :
    ENNReal.ofReal (1-1/(b-a)) • unitIntervalMeasure ≤
      (cond volume (Set.Ioc a b)).map Int.fract := by
…
```
Mentions: OAI.FiniteFactor.unitIntervalMeasure

theorem OAI.FiniteFactor.sourceAngle_phase_sandwich line 47

Source documentation

Two-sided near-uniformity for the actual single-phase law, on every Borel set. The error is exactly 1/(n times the source interval length).

theorem sourceAngle_phase_sandwich (i : SourceCoordinate) (n : ℝ) (hn : 0 < n) :
    ENNReal.ofReal (1-1/(n*sourceAngleUnit i)) • unitIntervalMeasure ≤
      (sourceAngleMarginal i).map (fun t => Int.fract (n*t)) ∧
    (sourceAngleMarginal i).map (fun t => Int.fract (n*t)) ≤
      ENNReal.ofReal (1+1/(n*sourceAngleUnit i)) • unitIntervalMeasure := by
…

Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceAngleUnit, OAI.FiniteFactor.unitIntervalMeasure, OAI.FiniteFactor.sourceAngleMarginal

theorem OAI.FiniteFactor.integral_error_of_measure_sandwich line 67

Source documentation

Nonnegative tests inherit the exact relative error from a measure sandwich.

theorem integral_error_of_measure_sandwich {α : Type*} [MeasurableSpace α]
    (μ ν : Measure α) (ε : ℝ) (hε : 0 ≤ ε) (hε1 : ε ≤ 1)
    (hlo : ENNReal.ofReal (1-ε) • μ ≤ ν)
    (hhi : ν ≤ ENNReal.ofReal (1+ε) • μ)
    (g : α → ℝ) (hg : ∀ x, 0 ≤ g x) (hgi : Integrable g μ) :
    Integrable g ν ∧ |(∫ x, g x ∂ν) - ∫ x, g x ∂μ| ≤ ε * ∫ x, g x ∂μ := by
…

theorem OAI.FiniteFactor.sourceAngle_single_phase_test line 84

Source documentation

The source's single-phase test estimate for all integrable nonnegative weights, not merely for rectangle indicators.

theorem sourceAngle_single_phase_test (i : SourceCoordinate) (n : ℝ) (hn : 0 < n)
    (hlen : 1 ≤ n*sourceAngleUnit i) (g : ℝ → ℝ)
    (hg : ∀ x, 0 ≤ g x) (hgm : Measurable g) (hgi : Integrable g unitIntervalMeasure) :
    |(∫ t, g (Int.fract (n*t)) ∂sourceAngleMarginal i) -
        ∫ t, g t ∂unitIntervalMeasure| ≤
      (1/(n*sourceAngleUnit i)) * ∫ t, g t ∂unitIntervalMeasure := by
…

Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceAngleUnit, OAI.FiniteFactor.unitIntervalMeasure, OAI.FiniteFactor.sourceAngleMarginal