OAI/Analysis/BernoulliCone/SobolevCalculus.lean

GitHub source file

128 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Bernoulli.Test.continuous_gradient line 20
2. theorem OAI.Bernoulli.Test.compact_gradient line 24
3. theorem OAI.Bernoulli.Test.memLp line 27
4. theorem OAI.Bernoulli.Test.memLp_gradient line 31
5. theorem OAI.Bernoulli.Test.eq_zero_outside line 36
6. theorem OAI.Bernoulli.Test.weakGradient line 40
7. theorem OAI.Bernoulli.Test.h1 line 59
8. theorem OAI.Bernoulli.Test.h10 line 62
9. lemma OAI.Bernoulli.memLp_inner_const line 73
10. lemma OAI.Bernoulli.Test.memLp_directional line 79
11. lemma OAI.Bernoulli.integrable_deriv_product line 83
12. lemma OAI.Bernoulli.integrable_inner_test line 88
13. lemma OAI.Bernoulli.H1.add line 93
14. lemma OAI.Bernoulli.H1.const_smul line 105
15. lemma OAI.Bernoulli.Test.const_mul line 118
16. lemma OAI.Bernoulli.Test.gradient_const_mul line 123
17. lemma OAI.Bernoulli.Test.h10_const_mul line 132
18. lemma OAI.Bernoulli.integrable_phase line 137
19. lemma OAI.Bernoulli.integrable_inner_of_memLp line 148
20. lemma OAI.Bernoulli.energy_affine line 155
21. lemma OAI.Bernoulli.linear_coefficient_eq_zero line 186
22. lemma OAI.Bernoulli.firstVariation_of_comparison line 202

    Source documentation

    The first variation for compact perturbations whose support stays uniformly inside the positive phase. This is derived from full Sobolev comparison.

    lemma firstVariation_of_comparison [IsFiniteMeasure (volume.restrict D)]
        {u φ : Space d → ℝ} {G : Space d → Space d}
        (hu : H1 D u G) (hu0 : ∀ᵐ x ∂volume.restrict D, 0 ≤ u x)
        (hmin : ∀ (v : Space d → ℝ) (V : Space d → Space d),
          H1 D v V → (∀ᵐ x ∂volume.restrict D, 0 ≤ v x) →
          H10 D (fun x => v x - u x) (fun x => V x - G x) →
          energy D u G ≤ energy D v V)
        (hφ : Test D φ) {δ : ℝ} (hδ : 0 < δ)
        (hpos : ∀ᵐ x ∂volume.restrict D, x ∈ tsupport φ → δ ≤ u x) :
        (∫ x in D, inner ℝ (G x) (gradient φ x)) = 0 := by
    …

    Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.H1, OAI.Bernoulli.H10, OAI.Bernoulli.energy, OAI.Bernoulli.Test

23. lemma OAI.Bernoulli.LocalMinimizer.firstVariation line 244
24. lemma OAI.Bernoulli.LocalMinimizer.weakHarmonic_of_continuous line 261

    Source documentation

    Once a continuous representative is obtained, every test compactly supported in its positive phase is an admissible two-sided variation.

    lemma LocalMinimizer.weakHarmonic_of_continuous {u : Space d → ℝ}
        (hu : LocalMinimizer D u) (hc : ContinuousOn u D) :
        ∃ G : Space d → Space d, H1Loc D u G ∧
          ∀ (c : Space d) (r : ℝ), 0 < r → Metric.closedBall c r ⊆ D →
          ∀ φ : Space d → ℝ, Test (Metric.ball c r ∩ {x | 0 < u x}) φ →
          (∫ x in Metric.ball c r, inner ℝ (G x) (gradient φ x)) = 0 := by
    …

    Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.LocalMinimizer, OAI.Bernoulli.H1Loc, OAI.Bernoulli.Test

25. lemma OAI.Bernoulli.OneHomogeneous.everywhere line 280
26. lemma OAI.Bernoulli.H1.gradient_unique line 297

    Source documentation

    The explicit gradient witnesses in the Sobolev definition are unique a.e. This uses Mathlib's fundamental lemma for compact smooth test functions.

    lemma H1.gradient_unique (hD : IsOpen D) (hG : H1 D u G) (hV : H1 D u V) :
        G =ᵐ[volume.restrict D] V := by
    …

    Mentions: OAI.Bernoulli.H1

