Fourier.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

Circle traces, Fourier uniqueness, and Laurent reconstruction

abbrev OAI.Nagata.W01.AngularCircle line 22
def OAI.Nagata.W01.circleParam line 24
theorem OAI.Nagata.W01.circleParam_ne_zero line 27
theorem OAI.Nagata.W01.continuous_circleParam line 31
theorem OAI.Nagata.W01.circleParam_coe line 34
theorem OAI.Nagata.W01.circleParam_arg line 38
def OAI.Nagata.W01.circleTrace line 43
theorem OAI.Nagata.W01.circleTrace_coe line 46
theorem OAI.Nagata.W01.continuous_circleTrace line 50
def OAI.Nagata.W01.circleTraceMap line 57
Source documentation
The actual continuous restriction to the circle, with continuity proved locally.
```
def circleTraceMap (r : ℝ) (hr : 0 < r) (f : ℂ → ℂ)
    (hf : ∀ z, z ≠ 0 → ContinuousAt f z) : C(AngularCircle, ℂ) :=
…
```
Mentions: OAI.Nagata.W01.AngularCircle
theorem OAI.Nagata.W01.punctured_eq_zero_of_circleTrace_zero line 62
Source documentation
Positive-radius circles exhaust the genuine domain C*.
```
theorem punctured_eq_zero_of_circleTrace_zero {f : ℂ → ℂ}
    (h : ∀ r : ℝ, 0 < r → ∀ t : AngularCircle, circleTrace r f t = 0) :
    ∀ z : ℂ, z ≠ 0 → f z = 0 := by
…
```
Mentions: OAI.Nagata.W01.AngularCircle, OAI.Nagata.W01.circleTrace
theorem OAI.Nagata.W01.continuous_circle_zero_of_fourier_zero line 74
Source documentation
A genuine continuous function on a circle is determined by its Fourier coefficients.
```
theorem continuous_circle_zero_of_fourier_zero (f : C(AddCircle T, ℂ))
    (h : ∀ k : ℤ, fourierCoeff f k = 0) : f = 0 := by
…
```
theorem OAI.Nagata.W01.continuous_circle_eq_of_fourier_eq line 85
Source documentation
Uniqueness compares the actual functions, rather than formal coefficient sequences.
```
theorem continuous_circle_eq_of_fourier_eq (f g : C(AddCircle T, ℂ))
    (h : ∀ k : ℤ, fourierCoeff f k = fourierCoeff g k) : f = g := by
…
```
theorem OAI.Nagata.W01.laurent_tangent_integrand line 107
theorem OAI.Nagata.W01.laurent_scalar_normalization line 118
theorem OAI.Nagata.W01.laurent_radius_factor_ne_zero line 122
theorem OAI.Nagata.W01.fourier_eq_circle_zpow line 138
theorem OAI.Nagata.W01.circleMap_zpow_fourier line 142
theorem OAI.Nagata.W01.laurent_integrand_parameterization line 146
theorem OAI.Nagata.W01.analyticLaurentCoeff_eq_fourier line 155
Source documentation
Exact comparison of the genuine complex circle integral with Fourier extraction.
```
theorem analyticLaurentCoeff_eq_fourier {r : ℝ} (hr : 0 < r)
    (f : ℂ → ℂ) (k : ℤ) :
    Nagata.W09.analyticLaurentCoeff r f k =
      (r : ℂ) ^ (-k) * fourierCoeff (circleTrace r f) k := by
…
```
Mentions: OAI.Nagata.W09.analyticLaurentCoeff, OAI.Nagata.W01.circleTrace
theorem OAI.Nagata.W01.circleTrace_zero_of_laurentCoeff_zero line 176
Source documentation
Zero Laurent coefficients on a radius force the actual circle restriction to vanish.
```
theorem circleTrace_zero_of_laurentCoeff_zero {r : ℝ} (hr : 0 < r) (f : ℂ → ℂ)
    (hf : ∀ z, z ≠ 0 → ContinuousAt f z)
    (hc : ∀ k : ℤ, Nagata.W09.analyticLaurentCoeff r f k = 0) :
    ∀ t : AngularCircle, circleTrace r f t = 0 := by
…
```
Mentions: OAI.Nagata.W09.analyticLaurentCoeff, OAI.Nagata.W01.AngularCircle, OAI.Nagata.W01.circleTrace

theorem OAI.Nagata.W01.punctured_zero_of_all_laurentCoeff_zero line 190

Source documentation

Laurent uniqueness on C* via actual continuous restrictions and circle exhaustion.

theorem punctured_zero_of_all_laurentCoeff_zero (f : ℂ → ℂ)
    (hf : ∀ z, z ≠ 0 → ContinuousAt f z)
    (hc : ∀ r : ℝ, 0 < r → ∀ k : ℤ, Nagata.W09.analyticLaurentCoeff r f k = 0) :
    ∀ z : ℂ, z ≠ 0 → f z = 0 := by
…

Mentions: OAI.Nagata.W09.analyticLaurentCoeff

theorem OAI.Nagata.W01.punctured_zero_of_radius_one_laurentCoeff_zero line 207
theorem OAI.Nagata.W01.laurentCoefficientMap_injective line 217
Source documentation
Actual extraction at radius one is injective on genuine holomorphic sections.
```
theorem laurentCoefficientMap_injective (τ : ℂ) (n : ℤ) (γ : ℂ) :
    Function.Injective (Nagata.W09.laurentCoefficientMap τ n γ) := by
…
```
Mentions: OAI.Nagata.W09.laurentCoefficientMap