Main.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FourierLLogL.main_of_grid line 17
theorem OAI.FourierLLogL.almost_everywhere_fourier_convergence line 25
Source documentation
Almost everywhere convergence in L log L, all symmetric cutoffs.
```
theorem almost_everywhere_fourier_convergence (f : Torus → ℂ) (hf : MemLLogL f) :
    ∃ E : Set Torus, MeasurableSet E ∧ circleMeasure E = 0 ∧ ∀ x ∉ E,
      Tendsto (fun N : ℕ ↦ symmetricPartialSum f N x) atTop (𝓝 (f x)) :=
…
```
Mentions: OAI.FourierLLogL.Torus, OAI.FourierLLogL.MemLLogL, OAI.FourierLLogL.circleMeasure, OAI.FourierLLogL.symmetricPartialSum
theorem OAI.FourierLLogL.maximal_good_sets line 30
theorem OAI.FourierLLogL.weak_L1_maximal_bound line 36
Source documentation
Cor. "Weak-L^1 maximal bound", in the equivalent all-levels form.
```
theorem weak_L1_maximal_bound :
    ∃ C : ℝ, 0 < C ∧ ∀ (f : Torus → ℂ), MemLLogL f →
      ∀ w : ℝ, 0 < w →
        w*circleMeasure.real (cloudSet f w) ≤ C*luxNorm f :=
…
```
Mentions: OAI.FourierLLogL.Torus, OAI.FourierLLogL.MemLLogL, OAI.FourierLLogL.cloudSet, OAI.FourierLLogL.luxNorm