RadialBridge.lean`

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SymmetricMahler.radialMap line 13
Source documentation
The actual M(r)=F(r) on the real diameter, taking its real part for a real-valued function on all of ℝ. The estimates use only 0≤r<1.
```
noncomputable def radialMap (r : ℝ) : ℝ := (MahlerConformal.F (r : ℂ)).re
```
Mentions: OAI.MahlerConformal.F
lemma OAI.SymmetricMahler.measurable_conformal_F line 15
lemma OAI.SymmetricMahler.measurable_radialMap line 24
lemma OAI.SymmetricMahler.continuousOn_radialMap line 28
theorem OAI.SymmetricMahler.hasDerivAt_radialMap line 34
theorem OAI.SymmetricMahler.radialMap_zero line 52
theorem OAI.SymmetricMahler.ofReal_radialMap line 56
Source documentation
Conjugation symmetry makes the real diameter's image real.
```
theorem ofReal_radialMap (r : ℝ) : (radialMap r : ℂ) = MahlerConformal.F (r : ℂ) := by
…
```
Mentions: OAI.SymmetricMahler.radialMap, OAI.MahlerConformal.F
theorem OAI.SymmetricMahler.hasDerivAt_radialMap_zero line 61
Source documentation
The derivative formula has the claimed positive removable value at zero.
```
theorem hasDerivAt_radialMap_zero : HasDerivAt radialMap (8/Real.pi^2) 0 := by
…
```
Mentions: OAI.SymmetricMahler.radialMap
theorem OAI.SymmetricMahler.conformal_radial_increment line 68
Source documentation
The actual series obeys the quantitative radial increment estimate.
```
theorem conformal_radial_increment {a b : ℝ}
    (ha : 0 ≤ a) (hab : a ≤ b) (hb : b < 1) :
    (4/Real.pi^2)*(b-a) ≤ radialMap b-radialMap a := by
…
```
Mentions: OAI.SymmetricMahler.radialMap
theorem OAI.SymmetricMahler.strictMonoOn_radialMap line 77
Source documentation
Strict radial monotonicity is proved on the entire positive real radius.
```
theorem strictMonoOn_radialMap : StrictMonoOn radialMap (Ico 0 1) := by
…
```
Mentions: OAI.SymmetricMahler.radialMap
theorem OAI.SymmetricMahler.radialMap_pos line 83
theorem OAI.SymmetricMahler.conformal_radial_error_small line 89
Source documentation
The actual series M has the required uniform small-error property. This instantiates the full real error analysis; its derivative is not an assumption.
```
theorem conformal_radial_error_small {ε : ℝ} (hε : 0 < ε) :
    ∃ m₀ : ℝ, ∀ m : ℝ, m₀ ≤ m → ∀ r₀ ∈ Ico (0 : ℝ) 1,
      IntervalIntegrable (errorIntegrand radialMap r₀ m) volume r₀ 1 ∧
      (∫ r in r₀..(1 : ℝ), errorIntegrand radialMap r₀ m r) < ε := by
…
```
Mentions: OAI.SymmetricMahler.errorIntegrand, OAI.SymmetricMahler.radialMap