27. lemma OAI.Bernoulli.integral_inner_bound line 334
28. lemma OAI.Bernoulli.Test.memLp_smul_const line 348
29. lemma OAI.Bernoulli.eq_zero_of_abs_lt line 356

    Source documentation

    Weak H¹ is closed for the actual L² norm on both components. This is used to zero-extend arbitrary H¹₀ competitors, not just smooth competitors.

    lemma eq_zero_of_abs_lt {z : ℝ} (h : ∀ ε : ℝ, 0 < ε → |z| < ε) : z = 0 := by
    …

30. lemma OAI.Bernoulli.weakGradient_of_approx line 360
31. lemma OAI.Bernoulli.WeakGradient.congr line 419
32. lemma OAI.Bernoulli.H1.congr line 435
33. lemma OAI.Bernoulli.H10.congr line 440
34. lemma OAI.Bernoulli.Test.fderiv_eq_zero_outside line 454
35. lemma OAI.Bernoulli.Test.mono line 458
36. lemma OAI.Bernoulli.H1.mono line 461
37. lemma OAI.Bernoulli.Test.mul line 476
38. lemma OAI.Bernoulli.Test.memLp_top line 480
39. lemma OAI.Bernoulli.Test.memLp_gradient_top line 484
40. lemma OAI.Bernoulli.Test.gradient_mul line 489
41. lemma OAI.Bernoulli.H1.mul_test line 504
42. lemma OAI.Bernoulli.energy_congr line 537
43. lemma OAI.Bernoulli.LocalMinimizer.congr line 543
44. lemma OAI.Bernoulli.LocalMinimizer.mono line 562
45. lemma OAI.Bernoulli.Test.gradient_eq_zero_outside line 572
46. lemma OAI.Bernoulli.H10.zero_extension line 579

    Source documentation

    Zero extension preserves the exact Sobolev norm of a zero-trace approximation; neither a smooth representative nor a boundary trace theorem is assumed.

    lemma H10.zero_extension (hu : H10 D u G) (hD : MeasurableSet D) (hDE : D ⊆ E) :
        H10 E (D.indicator u) (D.indicator G) := by
    …

    Mentions: OAI.Bernoulli.H10

47. lemma OAI.Bernoulli.eLpNorm_sub_lt_of_two line 616
48. lemma OAI.Bernoulli.H10.of_approx line 638
49. lemma OAI.Bernoulli.energy_split line 654
50. lemma OAI.Bernoulli.GlobalMinimizer.compare_bounded line 666
51. lemma OAI.Bernoulli.eLpNorm_two_eq_eLpNorm' line 721
52. lemma OAI.Bernoulli.eLpNorm_lt_of_bound line 726
53. lemma OAI.Bernoulli.eLpNorm_lt_of_bound_of_aestronglyMeasurable line 744
54. lemma OAI.Bernoulli.H10.mul_test line 759

    Source documentation

    Multiplying an arbitrary zero-trace Sobolev function by a smooth cutoff preserves zero trace, with the genuine weak product-rule gradient.

    lemma H10.mul_test (hu : H10 D u G) {φ : Space d → ℝ} (hφ : Test D φ) :
        H10 D (fun x => φ x * u x)
          (fun x => φ x • G x + u x • gradient φ x) := by
    …

    Mentions: OAI.Bernoulli.H10, OAI.Bernoulli.Space, OAI.Bernoulli.Test

55. abbrev OAI.Bernoulli.Mollification.Space line 823
56. def OAI.Bernoulli.Mollification.translate line 827

    Source documentation

    Translation on the actual Lebesgue L² space.

    def translate (f : Lp F 2 (volume : Measure (Space d))) (y : Space d) :
        Lp F 2 (volume : Measure (Space d)) :=
    …

    Mentions: OAI.Bernoulli.Mollification.Space

