Endpoint.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Deduction of the L log L theorem from a good set estimate

def OAI.FourierLLogL.symmetricMaximal line 14
theorem OAI.FourierLLogL.measurable_symmetricMaximal line 17
theorem OAI.FourierLLogL.symmetricMaximal_mul line 20
def OAI.FourierLLogL.GoodBound line 26
Source documentation
Good-set estimate. We state it at exponential heights exp d with d = 2^j.
```
def GoodBound : Prop :=
…
```

theorem OAI.FourierLLogL.GoodBound.ae_tail_majorant line 37

Source documentation

Transfer the good-set estimates to summable pointwise majorants for a sequence. Finitely many terms per point may not have been bounded. We include the untransformed term for use with approximations.

theorem GoodBound.ae_tail_majorant
    (hgb : GoodBound) (F : ℕ → Torus → ℂ) (w : ℕ → ℝ) (L : ℕ)
    (hF : ∀ j, Integrable (F j) circleMeasure)
    (hw : ∀ j, 0 < w j)
    (hsum : Summable (fun j => (2:ℝ)^j * w j))
    (hm : ∀ j, (∫ x, ‖F j x‖ ∂circleMeasure) ≤ w j)
    (hh : ∀ j, ∀ᵐ x ∂circleMeasure, ‖F j x‖ ≤ w j * Real.exp ((2:ℝ)^(j+L))) :
    ∀ᵐ x ∂circleMeasure, ∃ b : ℕ → ℝ, Summable b ∧ ∀ᶠ j : ℕ in atTop,
      ∀ N, ‖symmetricPartialSum (F j) N x‖ + ‖F j x‖ ≤ b j := by
…

Mentions: OAI.FourierLLogL.GoodBound, OAI.FourierLLogL.Torus, OAI.FourierLLogL.circleMeasure, OAI.FourierLLogL.symmetricPartialSum

def OAI.FourierLLogL.trigPolys line 138
Source documentation
Trigonometric polynomials, as a subspace of continuous functions.
```
def trigPolys : Submodule ℂ C(Torus, ℂ) := Submodule.span ℂ (Set.range fourier)
```
Mentions: OAI.FourierLLogL.Torus
lemma OAI.FourierLLogL.integrable_continuous line 140
theorem OAI.FourierLLogL.eventually_partialSum_trigPoly line 145
lemma OAI.FourierLLogL.exists_bounded_trigPoly_approx line 175
def OAI.FourierLLogL.pad line 238
lemma OAI.FourierLLogL.pad_pos line 240
lemma OAI.FourierLLogL.summable_pad line 242
lemma OAI.FourierLLogL.pad_height line 247
theorem OAI.FourierLLogL.GoodBound.ae_convergence_bounded line 265
theorem OAI.FourierLLogL.GoodBound.main_bound_consequence line 311