OAI/Analysis/DiskMaximal/Approximation.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakSobolev.HasGradient line 62

    Source documentation

    Directional, coordinate-free distributional gradient.

    def HasGradient (f : E → ℝ) (g : E → E) : Prop :=
…
  2. lemma OAI.WeakSobolev.HasGradient.congr_ae line 67
  3. lemma OAI.WeakSobolev.contDiff_hasGradient line 76
  4. lemma OAI.WeakSobolev.HasGradient.mul_contDiff line 88
  5. lemma OAI.WeakSobolev.gradient_convolution line 120
  6. lemma OAI.WeakSobolev.norm_convolution_le line 150
  7. lemma OAI.WeakSobolev.norm_sub_tendsto_zero line 171

    Source documentation

    Scheffe's argument for vector-valued L1 functions, without an a priori pointwise dominating function for the approximating sequence.

    lemma norm_sub_tendsto_zero {α F : Type*} [MeasurableSpace α]
    [NormedAddCommGroup F] {μ : Measure α} {f : α → F} {u : ℕ → α → F}
    (hf : Integrable f μ) (hu : ∀ n, Integrable (u n) μ)
    (hlim : ∀ᵐ x ∂μ, Tendsto (fun n => u n x) atTop (𝓝 (f x)))
    (hbound : ∀ n, (∫ x, ‖u n x‖ ∂μ) ≤ ∫ x, ‖f x‖ ∂μ) :
    Tendsto (fun n => ∫ x, ‖u n x-f x‖ ∂μ) atTop (𝓝 0) := by
…
  8. def OAI.WeakSobolev.mollifier line 206

    Source documentation

    A concrete normalized smooth approximate identity; all integrals retain the ambient Haar measure, rather than changing normalization.

    def mollifier (n : ℕ) : ContDiffBump (0 : E) where
…
  9. lemma OAI.WeakSobolev.mollifier_radius_tendsto line 213
  10. def OAI.WeakSobolev.smooth line 217
  11. def OAI.WeakSobolev.smoothVector line 219
  12. lemma OAI.WeakSobolev.smoothVector_integrable line 222
  13. lemma OAI.WeakSobolev.smoothVector_contDiff line 226
  14. lemma OAI.WeakSobolev.smoothVector_norm_le line 230
  15. lemma OAI.WeakSobolev.smoothVector_converges line 236
  16. lemma OAI.WeakSobolev.smooth_gradient line 244
  17. def OAI.WeakSobolev.cutoff line 268
  18. lemma OAI.WeakSobolev.cutoff_contDiff line 271
  19. lemma OAI.WeakSobolev.cutoff_compact line 275
  20. lemma OAI.WeakSobolev.cutoff_bound line 279
  21. lemma OAI.WeakSobolev.cutoff_tendsto line 283
  22. lemma OAI.WeakSobolev.norm_gradient_fderiv line 293
  23. lemma OAI.WeakSobolev.cutoff_gradient_bound line 297
  24. lemma OAI.WeakSobolev.cutoff_smul_integrable line 311
  25. lemma OAI.WeakSobolev.cutoff_smul_converges line 317
  26. lemma OAI.WeakSobolev.cutoff_gradient_integrable line 335
  27. lemma OAI.WeakSobolev.cutoff_gradient_converges line 344
  28. lemma OAI.WeakSobolev.integral_norm_sub_triangle line 365
  29. def OAI.WeakSobolev.cutGradient line 377
  30. lemma OAI.WeakSobolev.cutGradient_integrable line 381
  31. lemma OAI.WeakSobolev.cutGradient_converges line 387
  32. theorem OAI.WeakSobolev.exists_smooth_compact_approx line 403

    Source documentation

    Strong W11 density obtained by truncation and normalized mollification. Both approximations are genuine functions, not distributions defined by a new axiom.

    theorem exists_smooth_compact_approx {f : E → ℝ} {g : E → E}
    (hf : Integrable f μ) (hg : Integrable g μ) (hw : HasGradient (μ := μ) f g)
…

    Mentions: OAI.WeakSobolev.HasGradient

  33. lemma OAI.WeakSobolev.tendsto_eLpNorm_one line 437
  34. lemma OAI.WeakSobolev.integral_converges_norm line 447
  35. lemma OAI.WeakSobolev.exists_ae_subseq line 453
  36. lemma OAI.WeakSobolev.bounded_smul_converges line 459
  37. lemma OAI.WeakSobolev.integral_inner_mul line 480
  38. lemma OAI.WeakSobolev.HasGradient.limit line 489

    Source documentation

    The distributional identity is closed under strong L1 convergence of both functions and their genuine gradients.

    lemma HasGradient.limit {f : E → ℝ} {g : E → E} {u : ℕ → E → ℝ} {v : ℕ → E → E}
    (hf : Integrable f μ) (hg : Integrable g μ)
    (hu : ∀ n, Integrable (u n) μ) (hv : ∀ n, Integrable (v n) μ)
    (hw : ∀ n, HasGradient (μ := μ) (u n) (v n))
…

    Mentions: OAI.WeakSobolev.HasGradient

  39. lemma OAI.WeakSobolev.varying_smul_converges line 525
  40. lemma OAI.WeakSobolev.exists_smooth_sequence line 570
  41. lemma OAI.WeakSobolev.gradient_scalar_comp line 587
  42. lemma OAI.WeakSobolev.HasGradient.scalar_comp line 599
  43. def OAI.WeakSobolev.smoothAbs line 633

    Source documentation

    Smooth absolute-value approximation with zero preserved.

    def smoothAbs (ε x : ℝ) : ℝ := Real.sqrt (x^2+ε^2)-ε
  44. lemma OAI.WeakSobolev.smoothAbs_contDiff line 634
  45. lemma OAI.WeakSobolev.smoothAbs_hasDerivAt line 636
  46. lemma OAI.WeakSobolev.smoothAbs_deriv line 642
  47. lemma OAI.WeakSobolev.smoothAbs_deriv_bound line 644
  48. lemma OAI.WeakSobolev.smoothAbs_lipschitz line 651
  49. lemma OAI.WeakSobolev.smoothAbs_zero line 654
  50. lemma OAI.WeakSobolev.smoothAbs_bound line 656
  51. lemma OAI.WeakSobolev.smoothAbs_tendsto line 658
  52. def OAI.WeakSobolev.absCoefficient line 664
  53. lemma OAI.WeakSobolev.absCoefficient_bound line 665
  54. lemma OAI.WeakSobolev.absCoefficient_measurable line 669
  55. lemma OAI.WeakSobolev.smoothAbs_deriv_tendsto line 670
  56. lemma OAI.WeakSobolev.HasGradient.abs line 687
  57. lemma OAI.WeakSobolev.abs_gradient_bound line 718