57. lemma OAI.Bernoulli.Mollification.continuous_translate line 831
58. lemma OAI.Bernoulli.Mollification.coeFn_translate line 840
59. lemma OAI.Bernoulli.Mollification.translate_zero line 844
60. lemma OAI.Bernoulli.Mollification.norm_translate line 849
61. lemma OAI.Bernoulli.Mollification.translate_toLp line 853
62. lemma OAI.Bernoulli.Mollification.eLpNorm_translate_tendsto line 861
63. lemma OAI.Bernoulli.Mollification.integrable_inner_of_memLp line 876
64. lemma OAI.Bernoulli.Mollification.integral_inner_bound line 883
65. lemma OAI.Bernoulli.Mollification.integral_norm_inner_bound line 898
66. lemma OAI.Bernoulli.Mollification.integrable_convolution_inner line 914

    Source documentation

    The Fubini integrability needed to compare a pointwise convolution with its Bochner integral in L². The testing function is arbitrary L².

    lemma integrable_convolution_inner {κ : Space d → ℝ} {f g : Space d → F}
        (hκ : Integrable κ volume) (hf : MemLp f 2 volume) (hg : MemLp g 2 volume) :
        Integrable (fun p : Space d × Space d =>
          inner ℝ (κ p.2 • f (p.1 - p.2)) (g p.1)) (volume.prod volume) := by
    …

    Mentions: OAI.Bernoulli.Mollification.Space

67. lemma OAI.Bernoulli.Mollification.memLp_convolution line 945
68. lemma OAI.Bernoulli.Mollification.convolution_toLp_eq_integral_translate line 955

    Source documentation

    A pointwise mollification is the same element of L² as the Bochner average of translates. This proof includes the Fubini and representative bridge.

    lemma convolution_toLp_eq_integral_translate {κ : Space d → ℝ} {f : Space d → F}
        (hκ : Continuous κ) (hcκ : HasCompactSupport κ)
        (hf : MemLp f 2 volume) (hcf : HasCompactSupport f) :
        (memLp_convolution hκ hcκ hf hcf).toLp
          (κ ⋆[ContinuousLinearMap.lsmul ℝ ℝ, volume] f) =
          ∫ y, κ y • translate (hf.toLp f) y := by
    …

    Mentions: OAI.Bernoulli.Mollification.Space, OAI.Bernoulli.Mollification.memLp_convolution, OAI.Bernoulli.Mollification.translate

69. lemma OAI.Bernoulli.Mollification.convolution_toLp_tendsto line 1001

    Source documentation

    L² convergence of compactly supported mollifications. It applies at once to the function and its weak gradient, once the weak derivative identity has been proved.

    lemma convolution_toLp_tendsto {ι : Type uι} {l : Filter ι}
        {φ : ι → ContDiffBump (0 : Space d)} {f : Space d → F}
        (hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0))
        (hf : MemLp f 2 volume) (hcf : HasCompactSupport f) :
        Tendsto (fun i => (memLp_convolution (φ i).continuous_normed
          (φ i).hasCompactSupport_normed hf hcf).toLp
            ((φ i).normed volume ⋆[ContinuousLinearMap.lsmul ℝ ℝ, volume] f)) l
          (𝓝 (hf.toLp f)) := by
    …

    Mentions: OAI.Bernoulli.Mollification.Space, OAI.Bernoulli.Mollification.memLp_convolution

70. lemma OAI.Bernoulli.Mollification.eLpNorm_convolution_sub_tendsto line 1022
71. lemma OAI.Bernoulli.SobolevDensity.test_reflected line 1050
72. lemma OAI.Bernoulli.SobolevDensity.fderiv_reflected line 1055
73. lemma OAI.Bernoulli.SobolevDensity.gradient_convolution line 1064
74. lemma OAI.Bernoulli.SobolevDensity.tsupport_convolution_subset line 1108
75. lemma OAI.Bernoulli.SobolevDensity.tsupport_mollification_subset line 1116
76. def OAI.Bernoulli.SobolevDensity.bumps line 1128

    Source documentation

    A fixed sequence of positive-radius smooth normalized mollifiers.

    def bumps (d : ℕ) (n : ℕ) : ContDiffBump (0 : Space d) where
    …

    Mentions: OAI.Bernoulli.Space

77. lemma OAI.Bernoulli.SobolevDensity.bumps_tendsto line 1137
78. lemma OAI.Bernoulli.SobolevDensity.h10_of_compact_support line 1142

    Source documentation

    Simultaneous weak-H¹ mollification, including support inside the open set. The gradient convergence is proved, not demanded of the approximants.

    lemma h10_of_compact_support {D : Set (Space d)} (hD : IsOpen D)
        {u : Space d → ℝ} {G : Space d → Space d}
        (hu : H1 univ u G) (hcu : HasCompactSupport u) (hcG : HasCompactSupport G)
        (hsu : tsupport u ⊆ D) : H10 D u G := by
    …

    Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.H1, OAI.Bernoulli.H10

