PhaseMarginal.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.unitInterval_middle_compl line 11
theorem OAI.FiniteFactor.sourceAngle_positive_phase_domination line 32
Source documentation
The actual source-angle phase law has density at most five in the second phase range. This is domination on all Borel sets.
```
theorem sourceAngle_positive_phase_domination (i : SourceCoordinate) (c : ℝ)
    (hc : 0 < c) (hlen : 1/4 ≤ c*sourceAngleUnit i) :
    (sourceAngleMarginal i).map (fun t => Int.fract (c*t)) ≤
      (5 : ℝ≥0∞) • unitIntervalMeasure := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceAngleUnit, OAI.FiniteFactor.sourceAngleMarginal, OAI.FiniteFactor.unitIntervalMeasure
theorem OAI.FiniteFactor.fract_neg_middle_iff line 59
Source documentation
Reflection preserves the symmetric phase eligibility interval, including integer phases at the cut.
```
theorem fract_neg_middle_iff (b t : ℝ) :
    Int.fract (-t) ∈ Set.Icc b (1-b) ↔ Int.fract t ∈ Set.Icc b (1-b) := by
…
```
theorem OAI.FiniteFactor.threshold_middle_iff line 66
theorem OAI.FiniteFactor.sourceAngle_phase_miss line 72
Source documentation
Proposition phases' one-coordinate miss bound, valid for both signs and for every coordinate in the actual source interval.
```
theorem sourceAngle_phase_miss (i : SourceCoordinate) (k : ℤ) (b : ℝ) (hb : 0 ≤ b)
    (hk : ((sourceBlockSize i.1 : ℝ)*(sourceStageState i.1).K)/4 ≤ |(k : ℝ)|) :
    sourceAngleMarginal i {t | 1-Int.fract ((k : ℝ)*t) ∉ Set.Icc b (1-b)} ≤
      ENNReal.ofReal (10*b) := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceBlockSize, OAI.FiniteFactor.sourceStageState, OAI.FiniteFactor.sourceAngleMarginal