OAI/Analysis/LipschitzHilbert/Fourier/SimpleFourierPairing.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Simple tests for Fourier interpolation on the actual averaging measure

A finite measurable profile partitions the real line into its fibers. Its matrix entries are actual Fourier integrals over those fibers. The two finite interpolation endpoints follow from positivity and the proved improved fourth-moment theorem.

  1. theorem OAI.LipschitzHilbert.PhaseCombinatorics.profile_eq_sum line 28
  2. theorem OAI.LipschitzHilbert.PhaseCombinatorics.integrable_profile line 41
  3. theorem OAI.LipschitzHilbert.PhaseCombinatorics.profile_bound line 51
  4. theorem OAI.LipschitzHilbert.PhaseCombinatorics.integral_profile_power line 56
  5. def OAI.LipschitzHilbert.PhaseCombinatorics.profileMatrix line 70
  6. theorem OAI.LipschitzHilbert.PhaseCombinatorics.norm_profileMatrix_le line 74
  7. theorem OAI.LipschitzHilbert.PhaseCombinatorics.finitePairing_profileMatrix line 81
  8. theorem OAI.LipschitzHilbert.PhaseCombinatorics.profileMatrix_fourth_endpoint line 116
  9. theorem OAI.LipschitzHilbert.PhaseCombinatorics.simple_fourier_pairing_bound line 148

    Source documentation

    Arbitrary finite-valued measurable tests, without any normalization on the test. This is the simple-test input to the bounded duality argument.

    theorem simple_fourier_pairing_bound (ν : Measure ℝ) [IsProbabilityMeasure ν]
    (frequency : ι → ℝ) (φ : ℝ → κ) (hφ : ∀ j, MeasurableSet {t | φ t = j})
    {gap D r s t : ℝ} (hgap : 0 < gap) (hsep : Separated frequency gap) (hν : FourierGap ν gap)
    (hD : 1 ≤ D) (hcard : (Fintype.card ι : ℝ) ≤ D)
    (hr : 0 < r) (hs : 0 < s) (ht0 : 0 ≤ t) (ht1 : t ≤ 1)
    (hrdef : (1 - t) * (r / 1) + t * (r / fourthExponent D) = 1)
    (hsdef : (1 - t) * (s / 1) + t * (s / (4 / 3)) = 1)
    (a : ι → ℂ) (b : κ → ℂ) (ha : (∑ i, ‖a i‖ ^ r) = 1) :
    ‖∫ u, finiteFourierSum frequency a u * b (φ u) ∂ν‖ ≤
      (∫ u, ‖b (φ u)‖ ^ s ∂ν) ^ (1 / s) := by
…

    Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.Separated, OAI.LipschitzHilbert.PhaseCombinatorics.FourierGap, OAI.LipschitzHilbert.PhaseCombinatorics.fourthExponent, OAI.LipschitzHilbert.PhaseCombinatorics.finiteFourierSum

  10. theorem OAI.LipschitzHilbert.PhaseCombinatorics.simpleFunc_fourier_pairing_bound line 171
  11. def OAI.LipschitzHilbert.PhaseCombinatorics.fourierInterpolationExponent line 189
  12. theorem OAI.LipschitzHilbert.PhaseCombinatorics.fourier_interpolation_parameters line 193
  13. theorem OAI.LipschitzHilbert.PhaseCombinatorics.simpleFunc_fourier_pairing_bound_at_p line 223