noncomputable def Meas.embedMap (X : Type u_1) [TopologicalSpace X] (MX : Type u_2) [AddCommGroup MX] [Module ℂ MX] [TopologicalSpace MX] [CompactlySupportedMeasureSpace X MX] : (X →₀ ℂ) →ₗ[ℂ] MX

def Meas.atomicIn {X : Type u_1} [TopologicalSpace X] {MX : Type u_2} [AddCommGroup MX] [Module ℂ MX] [TopologicalSpace MX] [CompactlySupportedMeasureSpace X MX] (K : Set X) : Set MX

def Meas.IsSupportedIn {X : Type u_1} [TopologicalSpace X] {MX : Type u_2} [AddCommGroup MX] [Module ℂ MX] [TopologicalSpace MX] [CompactlySupportedMeasureSpace X MX] (μ : MX) (K : Set X) : Prop

def Meas.functionalSupp (X : Type u_1) [TopologicalSpace X] {MX : Type u_2} [AddCommGroup MX] [Module ℂ MX] [TopologicalSpace MX] [CompactlySupportedMeasureSpace X MX] (μ : MX) : Set X

instance ContinuousMap.instIsUniformAddGroupComplex {X : Type u_1} [TopologicalSpace X] : IsUniformAddGroup C(X, ℂ)

def ConcreteMeasSupp.IsSupportedIn {X : Type u_1} [TopologicalSpace X] (μ : C(X, ℂ) →L[ℂ] ℂ) (K : Set X) : Prop

def ConcreteMeasSupp.IsWeakStarCauchy {X : Type u_1} [TopologicalSpace X] (μ : ℕ → C(X, ℂ) →L[ℂ] ℂ) : Prop

def ConcreteMeasSupp.TendstoWeakStar {X : Type u_1} [TopologicalSpace X] (μ : ℕ → C(X, ℂ) →L[ℂ] ℂ) (μ₀ : C(X, ℂ) →L[ℂ] ℂ) : Prop

theorem ConcreteMeasSupp.cauchySeq_supportedIn_compact {X : Type u_2} [TopologicalSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] [T2Space X] (μ : ℕ → C(X, ℂ) →L[ℂ] ℂ) (hcauchy : IsWeakStarCauchy μ) : ∃ (K : Set X), IsCompact K ∧ ∀ (n : ℕ), IsSupportedIn (μ n) K

theorem ConcreteMeasSupp.pointwiseLimitOfCLM_continuous {X : Type u_2} [TopologicalSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] [T2Space X] (μ : ℕ → C(X, ℂ) →L[ℂ] ℂ) (g : C(X, ℂ) →ₗ[ℂ] ℂ) (hlim : ∀ (f : C(X, ℂ)), Filter.Tendsto (fun (n : ℕ) => (μ n) f) Filter.atTop (nhds (g f))) : Continuous ⇑g

theorem ConcreteMeasSupp.weakStarCauchyLimit_exists {X : Type u_2} [TopologicalSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] [T2Space X] (μ : ℕ → C(X, ℂ) →L[ℂ] ℂ) (_hcauchy : IsWeakStarCauchy μ) (_hlim : ∀ (f : C(X, ℂ)), ∃ (c : ℂ), Filter.Tendsto (fun (n : ℕ) => (μ n) f) Filter.atTop (nhds c)) : ∃ (μ₀ : C(X, ℂ) →L[ℂ] ℂ), TendstoWeakStar μ μ₀

theorem ConcreteMeasSupp.seqComplete {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] [T2Space X] (μ : ℕ → C(X, ℂ) →L[ℂ] ℂ) (hcauchy : IsWeakStarCauchy μ) : ∃ (K : Set X) (μ₀ : C(X, ℂ) →L[ℂ] ℂ), IsCompact K ∧ IsSupportedIn μ₀ K ∧ TendstoWeakStar μ μ₀

def ConcreteMeasSupp.functionalSupport {X : Type u_1} [TopologicalSpace X] (μ : C(X, ℂ) →L[ℂ] ℂ) : Set X

theorem ConcreteMeasSupp.isClosed_functionalSupport {X : Type u_1} [TopologicalSpace X] (μ : C(X, ℂ) →L[ℂ] ℂ) : IsClosed (functionalSupport μ)

