OAI/Analysis/Kakeya/FixedScale.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

Three-dimensional cylinder averages, fixed-scale maximal bounds and finite weighted sampling.

  1. abbrev OAI.Kakeya.Space line 12
  2. abbrev OAI.Kakeya.Direction line 13
  3. def OAI.Kakeya.surfaceMeasure line 15
  4. def OAI.Kakeya.tube line 18
  5. def OAI.Kakeya.tubeAverage line 23
  6. def OAI.Kakeya.maximal line 28
  7. def OAI.Kakeya.MaximalConjecture line 31
  8. theorem OAI.Kakeya.direction_norm line 42
  9. theorem OAI.Kakeya.direction_inner line 45
  10. theorem OAI.Kakeya.mem_tube_iff line 48
  11. theorem OAI.Kakeya.isClosed_tube line 64
  12. theorem OAI.Kakeya.measurableSet_tube line 75
  13. abbrev OAI.Kakeya.axis line 78
  14. theorem OAI.Kakeya.direction_ne_zero line 80
  15. theorem OAI.Kakeya.finrank_axis line 85
  16. theorem OAI.Kakeya.finrank_plane line 88
  17. theorem OAI.Kakeya.axis_projection line 94
  18. def OAI.Kakeya.cylinderCoordinates line 98
  19. theorem OAI.Kakeya.cylinderCoordinates_measurePreserving line 102
  20. theorem OAI.Kakeya.tube_zero_eq_preimage line 107
  21. theorem OAI.Kakeya.volume_axis_closedBall line 121
  22. theorem OAI.Kakeya.volume_plane_closedBall line 126
  23. theorem OAI.Kakeya.volume_tube_zero line 134
  24. theorem OAI.Kakeya.tube_translate_preimage line 140
  25. theorem OAI.Kakeya.volume_tube line 145
  26. theorem OAI.Kakeya.tubeAverage_le_holder line 151
  27. theorem OAI.Kakeya.maximal_le_holder line 179
  28. theorem OAI.Kakeya.cylinderCoordinates_norm_fst line 185
  29. theorem OAI.Kakeya.cylinderCoordinates_norm_snd line 192
  30. theorem OAI.Kakeya.ae_cylinderBoundary_ne line 199
  31. theorem OAI.Kakeya.eventually_le_iff_of_ne line 238
  32. theorem OAI.Kakeya.ae_tendsto_tubeIndicator line 247
  33. theorem OAI.Kakeya.tube_subset_closedBall line 267
  34. theorem OAI.Kakeya.integrableOn_closedBall_of_memLp line 277
  35. theorem OAI.Kakeya.continuous_tubeIntegral line 284
  36. theorem OAI.Kakeya.continuous_tubeAverage line 318
  37. theorem OAI.Kakeya.lowerSemicontinuous_maximal line 326
  38. theorem OAI.Kakeya.measurable_maximal line 334
  39. theorem OAI.Kakeya.memLp_maximal line 338
  40. theorem OAI.Kakeya.maximal_real_smul line 356
  41. lemma OAI.Kakeya.eLpNorm_cube_eq line 366
  42. lemma OAI.Kakeya.eLpNorm_ennreal_mul line 372
  43. theorem OAI.Kakeya.maximal_bound_of_normalized line 379
  44. lemma OAI.Kakeya.surfaceMeasure_univ line 422
  45. theorem OAI.Kakeya.tubeAverage_congr_ae line 434
  46. theorem OAI.Kakeya.maximal_congr_ae line 443
  47. theorem OAI.Kakeya.maximal_norm_le_holder line 451
  48. def OAI.Kakeya.WeightedConvex.trialMass line 478
  49. def OAI.Kakeya.WeightedConvex.selected line 481
  50. def OAI.Kakeya.WeightedConvex.trialCount line 484
  51. lemma OAI.Kakeya.WeightedConvex.trialCount_eq_card line 487
  52. lemma OAI.Kakeya.WeightedConvex.trialMass_nonneg line 496
  53. lemma OAI.Kakeya.WeightedConvex.sum_trialMass line 504
  54. lemma OAI.Kakeya.WeightedConvex.moment_eq line 509
  55. lemma OAI.Kakeya.WeightedConvex.moment_le line 521
  56. lemma OAI.Kakeya.WeightedConvex.subset_exponent line 534
  57. lemma OAI.Kakeya.WeightedConvex.subset_moment_le line 545
  58. lemma OAI.Kakeya.WeightedConvex.shifted_subset_moment_le line 561
  59. lemma OAI.Kakeya.WeightedConvex.total_lower_tail_moment line 576
  60. lemma OAI.Kakeya.WeightedConvex.total_lower_tail_quarter line 591
  61. lemma OAI.Kakeya.WeightedConvex.test_shifted_moment line 600
  62. lemma OAI.Kakeya.WeightedConvex.exists_trial_lt_one line 616
  63. theorem OAI.Kakeya.WeightedConvex.finite_indexed_sample line 628
  64. def OAI.Kakeya.WeightedConvex.logarithmicConstant line 691
  65. theorem OAI.Kakeya.WeightedConvex.logarithmic_indexed_sample line 694