Smoothness of a locally smooth representative

Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 3 (p. 334) is proved on balls: the Sobolev ladder runs inside a ball compactly contained in the region, and produces a smooth function agreeing almost everywhere with the solution there. The theorem is stated on the region. This file is the passage between the two, the only part of that argument with no analysis.

Two observations do the work.

• Agreement of the local representatives on their overlap. Both are continuous on the intersection of their balls, which is open, and agree almost everywhere with the same class there. A nonempty open set has positive Lebesgue measure, so two continuous functions agreeing almost everywhere on one agree on it.
• So no gluing is needed. Sending x to the value at x of the representative attached to x itself already agrees with every local representative on all of that representative's ball, by the previous point. Smoothness is then local, and the almost everywhere identity follows from a countable subcover.

Main declarations

• eqOn_of_ae_eq_of_continuousOn: continuous functions agreeing almost everywhere on an open set agree on it.
• exists_contDiffOn_of_locally_ae: local smooth representatives assemble into one.
• exists_contDiffOn_of_compact_ae: the same, with the local hypothesis stated over compact subsets rather than open balls, which is the shape a bootstrap run on a compact exhaustion supplies.
• exists_contDiffOn_of_closedBall_ae: the same, stated over closed balls, which is what a bootstrap such as interior_smooth supplies directly.

theorem EllipticPdes.Regularity.eqOn_of_ae_eq_of_continuousOn {d : ℕ} {W : Set (EuclideanSpace ℝ (Fin d))} (hW : IsOpen W) {f g : EuclideanSpace ℝ (Fin d) → ℝ} (hf : ContinuousOn f W) (hg : ContinuousOn g W) (hae : f =ᵐ[MeasureTheory.volume.restrict W] g) : Set.EqOn f g W

Almost everywhere equality upgrades to equality for continuous functions on an open set. Where they differ at a point they differ on an open neighbourhood, which has positive Lebesgue measure.

theorem EllipticPdes.Regularity.exists_contDiffOn_of_locally_ae {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (hUo : IsOpen U) (u : EuclideanSpace ℝ (Fin d) → ℝ) (h : ∀ x ∈ U, ∃ (B : Set (EuclideanSpace ℝ (Fin d))), IsOpen B ∧ x ∈ B ∧ B ⊆ U ∧ ∃ (v : EuclideanSpace ℝ (Fin d) → ℝ), ContDiffOn ℝ (↑⊤) v B ∧ v =ᵐ[MeasureTheory.volume.restrict B] u) : ∃ (u' : EuclideanSpace ℝ (Fin d) → ℝ), u' =ᵐ[MeasureTheory.volume.restrict U] u ∧ ContDiffOn ℝ (↑⊤) u' U

Local smooth representatives assemble into one. If every point of an open U has an open ball inside U on which some smooth function agrees almost everywhere with u, then a single smooth function does so on all of U.

No gluing construction appears. The value at x is taken from the representative attached to x, and eqOn_of_ae_eq_of_continuousOn makes that choice agree with every other representative on all of its own ball, which is what turns pointwise selection into a locally smooth function.

theorem EllipticPdes.Regularity.exists_contDiffOn_of_compact_ae {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (hUo : IsOpen U) (u : EuclideanSpace ℝ (Fin d) → ℝ) (h : ∀ (V : Set (EuclideanSpace ℝ (Fin d))), IsCompact V → V ⊆ U → ∃ (v : EuclideanSpace ℝ (Fin d) → ℝ), v =ᵐ[MeasureTheory.volume.restrict (interior V)] u ∧ ContDiffOn ℝ (↑⊤) v (interior V)) : ∃ (u' : EuclideanSpace ℝ (Fin d) → ℝ), u' =ᵐ[MeasureTheory.volume.restrict U] u ∧ ContDiffOn ℝ (↑⊤) u' U

Local smooth representatives on compact sets assemble into one. A version of exists_contDiffOn_of_locally_ae whose local hypothesis is stated over compact subsets of U rather than open balls: if every compact V ⊆ U has a smooth representative agreeing with u almost everywhere on the interior of V, then a single smooth function does so on all of U. This is the shape a bootstrap run on a compact exhaustion, such as interior_smooth, supplies its conclusion in, one exhaustion piece at a time, with nothing relating two different pieces; interior_smooth_global glues them through this lemma into one representative on the whole region.

theorem EllipticPdes.Regularity.exists_contDiffOn_of_closedBall_ae {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (hUo : IsOpen U) (u : EuclideanSpace ℝ (Fin d) → ℝ) (h : ∀ (x : EuclideanSpace ℝ (Fin d)) (r : ℝ), 0 < r → Metric.closedBall x r ⊆ U → ∃ (v : EuclideanSpace ℝ (Fin d) → ℝ), v =ᵐ[MeasureTheory.volume.restrict (Metric.ball x r)] u ∧ ContDiffOn ℝ (↑⊤) v (Metric.ball x r)) : ∃ (u' : EuclideanSpace ℝ (Fin d) → ℝ), u' =ᵐ[MeasureTheory.volume.restrict U] u ∧ ContDiffOn ℝ (↑⊤) u' U

A version of exists_contDiffOn_of_compact_ae asking only for closed balls, which is what the local hypotheses of a difference-quotient bootstrap supply directly, with no compact set to name first.