PreparedBase.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.exists_source_prepared_base line 19
Source documentation
One fixed realization supplies phases, rational independence, ordered sampling and the actual nonzero quasinilpotent operator in its generated algebra, before any candidate invariant projection. Factor and predual properties are not included: they remain obligations about this algebra.
```
theorem exists_source_prepared_base : ∃ θ : SourceCoordinate → ℝ,
    SourceRationalIndependent θ ∧
    (∃ j : ℕ, SourceSecondPhasesFrom θ j) ∧
    SourceOrderedTorusSampling θ ∧
    (∀ k : ℤ, MeasurePreserving (coordinateRotate θ k) sourceSamplingHaar sourceSamplingHaar) ∧
    (∀ k : ℤ, k ≠ 0 → ∀ x, coordinateRotate θ k x ≠ x) ∧
    ∃ hθ : SourceAngles θ,
      let T := sourceOperator θ sourceLogWeight hθ.nonneg sourceLogWeight_nonneg
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceRationalIndependent, OAI.FiniteFactor.SourceSecondPhasesFrom, OAI.FiniteFactor.SourceOrderedTorusSampling, OAI.FiniteFactor.coordinateRotate, OAI.FiniteFactor.sourceSamplingHaar, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.sourceOperator, OAI.FiniteFactor.sourceLogWeight, OAI.FiniteFactor.sourceLogWeight_nonneg