OAI/Analysis/Littlewood/Spreading.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.AsymptoticallyMinimalLittlewood.Spreading.quadratic_norm_scaled line 15

    Source documentation

    The uniform stationary-phase bound in the squared, scale-invariant form needed for every retained spread Fourier coefficient.

    lemma quadratic_norm_scaled {g : ℝ → ℂ} (hg : HasCompactSupport g)
    (hgs : ContDiff ℝ ∞ g) (hg1 : ∀ x, ‖g x‖≤1)
    {β : ℝ} (hβ : β≠0) :
    ∃ C : ℝ, 0≤C ∧ ∀ T, 0<T → ∀ u : ℝ,
      T*|β| *‖∫ x : ℝ, g x*phase (T*β) u x‖^2 ≤ (1+C/T)^2 := by
…
  2. def OAI.AsymptoticallyMinimalLittlewood.Spreading.multiBox line 46
  3. def OAI.AsymptoticallyMinimalLittlewood.Spreading.determinant line 49
  4. lemma OAI.AsymptoticallyMinimalLittlewood.Spreading.determinant_pos line 52
  5. lemma OAI.AsymptoticallyMinimalLittlewood.Spreading.multiBox_card_bound line 55
  6. lemma OAI.AsymptoticallyMinimalLittlewood.Spreading.multiBox_eventual_card line 67
  7. lemma OAI.AsymptoticallyMinimalLittlewood.Spreading.tensor_coefficient_eventual line 87
  8. lemma OAI.AsymptoticallyMinimalLittlewood.Spreading.row_mass_le line 115
  9. lemma OAI.AsymptoticallyMinimalLittlewood.Spreading.row_mass_tendsto line 127
  10. lemma OAI.AsymptoticallyMinimalLittlewood.Spreading.tensor_mass_tendsto line 141
  11. lemma OAI.AsymptoticallyMinimalLittlewood.Spreading.tensor_uniform_error line 159
  12. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.support_pair_sum line 185
  13. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.binary_positive_data line 203
  14. def OAI.AsymptoticallyMinimalLittlewood.Auxiliary.rowForm line 234
  15. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.rowForm_apply line 237
  16. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.rowForm_injective line 240
  17. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.positive_rowForm_ne_zero line 248
  18. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.positive_rowForm_nonparallel line 255
  19. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.mFourier_norm_apply line 275
  20. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.mFourier_add_point line 279
  21. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.mFourier_real line 284
  22. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.phase_tensor_character line 295
  23. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.spread_half_bound line 313
  24. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.tensor_trunc_expand line 355
  25. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.cutoff_power line 363
  26. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.spread_trunc_eventual_bound line 380
  27. structure OAI.AsymptoticallyMinimalLittlewood.Auxiliary.RawData line 450
  28. structure OAI.AsymptoticallyMinimalLittlewood.Auxiliary.FinitePacket line 466
  29. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.mFourier_sum_type line 476
  30. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.spread_numeric_coefficient line 482
  31. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.spread_numeric_width line 501
  32. lemma OAI.AsymptoticallyMinimalLittlewood.Auxiliary.spread_numeric_energy line 515
  33. theorem OAI.AsymptoticallyMinimalLittlewood.Auxiliary.exists_auxiliary_packet line 535

    Source documentation

    The full Fourier-spreading construction, before adjoining a harmless zero coefficient to ensure that the packing catalogue has at least two rows.

    theorem exists_auxiliary_packet {δ : ℝ} (hδ : 0<δ) (hδ20 : δ<1/20) :
    Nonempty (FinitePacket δ) := by
…

    Mentions: OAI.AsymptoticallyMinimalLittlewood.Auxiliary.FinitePacket