Gluing local Cⁿ representatives

A function that agrees almost everywhere near each point of a set Ω with a Cⁿ function agrees almost everywhere on all of Ω with a single function that is Cⁿ on Ω. The set Ω is arbitrary; the typical case is an open domain. Two local representatives are continuous and agree almost everywhere on their common open domain, so for a measure that charges every nonempty open set they agree everywhere there (MeasureTheory.Measure.eqOn_open_of_ae_eq). The value at y of any representative near y therefore defines the glued function on Ω; outside Ω it is u itself, so its exceptional set lies in Ω. Second countability turns the local almost everywhere equalities into a global one (MeasureTheory.measure_null_of_locally_null).

This is how regularity proved locally, for instance by multiplying a Sobolev function by cutoffs, becomes regularity of one representative on the whole domain. The case n = 0 glues continuous representatives.

Main results

• TauCeti.exists_contDiffOn_ae_eq_of_locally: local Cⁿ representatives glue to a Cⁿ representative on Ω.

theorem TauCeti.exists_contDiffOn_ae_eq_of_locally {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [MeasurableSpace E] [SecondCountableTopology E] {μ : MeasureTheory.Measure E} [μ.IsOpenPosMeasure] {n : WithTop ℕ∞} {u : E → F} {Ω : Set E} (h : ∀ x ∈ Ω, ∃ U ∈ nhds x, ∃ (g : E → F), ContDiffOn 𝕜 n g U ∧ u =ᵐ[μ.restrict U] g) : ∃ (g : E → F), ContDiffOn 𝕜 n g Ω ∧ u =ᵐ[μ.restrict Ω] g

Gluing local Cⁿ representatives. If near each point of the set Ω the function u agrees almost everywhere with a function that is Cⁿ on a neighbourhood of that point, then u agrees almost everywhere on Ω with a single function that is Cⁿ on Ω. The measure must charge every nonempty open set.