ScalarPhase.lean`

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

def OAI.KervaireScalarPhase.phase line 17
theorem OAI.KervaireScalarPhase.phase_one line 19
theorem OAI.KervaireScalarPhase.phase_nonneg line 21
theorem OAI.KervaireScalarPhase.phase_lt_one line 23
theorem OAI.KervaireScalarPhase.measurable_phase line 25
theorem OAI.KervaireScalarPhase.phase_exp line 28
theorem OAI.KervaireScalarPhase.phase_exp_normalized line 37
def OAI.KervaireScalarPhase.cutApproach line 44
Source documentation
Tangential approach to the phase cut, from the prescribed side.
```
def cutApproach (ε : ℝ) : ℂ := (1 - ε ^ 2 : ℝ) + ε * Complex.I
```
theorem OAI.KervaireScalarPhase.norm_cutApproach_lt_one line 46
theorem OAI.KervaireScalarPhase.exp_two_arg line 57
Source documentation
The polar angle encoded by a doubled exponential.
```
theorem exp_two_arg (x : ℂ) (hx : x ≠ 0) :
    Complex.exp ((2 * x.arg : ℝ) * Complex.I) = x / star x := by
…
```
theorem OAI.KervaireScalarPhase.phase_eq_arg_one_sub line 73
Source documentation
Exact scalar phase away from its cut, expressed by the logarithm in the disk.
```
theorem phase_eq_arg_one_sub {z : ℂ} (hz : ‖z‖ = 1) (hz' : z ≠ 1) :
    phase z = 1 / 2 + (1 - z).arg / Real.pi := by
…
```
Mentions: OAI.KervaireScalarPhase.phase
def OAI.KervaireScalarPhase.smoothPhase line 121
Source documentation
The regularization used in the trace inequality.
```
def smoothPhase (a z : ℂ) : ℝ := 1 / 2 + (1 - a * z).arg / Real.pi
```
theorem OAI.KervaireScalarPhase.re_one_sub_mul_pos line 123
theorem OAI.KervaireScalarPhase.smoothPhase_mem_Icc line 129
theorem OAI.KervaireScalarPhase.re_one_sub_pos line 140
theorem OAI.KervaireScalarPhase.tendsto_smoothPhase_cut line 152
Source documentation
The tangential limit agrees with the discontinuous phase, also at one.
```
theorem tendsto_smoothPhase_cut {z : ℂ} (hz : ‖z‖ = 1) :
    Tendsto (fun ε : ℝ => smoothPhase (cutApproach ε) z)
      (𝓝[>] 0) (𝓝 (phase z)) := by
…
```
Mentions: OAI.KervaireScalarPhase.smoothPhase, OAI.KervaireScalarPhase.cutApproach, OAI.KervaireScalarPhase.phase
theorem OAI.KervaireScalarPhase.smoothPhase_eq_series line 191
Source documentation
The Mercator sum realizes the same real phase regularization.
```
theorem smoothPhase_eq_series {a z : ℂ} (haz : ‖a * z‖ < 1) :
    smoothPhase a z = 1 / 2 -
      (∑' n : ℕ, (a * z) ^ (n+1) / (n+1)).im / Real.pi := by
…
```
Mentions: OAI.KervaireScalarPhase.smoothPhase
def OAI.KervaireScalarPhase.cutTime line 198
Source documentation
A concrete sequence in the open disk approaching the required side of the cut.
```
def cutTime (n : ℕ) : ℝ := 1 / ((n : ℝ) + 2)
```
theorem OAI.KervaireScalarPhase.cutTime_pos line 200
theorem OAI.KervaireScalarPhase.cutTime_lt_one line 204
theorem OAI.KervaireScalarPhase.tendsto_cutTime line 210
theorem OAI.KervaireScalarPhase.norm_cutApproach_cutTime_lt_one line 218
theorem OAI.KervaireScalarPhase.tendsto_smoothPhase_cutTime line 221