79. lemma OAI.Bernoulli.SobolevDensity.memLp_global_of_zero_outside line 1187
80. lemma OAI.Bernoulli.SobolevDensity.h1_mul_test_global line 1200

    Source documentation

    A compactly supported smooth cutoff of a local weak H¹ function is a whole-space weak H¹ function, with the actual product-rule gradient.

    lemma h1_mul_test_global {u : Space d → ℝ} {G : Space d → Space d}
        (hu : H1 D u G) (hD : MeasurableSet D)
        {φ : Space d → ℝ} (hφ : Test D φ) :
        H1 univ (fun x => φ x * u x)
          (fun x => φ x • G x + u x • gradient φ x) := by
    …

    Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.H1, OAI.Bernoulli.Test

81. lemma OAI.Bernoulli.SobolevDensity.h10_mul_test line 1248
82. lemma OAI.Bernoulli.LipschitzSobolev.measurable_gradient line 1270
83. lemma OAI.Bernoulli.LipschitzSobolev.norm_gradient_le line 1274
84. lemma OAI.Bernoulli.LipschitzSobolev.weakGradient line 1279
85. lemma OAI.Bernoulli.LipschitzSobolev.h1_ball line 1302
86. lemma OAI.Bernoulli.LipschitzSobolev.compact_gradient line 1319
87. lemma OAI.Bernoulli.LipschitzSobolev.h1_compact line 1322
88. lemma OAI.Bernoulli.H1.sub line 1348
89. lemma OAI.Bernoulli.LipschitzSobolev.h10 line 1353
90. lemma OAI.Bernoulli.GlobalMinimizer.compare_lipschitz line 1361

    Source documentation

    Genuine Sobolev comparison, specialized only AFTER two explicit functions have been shown Lipschitz and their difference compactly supported.

    lemma GlobalMinimizer.compare_lipschitz {d : ℕ} {u v : Space d → ℝ} {K L : NNReal}
        (hm : GlobalMinimizer u) (hu : LipschitzWith K u) (hv : LipschitzWith L v)
        (c : Space d) {r : ℝ} (hr : 0 < r)
        (hn : ∀ᵐ x ∂volume.restrict (Metric.ball c r), 0 ≤ v x)
        (hc : HasCompactSupport (fun x => v x - u x))
        (hs : tsupport (fun x => v x - u x) ⊆ Metric.ball c r) :
        energy (Metric.ball c r) u (gradient u) ≤ energy (Metric.ball c r) v (gradient v) := by
    …

    Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.GlobalMinimizer, OAI.Bernoulli.energy

91. lemma OAI.Bernoulli.SobolevCalculus.H10_sequence line 1387

    Source documentation

    The closure definition itself provides smooth approximants converging simultaneously in both L² seminorms.

    lemma H10_sequence (hu : H10 D u G) :
        ∃ f : ℕ → Space d → ℝ, (∀ n, Test D (f n)) ∧
          Tendsto (fun n => eLpNorm (f n - u) 2 (volume.restrict D)) atTop (𝓝 0) ∧
          Tendsto (fun n => eLpNorm (gradient (f n) - G) 2 (volume.restrict D)) atTop (𝓝 0) := by
    …

    Mentions: OAI.Bernoulli.H10, OAI.Bernoulli.Space, OAI.Bernoulli.Test

92. lemma OAI.Bernoulli.SobolevCalculus.gradient_comp line 1410
93. lemma OAI.Bernoulli.SobolevCalculus.test_comp_h1 line 1418
94. lemma OAI.Bernoulli.SobolevCalculus.tendsto_eLpNorm_zero_of_dominated line 1433

    Source documentation

    L² dominated convergence, expressed in the same seminorms as H10.

    lemma tendsto_eLpNorm_zero_of_dominated {f : ℕ → α → E} {b : α → ℝ}
        (hf : ∀ n, AEStronglyMeasurable (f n) μ) (hb : MemLp b 2 μ)
        (hbound : ∀ n, ∀ᵐ x ∂μ, ‖f n x‖ ≤ ‖b x‖)
        (hlim : ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop (𝓝 0)) :
        Tendsto (fun n => eLpNorm (f n) 2 μ) atTop (𝓝 0) := by
    …

