OAI/Analysis/DiskMaximal/WeakLimits.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakCompact.bounded_tendsto line 59

    Source documentation

    A single free ultrafilter furnishes simultaneous weak limits; no sequence of gradients or a Radon representation is being added as an assumption.

    lemma bounded_tendsto {a : ℕ → ℝ} {B : ℝ} (hb : ∀ n, |a n| ≤ B) :
    Tendsto a (hyperfilter ℕ) (𝓝 (limUnder (hyperfilter ℕ) a)) := by
…
  2. def OAI.WeakCompact.limitValue line 74
  3. lemma OAI.WeakCompact.limit_tendsto line 78
  4. def OAI.WeakCompact.limitPositive line 81
  5. lemma OAI.WeakCompact.limit_bound line 92
  6. def OAI.WeakCompact.limitMeasure line 97
  7. lemma OAI.WeakCompact.integral_limitMeasure line 99
  8. lemma OAI.WeakCompact.limitMeasure_compact_bound line 104
  9. lemma OAI.WeakCompact.limitMeasure_finite_bound line 119
  10. lemma OAI.WeakSobolev.gradient_l1_eq line 131
  11. lemma OAI.WeakSobolev.smooth_sobolev_two line 138
  12. lemma OAI.WeakSobolev.gradient_integral_le line 148
  13. lemma OAI.WeakSobolev.sobolev_two_le line 162

    Source documentation

    The planar Sobolev embedding extended by genuine strong W11 density. The harmless slack one is used only for finiteness/local convergence.

    lemma sobolev_two_le (hd : Module.finrank ℝ E = 2)
    {f : E → ℝ} {g : E → E} (hf : Integrable f μ) (hg : Integrable g μ)
    (hw : HasGradient (μ := μ) f g) :
…

    Mentions: OAI.WeakSobolev.HasGradient

  14. lemma OAI.WeakSobolev.memLp_two line 176
  15. lemma OAI.WeakSobolev.lipschitz_hasGradient line 181
  16. lemma OAI.DiskMaximalTools.rationalMaximal_ae_finite line 189
  17. def OAI.DiskMaximalTools.absoluteMeasure line 211

    Source documentation

    A density measure built from the actual absolute values; a.e. changes of representative do not change any radius average.

    def absoluteMeasure (f : ℂ → ℝ) : Measure ℂ := volume.withDensity (fun y => ENNReal.ofReal |f y|)
  18. lemma OAI.DiskMaximalTools.absoluteMeasure_finite line 213
  19. lemma OAI.DiskMaximalTools.absoluteMeasure_congr line 218
  20. def OAI.DiskMaximalTools.maximalComplex line 221
  21. def OAI.DiskMaximalTools.maximalComplexReal line 222
  22. lemma OAI.DiskMaximalTools.memLp_maximalComplexReal_of_measurable line 224
  23. lemma OAI.DiskMaximalTools.memLp_maximalComplexReal line 243
  24. lemma OAI.DiskMaximalTools.maximalComplex_ae_finite line 254
  25. lemma OAI.DiskMaximalTools.maximalComplex_eq_all_radii line 259
  26. lemma OAI.WeakSobolev.integral_norm_converges line 275
  27. def OAI.SobolevBand.band line 291
  28. lemma OAI.SobolevBand.average_abs_le line 293
  29. lemma OAI.SobolevBand.average_sub line 306
  30. lemma OAI.SobolevBand.values_bdd line 310
  31. lemma OAI.SobolevBand.average_le_band line 316
  32. lemma OAI.SobolevBand.band_le line 320
  33. lemma OAI.SobolevBand.band_sub_le line 326
  34. lemma OAI.SobolevBand.smooth_average_lipschitz line 345
  35. lemma OAI.SobolevBand.smooth_band_lipschitz line 365
  36. lemma OAI.SobolevBand.band_converges line 371
  37. lemma OAI.SobolevBand.band_lipschitz line 380
  38. lemma OAI.WeakCompact.density_test_integrable line 401
  39. def OAI.WeakCompact.densityPositive line 406
  40. lemma OAI.WeakCompact.densityPositive_bound line 422
  41. lemma OAI.WeakCompact.densityPositive_norm_bound line 432
  42. lemma OAI.WeakCompact.density_test_le_set line 438
  43. def OAI.WeakCompact.densityLimit line 452
  44. lemma OAI.WeakCompact.densityLimit_integral line 455
  45. lemma OAI.WeakCompact.densityLimit_mass line 459
  46. lemma OAI.WeakCompact.densityLimit_regular line 462
  47. lemma OAI.WeakCompact.densityLimit_finite line 463
  48. lemma OAI.WeakCompact.densityLimit_compact_bound line 468

    Source documentation

    The local lower-semicontinuity estimate needed for null-set localization. Only eventual bounds are required, so large-radius splitting may start late.

    lemma densityLimit_compact_bound {D : ℝ} {K O : Set X} (hK : IsCompact K) (hO : IsOpen O)
    (hKO : K ⊆ O) (hD : ∀ᶠ n in atTop, (∫ x in O,w n x ∂μ) ≤ D) :
    densityLimit w hw h0 hb K ≤ ENNReal.ofReal D := by
