ContinuousYoung.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The continuous-frequency Young estimate used by the homogeneous algebra

Only the nonnegative L¹–L² estimate needed for Fourier magnitudes is proved. Weighted Cauchy–Schwarz gives the pointwise bound; the existing convolution Fubini theorem integrates its majorant.

theorem OAI.DefocusingNLS.continuousWeightedCauchySchwarz line 24

Source documentation

Weighted Cauchy–Schwarz without introducing a probability normalization.

theorem continuousWeightedCauchySchwarz (f g : E → ℝ)
    (hf : Integrable f) (hg : AEStronglyMeasurable g volume)
    (hfp : ∀ x, 0 ≤ f x) (hgp : ∀ x, 0 ≤ g x)
    (hfg : Integrable (fun x => f x * g x ^ 2)) :
    (∫ x, f x * g x) ^ 2 ≤ (∫ x, f x) * ∫ x, f x * g x ^ 2 := by
…

def OAI.DefocusingNLS.positiveFrequencyConvolution line 58
theorem OAI.DefocusingNLS.positiveFrequencyConvolution_comm line 61

theorem OAI.DefocusingNLS.continuousYoung_nonnegative line 68

Source documentation

The exact L¹–L² Young bound, in its squared form.

theorem continuousYoung_nonnegative (f g : E → ℝ)
    (hf : Integrable f) (hg : Continuous g)
    (hfp : ∀ x, 0 ≤ f x) (hgp : ∀ x, 0 ≤ g x)
    (hg2 : Integrable (fun x => g x ^ 2))
    (K : ℝ) (_hK : 0 ≤ K) (hgb : ∀ x, g x ≤ K) :
    Integrable (fun ξ => positiveFrequencyConvolution f g ξ ^ 2) ∧
      (∫ ξ, positiveFrequencyConvolution f g ξ ^ 2) ≤
        (∫ ξ, f ξ) ^ 2 * ∫ ξ, g ξ ^ 2 := by
…

Mentions: OAI.DefocusingNLS.positiveFrequencyConvolution