AngularFibers.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SymmetricMahler.fiberDomain line 10
lemma OAI.SymmetricMahler.fiberDomain_isOpen line 13
lemma OAI.SymmetricMahler.exists_fiberAngle line 21
def OAI.SymmetricMahler.fiberAngle line 27
Source documentation
The unique upper-half-disk angle, extended by zero outside its open radial domain.
```
noncomputable def fiberAngle (q r : ℝ) : ℝ := by
…
```
lemma OAI.SymmetricMahler.fiberAngle_spec line 31
theorem OAI.SymmetricMahler.contDiffAt_fiberAngle line 39
Source documentation
Local implicit angles agree with the globally chosen fiber by uniqueness. Thus the global choice is smooth at every point of its open domain.
```
theorem contDiffAt_fiberAngle {q r : ℝ} (hr : r ∈ fiberDomain q) :
    ContDiffAt ℝ ∞ (fiberAngle q) r := by
…
```
Mentions: OAI.SymmetricMahler.fiberDomain, OAI.SymmetricMahler.fiberAngle
theorem OAI.SymmetricMahler.measurable_fiberAngle line 57
Source documentation
Measurability of the actual fiber angle, including its zero extension.
```
theorem measurable_fiberAngle (q : ℝ) : Measurable (fiberAngle q) := by
…
```
Mentions: OAI.SymmetricMahler.fiberAngle
theorem OAI.SymmetricMahler.mem_fiberDomain_of_basepoint line 70
Source documentation
Every radius after r0 has a unique fiber angle when M(r0)=|q|.
```
theorem mem_fiberDomain_of_basepoint {q r₀ r : ℝ} (hr₀ : 0 ≤ r₀)
    (hq : radialMap r₀ = |q|) (hr : r ∈ Ioo r₀ 1) : r ∈ fiberDomain q := by
…
```
Mentions: OAI.SymmetricMahler.radialMap, OAI.SymmetricMahler.fiberDomain