95. lemma OAI.Bernoulli.SobolevCalculus.test_comp_h10 line 1465
96. lemma OAI.Bernoulli.SobolevCalculus.h10_of_strong line 1476
97. lemma OAI.Bernoulli.SobolevCalculus.lipschitz_tendsto_eLpNorm line 1496
98. lemma OAI.Bernoulli.SobolevCalculus.lipschitz_tendsto_eLpNorm_of_aestronglyMeasurable line 1510
99. lemma OAI.Bernoulli.SobolevCalculus.bounded_smul_tendsto line 1522
100. lemma OAI.Bernoulli.SobolevCalculus.bounded_smul_strong line 1550
101. lemma OAI.Bernoulli.SobolevCalculus.h10_comp_C1 line 1585
102. def OAI.Bernoulli.SobolevCalculus.cutSlope line 1616
103. def OAI.Bernoulli.SobolevCalculus.cutPrimitive line 1618
104. lemma OAI.Bernoulli.SobolevCalculus.cutSlope_continuous line 1620
105. lemma OAI.Bernoulli.SobolevCalculus.cutSlope_nonneg line 1624
106. lemma OAI.Bernoulli.SobolevCalculus.cutSlope_le_one line 1627
107. lemma OAI.Bernoulli.SobolevCalculus.cutSlope_norm_le line 1629
108. lemma OAI.Bernoulli.SobolevCalculus.cutPrimitive_deriv line 1633
109. lemma OAI.Bernoulli.SobolevCalculus.cutPrimitive_contDiff line 1640
110. lemma OAI.Bernoulli.SobolevCalculus.cutPrimitive_lipschitz line 1648
111. lemma OAI.Bernoulli.SobolevCalculus.cutPrimitive_zero line 1654
112. lemma OAI.Bernoulli.SobolevCalculus.cutSlope_tendsto line 1657
113. lemma OAI.Bernoulli.SobolevCalculus.integral_step line 1676
114. lemma OAI.Bernoulli.SobolevCalculus.cutPrimitive_tendsto line 1695
115. lemma OAI.Bernoulli.SobolevCalculus.norm_positivePart line 1710
116. lemma OAI.Bernoulli.SobolevCalculus.step_memLp_top line 1714
117. lemma OAI.Bernoulli.SobolevCalculus.h10_positivePart line 1724
118. lemma OAI.Bernoulli.exists_cutoff line 1769
119. lemma OAI.Bernoulli.H1.neg line 1790
120. lemma OAI.Bernoulli.SobolevCalculus.h1_positivePart line 1799
121. lemma OAI.Bernoulli.SobolevCalculus.h10_of_local_compact_support line 1841

     Source documentation

     A compactly supported H¹ function in the open set has zero trace. No support or regularity condition is imposed on its given weak gradient.

     lemma h10_of_local_compact_support (hD : IsOpen D) (hu : H1 D u G)
         (hc : HasCompactSupport u) (hs : tsupport u ⊆ D) : H10 D u G := by
     …

     Mentions: OAI.Bernoulli.H1, OAI.Bernoulli.H10

122. lemma OAI.Bernoulli.SobolevCalculus.gradient_zero_on_zero_set line 1856

     Source documentation

     Stampacchia's zero-level-set property, obtained from the two truncations and distributional uniqueness.

     lemma gradient_zero_on_zero_set (hD : IsOpen D) (hu : H1 D u G) :
         ∀ᵐ x ∂volume.restrict D, u x = 0 → G x = 0 := by
     …

     Mentions: OAI.Bernoulli.H1

123. lemma OAI.Bernoulli.SobolevCalculus.bounded_smul_strong_of_fixed line 1878
124. lemma OAI.Bernoulli.SobolevCalculus.positivePart_gradient_strong_of_ae line 1912
125. lemma OAI.Bernoulli.SobolevCalculus.lipschitzWith_positivePart line 1951
126. lemma OAI.Bernoulli.SobolevCalculus.h10_positivePart_add_test line 1954
127. lemma OAI.Bernoulli.SobolevCalculus.h10_positivePart_trace_pointwise line 1969
128. lemma OAI.Bernoulli.SobolevCalculus.h10_positivePart_trace line 2015