AngleRelations.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.independent_sum_ne line 13

Source documentation

Independent real variables cannot satisfy a prescribed affine equation when the second variable has no atoms.

theorem independent_sum_ne {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}
    [IsProbabilityMeasure μ] {f g : Ω → ℝ} (hf : Measurable f) (hg : Measurable g)
    (hfg : IndepFun f g μ) (hg0 : ∀ r : ℝ, μ {ω | g ω = r} = 0) (c : ℝ) :
    ∀ᵐ ω ∂μ, f ω + g ω ≠ c := by
…

theorem OAI.FiniteFactor.sourceAngleLaw_scaled_atomless line 31
theorem OAI.FiniteFactor.sourceAngleLaw_relation_ne line 45
Source documentation
Every nontrivial finitely supported integer relation has probability zero.
```
theorem sourceAngleLaw_relation_ne (v : SourceCoordinate →₀ ℤ) (hv : v ≠ 0) (c : ℤ) :
    ∀ᵐ θ ∂sourceAngleLaw, v.sum (fun i n => (n : ℝ)*θ i) ≠ (c : ℝ) := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceAngleLaw
def OAI.FiniteFactor.SourceRationalIndependent line 65
Source documentation
Exact integer formulation of rational independence of 1 and all angles.
```
def SourceRationalIndependent (θ : SourceCoordinate → ℝ) : Prop :=
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate
theorem OAI.FiniteFactor.sourceAngleLaw_rationalIndependent line 69