theorem ConcreteMeasSupp.not_in_support_local_vanishing {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] [T2Space X] (μ : C(X, ℂ) →L[ℂ] ℂ) (x : X) (hx : x ∉ functionalSupport μ) : ∃ U ∈ nhds x, ∀ (g : C(X, ℂ)), (∀ y ∉ U, g y = 0) → μ g = 0

theorem ConcreteMeasSupp.exists_pou_subordinate_open {X : Type u_2} [TopologicalSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] [T2Space X] (S : Set X) (hS : IsOpen S) (U : X → Set X) (hUo : ∀ (x : X), IsOpen (U x)) (hUmem : ∀ x ∈ S, x ∈ U x) : ∃ (ρ : ℕ → C(X, ℝ)) (idx : ℕ → X), (∀ (n : ℕ), ρ n ≠ 0 → idx n ∈ S) ∧ (∀ (n : ℕ) (x : X), 0 ≤ (ρ n) x) ∧ (∀ (n : ℕ), tsupport ⇑(ρ n) ⊆ U (idx n)) ∧ (LocallyFinite fun (n : ℕ) => Function.support ⇑(ρ n)) ∧ ∀ x ∈ S, ∑ᶠ (n : ℕ), (ρ n) x = 1

noncomputable def ConcreteMeasSupp.toComplexCM : C(ℝ, ℂ)

theorem ConcreteMeasSupp.pou_decomposition {X : Type u_2} [TopologicalSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] [T2Space X] (S : Set X) (hS : IsOpen S) (f : C(X, ℂ)) (hfS : ∀ x ∉ S, f x = 0) (U : X → Set X) (hUo : ∀ (x : X), IsOpen (U x)) (hUmem : ∀ x ∈ S, x ∈ U x) : ∃ (g : ℕ → C(X, ℂ)) (idx : ℕ → X), (∀ (n : ℕ), g n ≠ 0 → idx n ∈ S) ∧ (∀ (n : ℕ), ∀ y ∉ U (idx n), (g n) y = 0) ∧ (LocallyFinite fun (n : ℕ) => Function.support ⇑(g n)) ∧ ∀ (x : X), HasSum (fun (n : ℕ) => (g n) x) (f x)

theorem ConcreteMeasSupp.pou_kills_functional {X : Type u_2} [TopologicalSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] [T2Space X] (μ : C(X, ℂ) →L[ℂ] ℂ) (f : C(X, ℂ)) (g : ℕ → C(X, ℂ)) (hlf : LocallyFinite fun (n : ℕ) => Function.support ⇑(g n)) (hpw : ∀ (x : X), HasSum (fun (n : ℕ) => (g n) x) (f x)) (hzero : ∀ (n : ℕ), μ (g n) = 0) : μ f = 0

theorem ConcreteMeasSupp.partitionOfUnity_kills_on_openSet {X : Type u_2} [TopologicalSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] [T2Space X] (μ : C(X, ℂ) →L[ℂ] ℂ) (f : C(X, ℂ)) (S : Set X) (hS : IsOpen S) (hfS : ∀ x ∉ S, f x = 0) (U : X → Set X) (hUo : ∀ (x : X), IsOpen (U x)) (hUmem : ∀ x ∈ S, x ∈ U x) (hUkill : ∀ x ∈ S, ∀ (g : C(X, ℂ)), (∀ y ∉ U x, g y = 0) → μ g = 0) : μ f = 0

theorem ConcreteMeasSupp.functional_kills_vanishing_on_closed_support {X : Type u_2} [TopologicalSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] [T2Space X] (μ : C(X, ℂ) →L[ℂ] ℂ) (f : C(X, ℂ)) (hf : ∀ x ∈ functionalSupport μ, f x = 0) (hloc : ∀ x ∉ functionalSupport μ, ∃ U ∈ nhds x, ∀ (g : C(X, ℂ)), (∀ y ∉ U, g y = 0) → μ g = 0) : μ f = 0

theorem ConcreteMeasSupp.prop_3_3_vanishing_on_support {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] [T2Space X] (μ : C(X, ℂ) →L[ℂ] ℂ) (f : C(X, ℂ)) (hf : ∀ x ∈ functionalSupport μ, f x = 0) : μ f = 0