Basic.lean`

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Genuine torus, smooth local quotient lifts, Haar probability, full mean-zero complex L2, and unconditional conclusion.

abbrev OAI.ThreeTorus.Torus line 14
Also declared: ComparatorChallenges/ThreeTorus.lean:21 (same declaration text).
abbrev OAI.ThreeTorus.Cover line 15
Also declared: ComparatorChallenges/ThreeTorus.lean:22 (same declaration text).
def OAI.ThreeTorus.project line 17
Also declared: ComparatorChallenges/ThreeTorus.lean:24 (same declaration text).
def OAI.ThreeTorus.Smooth line 19
Also declared: ComparatorChallenges/ThreeTorus.lean:26 (same declaration text).
def OAI.ThreeTorus.μ line 24
Also declared: ComparatorChallenges/ThreeTorus.lean:31 (same declaration text).
instance OAI.ThreeTorus.(instance at line 26) line 26
abbrev OAI.ThreeTorus.H line 28
Also declared: ComparatorChallenges/ThreeTorus.lean:35 (same declaration text).
def OAI.ThreeTorus.meanZero line 31
Source documentation
The full complex subspace defined by zero Lebesgue integral.
Also declared: ComparatorChallenges/ThreeTorus.lean:38 (same declaration text).
```
def meanZero : Submodule ℂ H where
…
```
Mentions: OAI.ThreeTorus.H
abbrev OAI.ThreeTorus.H₀ line 54
Also declared: ComparatorChallenges/ThreeTorus.lean:61 (same declaration text).
abbrev OAI.ThreeTorus.CircleH line 55
Also declared: ComparatorChallenges/ThreeTorus.lean:62 (same declaration text).
def OAI.ThreeTorus.IsReal line 57
Also declared: ComparatorChallenges/ThreeTorus.lean:64 (same declaration text).
def OAI.ThreeTorus.MainConclusion line 60
Source documentation
Complete simple Lebesgue spectrum, including the stated consequences.
Also declared: ComparatorChallenges/ThreeTorus.lean:67 (same declaration text).
```
def MainConclusion : Prop :=
…
```