Discrepancy.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceSampling_phase_length line 14
Source documentation
Every constructed power is long enough for density at most two on every coordinate in the sampling prefix.
```
theorem sourceSampling_phase_length (s : ℕ) (hs : 200000 ≤ sourceBlockSize s)
    (i : SourceCoordinate) (hi : i.1 ≤ s) (n : ℤ) (hn : n ∈ sourceSamplingPowers s) :
    1 ≤ (n : ℝ)*sourceAngleUnit i := by
…
```
Mentions: OAI.FiniteFactor.sourceBlockSize, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingPowers, OAI.FiniteFactor.sourceAngleUnit
theorem OAI.FiniteFactor.sourceSampling_phase_domination line 35
theorem OAI.FiniteFactor.samplingCharacter_pair_expression line 56

theorem OAI.FiniteFactor.sourceSampling_rectangle_bound line 66

Source documentation

Rectangle discrepancy for the actual pair law of the deterministic selected powers, with every probabilistic hypothesis discharged.

theorem sourceSampling_rectangle_bound (s : ℕ) (hs : 200000 ≤ sourceBlockSize s)
    (i : SourceCoordinate) (hi : i.1 ≤ s) (n n' : ℤ)
    (hn : n ∈ sourceSamplingPowers s) (hn' : n' ∈ sourceSamplingPowers s) (hne : n ≠ n')
    (a b a' b' : ℝ) :
    |(sourceAngleLaw {θ | Int.fract ((n : ℝ)*θ i) ∈ Set.Icc a b ∧
        Int.fract ((n' : ℝ)*θ i) ∈ Set.Icc a' b'}).toReal -
      (unitIntervalMeasure (Set.Icc a b)).toReal*(unitIntervalMeasure (Set.Icc a' b')).toReal| ≤
      26*(sourceBlockSize s : ℝ)^(-80 : ℝ) := by
…

Mentions: OAI.FiniteFactor.sourceBlockSize, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingPowers, OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.unitIntervalMeasure