Exact source: MathlibAnnex/Analysis/Distribution/TestField.lean
Pinned GitHub source · Raw UTF-8 source
Back to Zero weak gradient gives zero derivatives of local mollifications
1import Mathlib.Analysis.Distribution.ContDiffMapSupportedIn23/-! Compact C¹ test fields. A variable compact carrier packages the existing4`ContDiffMapSupportedIn` provider; no duplicate regularity/support structure.5The parent RET2 source was independently elaborated. This bounded API-repair6revision is qualified by the exact build evidence accompanying this source. -/78noncomputable section9open Set TopologicalSpace1011namespace MathlibAnnex1213/-- A C¹ vector field together with one compact set containing its support. -/14abbrev CompactC1VectorField (E : Type*) [NormedAddCommGroup E] [NormedSpace ℝ E] :=15 Σ K : Compacts E, ContDiffMapSupportedIn E E 1 K1617namespace CompactC1VectorField18variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]1920instance : CoeFun (CompactC1VectorField E) (fun _ => E → E) :=21 ⟨fun W => W.2⟩2223/-- The chosen compact carrier; it need not equal topological support. -/24def carrier (W : CompactC1VectorField E) : Set E := W.12526theorem isCompact_carrier (W : CompactC1VectorField E) : IsCompact W.carrier :=27 W.1.isCompact2829theorem support_subset (W : CompactC1VectorField E) : Function.support W ⊆ W.carrier :=30 W.2.support_subset3132theorem tsupport_subset (W : CompactC1VectorField E) : tsupport W ⊆ W.carrier :=33 W.2.tsupport_subset3435theorem contDiff (W : CompactC1VectorField E) : ContDiff ℝ 1 W := W.2.contDiff3637theorem continuous (W : CompactC1VectorField E) : Continuous W := W.contDiff.continuous3839theorem hasCompactSupport (W : CompactC1VectorField E) : HasCompactSupport W :=40 W.2.hasCompactSupport4142/-- Construct a variable-carrier field using the existing fixed-carrier provider. -/43def ofSupport (f : E → E) (K : Set E) (hK : IsCompact K)44 (hs : Function.support f ⊆ K) (hf : ContDiff ℝ 1 f) : CompactC1VectorField E :=45 ⟨⟨K, hK⟩, ContDiffMapSupportedIn.of_support_subset hf hs⟩4647@[simp] theorem ofSupport_apply (f : E → E) (K : Set E) (hK : IsCompact K)48 (hs : Function.support f ⊆ K) (hf : ContDiff ℝ 1 f) (x : E) :49 ofSupport f K hK hs hf x = f x := rfl5051@[simp] theorem carrier_ofSupport (f : E → E) (K : Set E) (hK : IsCompact K)52 (hs : Function.support f ⊆ K) (hf : ContDiff ℝ 1 f) :53 (ofSupport f K hK hs hf).carrier = K := rfl5455/-- A field vanishes, with its derivative, off its closed compact carrier. -/56theorem fderiv_eq_zero_of_not_mem_carrier (W : CompactC1VectorField E)57 {x : E} (hx : x ∉ W.carrier) : fderiv ℝ W x = 0 := by58 exact fderiv_of_notMem_tsupport ℝ (fun h => hx (W.tsupport_subset h))5960end CompactC1VectorField61end MathlibAnnex