Infinite differentiability on the whole of the interior

interior_smooth produces a smooth representative on the interior of each compact V ⋐ Ω separately, with nothing relating the representatives two different choices of V supply. This file glues them into a single function smooth on the whole of Ω.

The gluing needs no construction of its own. Two representatives, one for a compact V₁ and one for a compact V₂, are continuous and agree almost everywhere with the same class wherever their interiors meet, so they agree there; exists_contDiffOn_of_compact_ae is exactly this fact packaged for a hypothesis stated over every compact subset of Ω at once, and applying it to the family interior_smooth supplies is the whole proof.

Main declarations

• interior_smooth_global: Evans's Theorem 3, with one representative smooth on all of Ω rather than on the interior of each compact exhaustion piece.

theorem EllipticPdes.Regularity.interior_smooth_global {n : ℕ} (Op : Sobolev.FullEllipticOp (n + 1)) {Ω : Set (EuclideanSpace ℝ (Fin (n + 1)))} (hΩm : MeasurableSet Ω) (hΩo : IsOpen Ω) (hA1 : IsLipCoeff Op.toEllipticCoeff) (hA : (k : ℕ) → IsWkInftyCoeff Op.toEllipticCoeff k) (hbc : (k : ℕ) → IsWkInftyLower Op k) (u : ↥(Sobolev.H01 Ω)) (f : Sobolev.L2D Ω) (hf : ∀ (k : ℕ), ∃ (hfk : HasIteratedWeakDerivOn Ω k f) (M : ℝ), IteratedL2Bound hfk M) (hweak : ∀ (w : ↥(Sobolev.H01 Ω)), ((Op.fullBilin Ω) u) w = ∫ (x : EuclideanSpace ℝ (Fin (n + 1))) in Ω, ↑↑f x * ↑↑((↑w).ofLp 0) x) : ∃ (u' : EuclideanSpace ℝ (Fin (n + 1)) → ℝ), u' =ᵐ[MeasureTheory.volume.restrict Ω] ↑↑((extendL2 hΩm) ((↑u).ofLp 0)) ∧ ContDiffOn ℝ (↑⊤) u' Ω

Infinite differentiability in the interior (Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 3, p. 334), with one representative on all of Ω. Under the hypotheses of interior_smooth, the local representatives on the interior of every compact V ⊆ Ω agree on the interiors they share, so exists_contDiffOn_of_compact_ae assembles them into a single function smooth on the whole open set Ω, rather than merely on the interior of each compact subset in turn.