PhaseCoverage.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FiniteFactor.sourceFirstPhaseLower line 10
theorem OAI.FiniteFactor.sourcePhaseUpper_tendsto line 12
theorem OAI.FiniteFactor.sourcePhaseOverlap line 21
theorem OAI.FiniteFactor.sourcePhase_range_coverage line 26
Source documentation
The real interval coverage from the contradiction, with the first range used only at strictly later blocks. No magnitude is silently omitted.
```
theorem sourcePhase_range_coverage (j : ℕ) (t : ℝ) (ht : sourcePhaseLower j ≤ t) :
    ∃ s : ℕ,
      (j ≤ s ∧ sourcePhaseLower s ≤ t ∧ t ≤ sourcePhaseUpper s) ∨
      (j < s ∧ sourceFirstPhaseLower s ≤ t ∧ t ≤ sourcePhaseLower s) := by
…
```
Mentions: OAI.FiniteFactor.sourcePhaseLower, OAI.FiniteFactor.sourcePhaseUpper, OAI.FiniteFactor.sourceFirstPhaseLower
def OAI.FiniteFactor.sourceQualifying line 51
Source documentation
The finite deterministic qualifying list at one selected block.
```
def sourceQualifying (θ : SourceCoordinate → ℝ) (s : ℕ) (k : ℤ) (w : Fin 2) :
    Finset SourceCoordinate :=
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate
def OAI.FiniteFactor.SourceSecondPhasesFrom line 56
theorem OAI.FiniteFactor.sourceAngleLaw_second_phases_from line 61

theorem OAI.FiniteFactor.exists_source_qualifying_assignment line 70

Source documentation

For every large omitted index, this constructs a block, width, and finite qualifying list depending only on the fixed angles and the index.

theorem exists_source_qualifying_assignment (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ)
    (j : ℕ) (hphase : SourceSecondPhasesFrom θ j) (k : ℤ)
    (hk : sourcePhaseLower j ≤ |(k : ℝ)|) :
    ∃ (s : ℕ) (w : Fin 2) (I : Finset SourceCoordinate),
      j ≤ s ∧ (w = 0 → j < s) ∧ I ⊆ sourceBlockCoordinates s ∧
      (sourceBlockSize s : ℝ)/20 ≤ (I.card : ℝ) ∧
      ∀ i ∈ I, 1-Int.fract ((k : ℝ)*θ i) ∈ Set.Icc (sourceWidth s w) (1-sourceWidth s w) := by
…

Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.SourceSecondPhasesFrom, OAI.FiniteFactor.sourcePhaseLower, OAI.FiniteFactor.sourceBlockCoordinates, OAI.FiniteFactor.sourceBlockSize, OAI.FiniteFactor.sourceWidth