…

    Mentions: OAI.WeakCompact.densityLimit

  49. lemma OAI.WeakCompact.densityLimit_sharp_mass line 492
  50. lemma OAI.WeakCompact.absolutelyContinuous_of_compact_null line 514
  51. def OAI.SobolevBand.low line 532
  52. def OAI.SobolevBand.high line 533
  53. lemma OAI.SobolevBand.low_pos line 534
  54. lemma OAI.SobolevBand.high_pos line 535
  55. lemma OAI.SobolevBand.low_le_high line 536
  56. lemma OAI.SobolevBand.low_antitone line 541
  57. lemma OAI.SobolevBand.high_monotone line 544
  58. lemma OAI.SobolevBand.low_tendsto line 547
  59. lemma OAI.SobolevBand.high_tendsto line 550
  60. lemma OAI.SobolevBand.eventually_mem_band line 552
  61. lemma OAI.SobolevBand.absolute_average_eq line 556
  62. lemma OAI.SobolevBand.abs_average_nonneg line 563
  63. lemma OAI.SobolevBand.abs_band_nonneg line 568
  64. lemma OAI.SobolevBand.abs_band_le_maximal line 572
  65. lemma OAI.SobolevBand.band_mono_interval line 581
  66. lemma OAI.SobolevBand.diagonal_monotone line 588
  67. lemma OAI.SobolevBand.diagonal_tendsto line 593
  68. lemma OAI.SobolevBand.locallyIntegrable_maximal line 617
  69. lemma OAI.SobolevBand.diagonal_local_L1 line 622
  70. lemma OAI.SobolevBand.geometric_band_eq line 651
  71. lemma OAI.SobolevBand.smooth_band_integrable_gradient line 657
  72. lemma OAI.SobolevBand.smooth_dyadic_bound line 662
  73. lemma OAI.SobolevBand.band_ae_touching line 670
  74. lemma OAI.SobolevBand.split_gradient line 683

    Source documentation

    Quantitative large-radius truncation; small radii are the only term needing localization. Differentiable touching avoids any unproved max-chain rule.

    lemma split_gradient {f : ℂ → ℝ} (hf : ContDiff ℝ 1 f) (hc : HasCompactSupport f)
    {a t b : ℝ} (ha : 0<a) (hat : a≤t) (htb : t≤b) :
    ∀ᵐ x, ‖gradient (band f a b) x‖ ≤ ‖gradient (band f a t) x‖+
      (∫ y,‖gradient f y‖)/(Real.pi*t^2) := by
…

    Mentions: OAI.SobolevBand.band