Exact source: MathlibAnnex/Analysis/Distribution/WeakGradient/Local.lean
Pinned GitHub source · Raw UTF-8 source
Back to Zero weak gradient gives zero derivatives of local mollifications
1import MathlibAnnex.Analysis.Distribution.WeakGradient.Basic2import Mathlib.Analysis.Calculus.BumpFunction.Convolution3import Mathlib.Analysis.Calculus.ContDiff.Convolution4import Mathlib.Analysis.Calculus.MeanValue5import Mathlib.Tactic67/-! Interior compact localization and mollification. Arbitrary directions replace8coordinate basis vectors, so the proof works in any finite-dimensional real9normed space with a specified additive Haar measure. The parent RET2 source10was independently elaborated; this API-repair revision is qualified by the exact build evidence accompanying this source. -/11noncomputable section12open Set Metric MeasureTheory Filter TopologicalSpace ContinuousLinearMap13open scoped ENNReal Topology Convolution BigOperators14namespace MathlibAnnex.WeakGradient15variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]16 [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]17variable {μ : Measure E} [μ.IsAddHaarMeasure]1819/-- A quantitative ball contained in an open set. -/20structure LocalBallData (U : Set E) (x : E) where21 radius : ℝ22 radius_pos : 0 < radius23 closed_four_subset : closedBall x (4 * radius) ⊆ U2425namespace LocalBallData2627variable {U : Set E} {x : E}2829/-- Inner open ball on which local constancy will be proved. -/30def inner (D : LocalBallData U x) : Set E := ball x D.radius3132/-- Compact carrier used to localize the merely locally integrable function. -/33def carrier (D : LocalBallData U x) : Set E := closedBall x (4 * D.radius)3435/-- Intermediate carrier containing every translated mollifier used above the36inner ball. -/37def middle (D : LocalBallData U x) : Set E := closedBall x (2 * D.radius)3839@[simp] theorem center_mem_inner (D : LocalBallData U x) : x ∈ D.inner := by40 exact mem_ball_self D.radius_pos4142 theorem isOpen_inner (D : LocalBallData U x) : IsOpen D.inner := isOpen_ball4344 theorem inner_nonempty (D : LocalBallData U x) : D.inner.Nonempty :=45 ⟨x, D.center_mem_inner⟩4647 theorem isCompact_carrier (D : LocalBallData U x) : IsCompact D.carrier :=48 isCompact_closedBall _ _4950 theorem measurableSet_carrier (D : LocalBallData U x) : MeasurableSet D.carrier :=51 measurableSet_closedBall5253 theorem carrier_subset (D : LocalBallData U x) : D.carrier ⊆ U :=54 D.closed_four_subset5556 theorem inner_subset_carrier (D : LocalBallData U x) : D.inner ⊆ D.carrier := by57 intro y hy58 change dist y x < D.radius at hy59 exact mem_closedBall.mpr60 (hy.le.trans (by nlinarith [D.radius_pos]))6162/-- A translated support of radius at most `D.radius` above an inner-ball point63is contained in the intermediate closed ball. -/64theorem translated_closedBall_subset_middle (D : LocalBallData U x)65 {y : E} (hy : y ∈ D.inner) {ρ : ℝ} (_hρ0 : 0 ≤ ρ)66 (hρ : ρ ≤ D.radius) : closedBall y ρ ⊆ D.middle := by67 change dist y x < D.radius at hy68 intro z hz69 have hzy : dist z y ≤ ρ := mem_closedBall.mp hz70 have hyx : dist y x < D.radius := hy71 have hzx : dist z x < 2 * D.radius := by72 calc73 dist z x ≤ dist z y + dist y x := dist_triangle _ _ _74 _ < ρ + D.radius := add_lt_add_of_le_of_lt hzy hyx75 _ ≤ 2 * D.radius := by nlinarith76 exact mem_closedBall.mpr hzx.le7778 theorem middle_subset_carrier (D : LocalBallData U x) : D.middle ⊆ D.carrier := by79 intro y hy80 have h : dist y x ≤ 2 * D.radius := mem_closedBall.mp hy81 exact mem_closedBall.mpr (h.trans (by nlinarith [D.radius_pos]))8283 theorem middle_subset_open (D : LocalBallData U x) : D.middle ⊆ U :=84 D.middle_subset_carrier.trans D.carrier_subset8586end LocalBallData8788/-- Every point of an open set has a quantitative local ball. -/89theorem nonempty_localBallData {U : Set E}90 (hU : IsOpen U) {x : E} (hx : x ∈ U) :91 Nonempty (LocalBallData U x) := by9293 rcases Metric.isOpen_iff.1 hU x hx with ⟨r, hr, hrU⟩94 let ρ := r / 895 have hρ : 0 < ρ := by dsimp [ρ]; positivity96 refine ⟨{ radius := ρ, radius_pos := hρ, closed_four_subset := ?_ }⟩97 intro y hy98 apply hrU99 have hyx : dist y x ≤ 4 * ρ := mem_closedBall.mp hy100 have : 4 * ρ < r := by dsimp [ρ]; nlinarith101 exact mem_ball.mpr (hyx.trans_lt this)102103/-- Zero extension of `u` from a measurable compact carrier. -/104def compactLocalization (K : Set E)105 (u : E → ℝ) : E → ℝ := K.indicator u106107@[simp] theorem compactLocalization_of_mem108 {K : Set E} {u : E → ℝ} {x : E} (hx : x ∈ K) :109 compactLocalization K u x = u x := by simp [compactLocalization, hx]110111@[simp] theorem compactLocalization_of_not_mem112 {K : Set E} {u : E → ℝ} {x : E} (hx : x ∉ K) :113 compactLocalization K u x = 0 := by simp [compactLocalization, hx]114115/-- Local integrability on `U` gives integrability on a compact subset of `U`. -/116theorem integrableOn_localBallCarrier {U : Set E}117 {u : E → ℝ} (hu : LocallyIntegrableOn u U μ)118 {x : E} (D : LocalBallData U x) :119 IntegrableOn u D.carrier μ := by120 exact hu.integrableOn_compact_subset D.carrier_subset D.isCompact_carrier121122/-- The compact localization is globally integrable. -/123theorem integrable_compactLocalization {U : Set E}124 {u : E → ℝ} (hu : LocallyIntegrableOn u U μ)125 {x : E} (D : LocalBallData U x) :126 Integrable (compactLocalization D.carrier u) μ := by127128 rw [compactLocalization, integrable_indicator_iff D.measurableSet_carrier]129 exact integrableOn_localBallCarrier hu D130131/-- Hence the compact localization is globally locally integrable. -/132theorem locallyIntegrable_compactLocalization {U : Set E}133 {u : E → ℝ} (hu : LocallyIntegrableOn u U μ)134 {x : E} (D : LocalBallData U x) :135 LocallyIntegrable (compactLocalization D.carrier u) μ :=136 (integrable_compactLocalization hu D).locallyIntegrable137138/-- On the inner ball, compact localization does not change the function. -/139theorem compactLocalization_eq_ae_inner {U : Set E}140 {u : E → ℝ} {x : E} (D : LocalBallData U x) :141 compactLocalization D.carrier u =ᵐ[μ.restrict D.inner] u := by142 filter_upwards [ae_restrict_mem (D.isOpen_inner.measurableSet)] with y hy143 exact compactLocalization_of_mem (D.inner_subset_carrier hy)144145146/-- Smooth bump centered at zero with explicit shrinking radii. -/147noncomputable def shrinkingBump (R : ℝ) (hR : 0 < R)148 (k : ℕ) : ContDiffBump (0 : E) where149 rIn := R / (2 * ((k + 2 : ℕ) : ℝ))150 rOut := R / (((k + 2 : ℕ) : ℝ))151 rIn_pos := by positivity152 rIn_lt_rOut := by153 have hk : 0 < ((k + 2 : ℕ) : ℝ) := by positivity154 apply (div_lt_div_iff₀ (mul_pos (by norm_num) hk) hk).2155 nlinarith [hR]156157@[simp] theorem shrinkingBump_rIn (R : ℝ) (hR : 0 < R) (k : ℕ) :158 (shrinkingBump (E := E) R hR k).rIn =159 R / (2 * ((k + 2 : ℕ) : ℝ)) := rfl160161@[simp] theorem shrinkingBump_rOut (R : ℝ) (hR : 0 < R) (k : ℕ) :162 (shrinkingBump (E := E) R hR k).rOut =163 R / (((k + 2 : ℕ) : ℝ)) := rfl164165/-- Uniform ratio required by the differentiation theorem. -/166theorem shrinkingBump_ratio (R : ℝ) (hR : 0 < R) (k : ℕ) :167 (shrinkingBump (E := E) R hR k).rOut ≤168 2 * (shrinkingBump (E := E) R hR k).rIn := by169 rw [shrinkingBump_rOut, shrinkingBump_rIn]170 have hk : (((k + 2 : ℕ) : ℝ)) ≠ 0 := by positivity171 apply le_of_eq172 field_simp [hk]173174/-- All outer radii are at most half of `R`. -/175theorem shrinkingBump_rOut_le_half (R : ℝ) (hR : 0 < R) (k : ℕ) :176 (shrinkingBump (E := E) R hR k).rOut ≤ R / 2 := by177 have hk : (2 : ℝ) ≤ ((k + 2 : ℕ) : ℝ) := by norm_num178 exact div_le_div_of_nonneg_left hR.le (by positivity) hk179180/-- Outer radii tend to zero. -/181theorem tendsto_shrinkingBump_rOut_zero (R : ℝ) (hR : 0 < R) :182 Tendsto (fun k : ℕ => (shrinkingBump (E := E) R hR k).rOut)183 atTop (𝓝 0) := by184185 have hnat : Tendsto (fun k : ℕ => k + 2) atTop atTop := by186 exact tendsto_add_atTop_nat 2187 have hcast :188 Tendsto (fun k : ℕ => (((k + 2 : ℕ) : ℝ))) atTop atTop :=189 (tendsto_natCast_atTop_iff).2 hnat190 have hinv : Tendsto (fun k : ℕ => (((k + 2 : ℕ) : ℝ))⁻¹)191 atTop (𝓝 0) := tendsto_inv_atTop_zero.comp hcast192 simpa [shrinkingBump, div_eq_mul_inv] using193 (tendsto_const_nhds.mul hinv)194195/-- The normalized mollification of a scalar function. -/196noncomputable def localMollification (R : ℝ) (hR : 0 < R)197 (v : E → ℝ) (k : ℕ) : E → ℝ :=198 (shrinkingBump (E := E) R hR k).normed μ ⋆[lsmul ℝ ℝ, μ] v199200/-- The controlled mollifications converge a.e. to every globally locally201integrable scalar function. -/202theorem ae_tendsto_localMollification (R : ℝ) (hR : 0 < R)203 {v : E → ℝ} (hv : LocallyIntegrable v μ) :204 ∀ᵐ y ∂μ,205 Tendsto (fun k : ℕ => localMollification (μ := μ) R hR v k y)206 atTop (𝓝 (v y)) := by207208 exact ContDiffBump.ae_convolution_tendsto_right_of_locallyIntegrable209 (tendsto_shrinkingBump_rOut_zero (E := E) R hR)210 (Eventually.of_forall fun k => shrinkingBump_ratio (E := E) R hR k)211 hv212213/-- Scalar normalized bump used in the `k`-th local mollification. -/214noncomputable def normalizedShrinkingBump (R : ℝ) (hR : 0 < R)215 (k : ℕ) : E → ℝ :=216 (shrinkingBump (E := E) R hR k).normed μ217218/-- Translated bump field in direction `e`. -/219noncomputable def translatedBumpField (R : ℝ) (hR : 0 < R)220 (k : ℕ) (y : E) (e : E) : CompactC1VectorField E :=221 CompactC1VectorField.ofSupport222 (fun z => normalizedShrinkingBump (μ := μ) R hR k (y - z) • e)223 (closedBall y (shrinkingBump (E := E) R hR k).rOut)224 (isCompact_closedBall _ _)225 (by226 intro z hz227 have hφ : normalizedShrinkingBump (μ := μ) R hR k (y - z) ≠ 0 := by228 intro hzero229 exact hz (by simp [hzero])230 have hsupp : y - z ∈ Function.support231 (normalizedShrinkingBump (μ := μ) R hR k) := hφ232 have hball : y - z ∈ ball (0 : E)233 (shrinkingBump (E := E) R hR k).rOut := by234235 simpa [normalizedShrinkingBump,236 ContDiffBump.support_normed_eq] using hsupp237 have : dist z y < (shrinkingBump (E := E) R hR k).rOut := by238 simpa [mem_ball, dist_eq_norm, norm_sub_rev] using hball239 exact mem_closedBall.mpr this.le240 )241 (by242243 exact (((shrinkingBump (E := E) R hR k).contDiff_normed244 (μ := μ) (n := (1 : ℕ∞))).comp245 (contDiff_const.sub contDiff_id)).smul contDiff_const)246247248/-- The translated field is supported inside `U` above an inner-ball point. -/249theorem translatedBumpField_carrier_subset250 {U : Set E} {x : E} (D : LocalBallData U x)251 {y : E} (hy : y ∈ D.inner) (k : ℕ) (e : E) :252 (translatedBumpField (μ := μ) D.radius D.radius_pos k y e).carrier ⊆ U := by253 intro z hz254 exact D.middle_subset_open255 (D.translated_closedBall_subset_middle hy256 (le_of_lt (shrinkingBump (E := E) D.radius D.radius_pos k).rOut_pos)257 ((shrinkingBump_rOut_le_half (E := E) D.radius D.radius_pos k).trans258 (by nlinarith [D.radius_pos])) hz)259260261/-- The translated field tests an arbitrary direction, not a selected basis. -/262theorem divergence_translatedBumpField263 (R : ℝ) (hR : 0 < R) (k : ℕ) (y z : E) (e : E) :264 divergence (translatedBumpField (μ := μ) R hR k y e) z =265 - fderiv ℝ (normalizedShrinkingBump (μ := μ) R hR k) (y - z) e := by266 apply divergence_sub_smul267 exact ((shrinkingBump (E := E) R hR k).contDiff_normed268 (μ := μ) (n := (1 : ℕ∞))).differentiable (by norm_num) (y - z)269270/-- Derivative of the mollification in one direction, written with271the same translated kernel as the weak test field. -/272theorem localMollification_fderiv_apply273 (R : ℝ) (hR : 0 < R) {v : E → ℝ}274 (hv : LocallyIntegrable v μ) (k : ℕ) (y : E) (e : E) :275 fderiv ℝ (localMollification (μ := μ) R hR v k) y (e) =276 ∫ z, v z *277 fderiv ℝ (normalizedShrinkingBump (μ := μ) R hR k) (y - z) (e) ∂μ := by278279 -- `HasCompactSupport.hasFDerivAt_convolution_left` differentiates the bump.280 -- The provider's Haar change-of-variable lemma rewrites the281 -- derivative convolution in the displayed `y-z` form.282 have hφc : HasCompactSupport283 (normalizedShrinkingBump (μ := μ) (E := E) R hR k) := by284 exact (shrinkingBump (E := E) R hR k).hasCompactSupport_normed285 have hφd : ContDiff ℝ 1286 (normalizedShrinkingBump (μ := μ) (E := E) R hR k) :=287 (shrinkingBump (E := E) R hR k).contDiff_normed288 (μ := μ) (n := (1 : ℕ∞))289 have hderiv := hφc.hasFDerivAt_convolution_left290 (lsmul ℝ ℝ) hφd hv y291 have hbase :=292 congrArg (fun L : E →L[ℝ] ℝ => L (e)) hderiv.fderiv293 change (fderiv ℝ294 ((normalizedShrinkingBump (μ := μ) (E := E) R hR k) ⋆[lsmul ℝ ℝ, μ] v) y)295 (e) = _296 rw [hbase]297 have hint := ((hφc.fderiv ℝ).convolutionExists_left298 (ContinuousLinearMap.precompL E (lsmul ℝ ℝ))299 (hφd.continuous_fderiv one_ne_zero) hv) y300 change Integrable (fun t : E =>301 (ContinuousLinearMap.precompL E (lsmul ℝ ℝ)302 (fderiv ℝ (normalizedShrinkingBump (μ := μ) (E := E) R hR k) t))303 (v (y - t))) μ at hint304 rw [MeasureTheory.convolution_def]305 rw [ContinuousLinearMap.integral_apply hint (e)]306 have hcv := (Measure.measurePreserving_sub_left μ y).integral_comp307 (MeasurableEquiv.subLeft y).measurableEmbedding308 (fun z : E => v z *309 fderiv ℝ (normalizedShrinkingBump (μ := μ) (E := E) R hR k)310 (y - z) (e))311 simpa [localMollification, normalizedShrinkingBump,312 ContinuousLinearMap.precompL_apply, MeasureTheory.convolution_def,313 sub_sub_cancel, mul_comm] using hcv314315316/-- The weak integral over `U` equals the corresponding whole-space integral317with the compact localization. -/318theorem weakIntegral_eq_localized_bumpIntegral319 {U : Set E} {u : E → ℝ}320 (hU : IsOpen U)321 (hweak : WeakDivergenceZero μ U u)322 {x : E} (D : LocalBallData U x)323 {y : E} (hy : y ∈ D.inner) (k : ℕ) (e : E) :324 ∫ z, compactLocalization D.carrier u z *325 divergence (translatedBumpField (μ := μ) D.radius D.radius_pos k y e) z ∂μ = 0 := by326 let W := translatedBumpField (μ := μ) D.radius D.radius_pos k y e327 have hWU : W.carrier ⊆ U :=328 translatedBumpField_carrier_subset D hy k e329 have hzero := hweak W hWU330 have hsupport : ∀ᵐ z ∂μ,331 compactLocalization D.carrier u z * divergence W z =332 (U.indicator fun z => u z * divergence W z) z := by333 filter_upwards with z334 by_cases hzW : z ∈ W.carrier335 · have hzK : z ∈ D.carrier := by336 exact D.middle_subset_carrier337 (D.translated_closedBall_subset_middle hy338 (le_of_lt (shrinkingBump (E := E) D.radius D.radius_pos k).rOut_pos)339 ((shrinkingBump_rOut_le_half (E := E) D.radius D.radius_pos k).trans340 (by nlinarith [D.radius_pos])) hzW)341 have hzU : z ∈ U := hWU hzW342 simp [compactLocalization, hzK, hzU]343 · have hdiv : divergence W z = 0 := by344345 -- Closedness of the compact carrier gives a zero neighborhood.346 have hfd := W.fderiv_eq_zero_of_not_mem_carrier hzW347 simp [divergence, hfd]348 rw [hdiv]349 by_cases hzU : z ∈ U <;> simp [hzU, hdiv]350 rw [integral_congr_ae hsupport]351 simpa [MeasureTheory.integral_indicator hU.measurableSet] using hzero352353/-- Every directional derivative of the local mollification vanishes on the354inner ball. -/355theorem localMollification_fderiv_apply_eq_zero356 {U : Set E} {u : E → ℝ}357 (hU : IsOpen U)358 (hu : LocallyIntegrableOn u U μ)359 (hweak : WeakDivergenceZero μ U u)360 {x : E} (D : LocalBallData U x)361 {y : E} (hy : y ∈ D.inner) (k : ℕ) (e : E) :362 fderiv ℝ363 (localMollification (μ := μ) D.radius D.radius_pos364 (compactLocalization D.carrier u) k) y (e) = 0 := by365 rw [localMollification_fderiv_apply D.radius D.radius_pos366 (locallyIntegrable_compactLocalization hu D) k y e]367 have hweak0 := weakIntegral_eq_localized_bumpIntegral hU hweak D hy k e368 simp_rw [divergence_translatedBumpField] at hweak0369 have hneg : -(∫ z, compactLocalization D.carrier u z *370 fderiv ℝ (normalizedShrinkingBump (μ := μ) D.radius D.radius_pos k)371 (y - z) (e) ∂μ) = 0 := by372 simpa only [mul_neg, integral_neg] using hweak0373 exact neg_eq_zero.mp hneg374375/-- Vanishing in every direction is vanishing of the full derivative. -/376theorem localMollification_fderiv_eq_zero377 {U : Set E} {u : E → ℝ} (hU : IsOpen U)378 (hu : LocallyIntegrableOn u U μ) (hweak : WeakDivergenceZero μ U u)379 {x : E} (D : LocalBallData U x) (k : ℕ) :380 Set.EqOn (fderiv ℝ (localMollification (μ := μ) D.radius D.radius_pos381 (compactLocalization D.carrier u) k)) 0 D.inner := by382 intro y hy383 apply ContinuousLinearMap.ext384 intro e385 exact localMollification_fderiv_apply_eq_zero hU hu hweak D hy k e386387/-- The local mollification is smooth. -/388theorem contDiff_localMollification389 {U : Set E} {u : E → ℝ}390 (hu : LocallyIntegrableOn u U μ)391 {x : E} (D : LocalBallData U x) (k : ℕ) :392 ContDiff ℝ (⊤ : ℕ∞)393 (localMollification (μ := μ) D.radius D.radius_pos394 (compactLocalization D.carrier u) k) := by395396 exact (shrinkingBump (E := E) D.radius D.radius_pos k).hasCompactSupport_normed397 |>.contDiff_convolution_left (lsmul ℝ ℝ)398 ((shrinkingBump (E := E) D.radius D.radius_pos k).contDiff_normed399 (μ := μ) (n := (⊤ : ℕ∞)))400 (locallyIntegrable_compactLocalization hu D)401402/-- Each mollification is pointwise constant on the connected inner ball. -/403theorem exists_localMollification_constant404 {U : Set E} {u : E → ℝ}405 (hU : IsOpen U)406 (hu : LocallyIntegrableOn u U μ)407 (hweak : WeakDivergenceZero μ U u)408 {x : E} (D : LocalBallData U x) (k : ℕ) :409 ∃ c : ℝ, ∀ y ∈ D.inner,410 localMollification (μ := μ) D.radius D.radius_pos411 (compactLocalization D.carrier u) k y = c := by412 have hsmooth := contDiff_localMollification hu D k413 exact D.isOpen_inner.exists_is_const_of_fderiv_eq_zero414 (convex_ball x D.radius |>.isPreconnected)415 (hsmooth.differentiable (by simp)).differentiableOn416 (localMollification_fderiv_eq_zero hU hu hweak D k)417418419/-- Inner balls have positive Haar measure. -/420theorem localBall_inner_measure_pos {U : Set E}421 {x : E} (D : LocalBallData U x) : 0 < μ D.inner := by422 exact D.isOpen_inner.measure_pos μ D.inner_nonempty423424/-- There is a convergence point of the mollifier sequence inside the inner425ball. -/426theorem exists_inner_convergencePoint {U : Set E}427 {u : E → ℝ} (hu : LocallyIntegrableOn u U μ)428 {x : E} (D : LocalBallData U x) :429 ∃ y₀ ∈ D.inner,430 Tendsto431 (fun k : ℕ => localMollification (μ := μ) D.radius D.radius_pos432 (compactLocalization D.carrier u) k y₀)433 atTop (𝓝 (compactLocalization D.carrier u y₀)) := by434 have hconv := ae_tendsto_localMollification D.radius D.radius_pos435 (locallyIntegrable_compactLocalization hu D)436 have hconvInner : ∀ᵐ y ∂μ.restrict D.inner,437 Tendsto438 (fun k : ℕ => localMollification (μ := μ) D.radius D.radius_pos439 (compactLocalization D.carrier u) k y)440 atTop (𝓝 (compactLocalization D.carrier u y)) :=441 ae_restrict_of_ae hconv442 have hmem : ∀ᵐ y ∂μ.restrict D.inner, y ∈ D.inner :=443 ae_restrict_mem D.isOpen_inner.measurableSet444 have hpos := localBall_inner_measure_pos (μ := μ) D445 haveI : (ae (μ.restrict D.inner)).NeBot :=446 MeasureTheory.ae_restrict_neBot.mpr hpos.ne'447448 -- Select a common convergence point in the positive-measure ball.449 obtain ⟨y₀, hcy, hy₀⟩ :=450 (hconvInner.and hmem).exists451 exact ⟨y₀, hy₀, hcy⟩452453/-- Equality of every mollified value on the inner ball. -/454theorem localMollification_eq_at_inner_points455 {U : Set E} {u : E → ℝ}456 (hU : IsOpen U)457 (hu : LocallyIntegrableOn u U μ)458 (hweak : WeakDivergenceZero μ U u)459 {x : E} (D : LocalBallData U x)460 {y z : E} (hy : y ∈ D.inner) (hz : z ∈ D.inner) (k : ℕ) :461 localMollification (μ := μ) D.radius D.radius_pos462 (compactLocalization D.carrier u) k y =463 localMollification (μ := μ) D.radius D.radius_pos464 (compactLocalization D.carrier u) k z := by465 rcases exists_localMollification_constant hU hu hweak D k with ⟨c, hc⟩466 exact (hc y hy).trans (hc z hz).symm467468/-- The compact localization is a.e. constant on the inner ball. -/469theorem compactLocalization_aeConstant_inner470 {U : Set E} (hU : IsOpen U)471 {u : E → ℝ}472 (hu : LocallyIntegrableOn u U μ)473 (hweak : WeakDivergenceZero μ U u)474 {x : E} (D : LocalBallData U x) :475 ∃ c : ℝ, AEConstantOn μ476 (compactLocalization D.carrier u) D.inner c := by477 rcases exists_inner_convergencePoint hu D with ⟨y₀, hy₀, hconv₀⟩478 refine ⟨compactLocalization D.carrier u y₀, ?_⟩479 have hconv := ae_tendsto_localMollification D.radius D.radius_pos480 (locallyIntegrable_compactLocalization hu D)481 have hconvInner : ∀ᵐ y ∂μ.restrict D.inner,482 Tendsto483 (fun k : ℕ => localMollification (μ := μ) D.radius D.radius_pos484 (compactLocalization D.carrier u) k y)485 atTop (𝓝 (compactLocalization D.carrier u y)) :=486 ae_restrict_of_ae hconv487 filter_upwards [hconvInner,488 ae_restrict_mem D.isOpen_inner.measurableSet] with y hconvy hy489 have heq :490 (fun k : ℕ => localMollification (μ := μ) D.radius D.radius_pos491 (compactLocalization D.carrier u) k y) =492 (fun k : ℕ => localMollification (μ := μ) D.radius D.radius_pos493 (compactLocalization D.carrier u) k y₀) := by494 funext k495 exact localMollification_eq_at_inner_points hU hu hweak D hy hy₀ k496 have hconv₀' : Tendsto497 (fun k : ℕ => localMollification (μ := μ) D.radius D.radius_pos498 (compactLocalization D.carrier u) k y)499 atTop (𝓝 (compactLocalization D.carrier u y₀)) := by500 simpa [heq] using hconv₀501 exact tendsto_nhds_unique hconvy hconv₀' 502503/-- The original function is a.e. constant on the same inner ball. -/504theorem exists_aeConstant_inner505 {U : Set E} (hU : IsOpen U)506 {u : E → ℝ}507 (hu : LocallyIntegrableOn u U μ)508 (hweak : WeakDivergenceZero μ U u)509 {x : E} (D : LocalBallData U x) :510 ∃ c : ℝ, AEConstantOn μ u D.inner c := by511 rcases compactLocalization_aeConstant_inner hU hu hweak D with ⟨c, hc⟩512 refine ⟨c, ?_⟩513 exact (compactLocalization_eq_ae_inner D).symm.trans hc514515/-- Every point has an open neighborhood on which the function is a.e.516constant. -/517theorem nonempty_localAEConstantAt518 {U : Set E} (hU : IsOpen U)519 {u : E → ℝ}520 (hu : LocallyIntegrableOn u U μ)521 (hweak : WeakDivergenceZero μ U u)522 {x : E} (hx : x ∈ U) :523 Nonempty (LocalAEConstantAt μ U u x) := by524 rcases nonempty_localBallData hU hx with ⟨D⟩525 rcases exists_aeConstant_inner hU hu hweak D with ⟨c, hc⟩526 refine ⟨{527 neighborhood := D.inner528 isOpen_neighborhood := D.isOpen_inner529 mem_neighborhood := D.center_mem_inner530 neighborhood_subset := D.inner_subset_carrier.trans D.carrier_subset531 constant := c532 ae_eq := hc }⟩533534535end MathlibAnnex.WeakGradient