class CompactlySupportedMeasureSpace (X : Type u_1) [TopologicalSpace X] (MX : Type u_2) [AddCommGroup MX] [Module ℂ MX] [TopologicalSpace MX] : Type (max u_1 u_2)

• dirac : X → MX
• evalPairing : MX →ₗ[ℂ] C(X, ℂ) →ₗ[ℂ] ℂ
• evalPairing_dirac (x : X) (f : C(X, ℂ)) : (evalPairing (dirac x)) f = f x
• evalPairing_continuous (f : C(X, ℂ)) : Continuous fun (μ : MX) => (evalPairing μ) f
• hasCompactSupport (μ : MX) : ∃ (K : Set X), IsCompact K ∧ ∀ (f : C(X, ℂ)), (∀ x ∈ K, f x = 0) → (evalPairing μ) f = 0
• topology_eq_initial (μ : MX) : nhds μ = ⨅ (f : C(X, ℂ)), Filter.comap (fun (ν : MX) => (evalPairing ν) f) (nhds ((evalPairing μ) f))

theorem linear_func_decomp_pi_abstract {ι : Type u_1} [Fintype ι] [DecidableEq ι] (l : (ι → ℂ) →ₗ[ℂ] ℂ) (w : ι → ℂ) : l w = ∑ i : ι, l (Function.update 0 i 1) * w i

theorem evalPairing_linearCombination_dirac {X : Type u_1} [TopologicalSpace X] {MX : Type u_2} [AddCommGroup MX] [Module ℂ MX] [TopologicalSpace MX] [inst : CompactlySupportedMeasureSpace X MX] (c : X →₀ ℂ) (f : C(X, ℂ)) : (CompactlySupportedMeasureSpace.evalPairing ((Finsupp.linearCombination ℂ CompactlySupportedMeasureSpace.dirac) c)) f = c.sum fun (x : X) (a : ℂ) => a * f x

theorem abstract_match_on_finset_restricted {X : Type u_1} [TopologicalSpace X] {MX : Type u_2} [AddCommGroup MX] [Module ℂ MX] [TopologicalSpace MX] [inst : CompactlySupportedMeasureSpace X MX] (μ : MX) (K : Set X) (hK : ∀ (f : C(X, ℂ)), (∀ x ∈ K, f x = 0) → (CompactlySupportedMeasureSpace.evalPairing μ) f = 0) (I : Finset C(X, ℂ)) : ∃ (c : X →₀ ℂ), ↑c.support ⊆ K ∧ ∀ f ∈ I, (CompactlySupportedMeasureSpace.evalPairing ((Finsupp.linearCombination ℂ CompactlySupportedMeasureSpace.dirac) c)) f = (CompactlySupportedMeasureSpace.evalPairing μ) f

theorem CompactlySupportedMeasureSpace.supported_in_compact {X : Type u_1} [TopologicalSpace X] {MX : Type u_2} [AddCommGroup MX] [Module ℂ MX] [TopologicalSpace MX] [inst : CompactlySupportedMeasureSpace X MX] (μ : MX) : ∃ (K : Set X), IsCompact K ∧ μ ∈ closure (⇑(Finsupp.linearCombination ℂ dirac) '' {f : X →₀ ℂ | ↑f.support ⊆ K})

theorem CompactlySupportedMeasureSpace.isSupportedIn_sInter_closed {X : Type u_1} [TopologicalSpace X] {MX : Type u_2} [AddCommGroup MX] [Module ℂ MX] [TopologicalSpace MX] [CompactlySupportedMeasureSpace X MX] (μ : MX) (S : Set (Set X)) (hS : ∀ K ∈ S, IsClosed K ∧ μ ∈ closure (⇑(Finsupp.linearCombination ℂ dirac) '' {f : X →₀ ℂ | ↑f.support ⊆ K})) : μ ∈ closure (⇑(Finsupp.linearCombination ℂ dirac) '' {f : X →₀ ℂ | ↑f.support ⊆ ⋂₀ S})

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

noncomputable def concreteDirac (X : Type u_1) [TopologicalSpace X] (x : X) : WeakDual ℂ C(X, ℂ)

noncomputable def concreteDiracEmbed (X : Type u_1) [TopologicalSpace X] : (X →₀ ℂ) →ₗ[ℂ] WeakDual ℂ C(X, ℂ)

theorem weakDual_frechetUrysohn (X : Type u_1) [TopologicalSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] [T2Space X] : FrechetUrysohnSpace (WeakDual ℂ C(X, ℂ))

theorem linear_func_decomp_pi {ι : Type u_1} [Fintype ι] [DecidableEq ι] (l : (ι → ℂ) →ₗ[ℂ] ℂ) (w : ι → ℂ) : l w = ∑ i : ι, l (Function.update 0 i 1) * w i

theorem concreteDiracEmbed_apply_sum (X : Type u_1) [TopologicalSpace X] (c : X →₀ ℂ) (f : C(X, ℂ)) : ((concreteDiracEmbed X) c) f = ∑ x ∈ c.support, c x * f x

theorem concreteDiracEmbed_match_on_finset (X : Type u_1) [TopologicalSpace X] (μ : WeakDual ℂ C(X, ℂ)) (I : Finset C(X, ℂ)) : ∃ (c : X →₀ ℂ), ∀ f ∈ I, ((concreteDiracEmbed X) c) f = μ f

theorem concreteDiracEmbed_match_on_finset_restricted (X : Type u_1) [TopologicalSpace X] (μ : WeakDual ℂ C(X, ℂ)) (K : Set X) (hK : ∀ (f : C(X, ℂ)), (∀ x ∈ K, f x = 0) → μ f = 0) (I : Finset C(X, ℂ)) : ∃ (c : X →₀ ℂ), ↑c.support ⊆ K ∧ ∀ f ∈ I, ((concreteDiracEmbed X) c) f = μ f

theorem concreteDiracEmbed_range_dense_ax (X : Type u_1) [TopologicalSpace X] (μ : WeakDual ℂ C(X, ℂ)) : μ ∈ closure (Set.range ⇑(concreteDiracEmbed X))

theorem finitelySupportedMeasures_dense (X : Type u_1) [TopologicalSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] [T2Space X] : Dense (Set.range ⇑(concreteDiracEmbed X))

theorem lemma_3_4_dense_concrete (X : Type u_1) [TopologicalSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] [T2Space X] : Dense (Set.range ⇑(concreteDiracEmbed X))

theorem finitelySupportedMeasures_seqDense (X : Type u_1) [TopologicalSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] [T2Space X] (μ : WeakDual ℂ C(X, ℂ)) : ∃ (μ_seq : ℕ → X →₀ ℂ), Filter.Tendsto (fun (n : ℕ) => (concreteDiracEmbed X) (μ_seq n)) Filter.atTop (nhds μ)

theorem lemma_3_4_seq_dense_concrete (X : Type u_1) [TopologicalSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] [T2Space X] (μ : WeakDual ℂ C(X, ℂ)) : ∃ (μ_seq : ℕ → X →₀ ℂ), Filter.Tendsto (fun (n : ℕ) => (concreteDiracEmbed X) (μ_seq n)) Filter.atTop (nhds μ)

theorem lemma_3_4_seq_dense {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] [T2Space X] (μ : WeakDual ℂ C(X, ℂ)) : ∃ (μ_seq : ℕ → X →₀ ℂ), Filter.Tendsto (fun (n : ℕ) => (concreteDiracEmbed X) (μ_seq n)) Filter.atTop (nhds μ)

noncomputable def boxtimesAtomic (X : Type u_1) (Y : Type u_2) : (X →₀ ℂ) →ₗ[ℂ] (Y →₀ ℂ) →ₗ[ℂ] X × Y →₀ ℂ

theorem boxtimesAtomic_single_single (X : Type u_1) (Y : Type u_2) (x : X) (y : Y) (a b : ℂ) : ((boxtimesAtomic X Y) (Finsupp.single x a)) (Finsupp.single y b) = Finsupp.single (x, y) (a * b)

noncomputable def boxtimesAtomicToMeas (X : Type u_1) [TopologicalSpace X] (Y : Type u_2) [TopologicalSpace Y] : (X →₀ ℂ) →ₗ[ℂ] (Y →₀ ℂ) →ₗ[ℂ] WeakDual ℂ C(X × Y, ℂ)

theorem blt_extension_exists_ax {D₁ : Type u_3} [AddCommGroup D₁] [Module ℂ D₁] {D₂ : Type u_4} [AddCommGroup D₂] [Module ℂ D₂] {M₁ : Type u_5} [AddCommGroup M₁] [Module ℂ M₁] [TopologicalSpace M₁] {M₂ : Type u_6} [AddCommGroup M₂] [Module ℂ M₂] [TopologicalSpace M₂] {Z : Type u_7} [AddCommGroup Z] [Module ℂ Z] [TopologicalSpace Z] [T2Space Z] (ι₁ : D₁ →ₗ[ℂ] M₁) (ι₂ : D₂ →ₗ[ℂ] M₂) (hd₁ : Dense (Set.range ⇑ι₁)) (hd₂ : Dense (Set.range ⇑ι₂)) (f : D₁ →ₗ[ℂ] D₂ →ₗ[ℂ] Z) : ∃ (g : M₁ →ₗ[ℂ] M₂ →ₗ[ℂ] Z), (∀ (x₁ : D₁) (x₂ : D₂), (g (ι₁ x₁)) (ι₂ x₂) = (f x₁) x₂) ∧ (∀ (m₂ : M₂), Continuous fun (m₁ : M₁) => (g m₁) m₂) ∧ ∀ (m₁ : M₁), Continuous fun (m₂ : M₂) => (g m₁) m₂

noncomputable def bltExtensionMap {D₁ : Type u_3} [AddCommGroup D₁] [Module ℂ D₁] {D₂ : Type u_4} [AddCommGroup D₂] [Module ℂ D₂] {M₁ : Type u_5} [AddCommGroup M₁] [Module ℂ M₁] [TopologicalSpace M₁] {M₂ : Type u_6} [AddCommGroup M₂] [Module ℂ M₂] [TopologicalSpace M₂] {Z : Type u_7} [AddCommGroup Z] [Module ℂ Z] [TopologicalSpace Z] [T2Space Z] (ι₁ : D₁ →ₗ[ℂ] M₁) (ι₂ : D₂ →ₗ[ℂ] M₂) (hd₁ : Dense (Set.range ⇑ι₁)) (hd₂ : Dense (Set.range ⇑ι₂)) (f : D₁ →ₗ[ℂ] D₂ →ₗ[ℂ] Z) : M₁ →ₗ[ℂ] M₂ →ₗ[ℂ] Z

theorem blt_extension_extends {D₁ : Type u_3} [AddCommGroup D₁] [Module ℂ D₁] {D₂ : Type u_4} [AddCommGroup D₂] [Module ℂ D₂] {M₁ : Type u_5} [AddCommGroup M₁] [Module ℂ M₁] [TopologicalSpace M₁] {M₂ : Type u_6} [AddCommGroup M₂] [Module ℂ M₂] [TopologicalSpace M₂] {Z : Type u_7} [AddCommGroup Z] [Module ℂ Z] [TopologicalSpace Z] [T2Space Z] (ι₁ : D₁ →ₗ[ℂ] M₁) (ι₂ : D₂ →ₗ[ℂ] M₂) (hd₁ : Dense (Set.range ⇑ι₁)) (hd₂ : Dense (Set.range ⇑ι₂)) (f : D₁ →ₗ[ℂ] D₂ →ₗ[ℂ] Z) (x₁ : D₁) (x₂ : D₂) : ((bltExtensionMap ι₁ ι₂ hd₁ hd₂ f) (ι₁ x₁)) (ι₂ x₂) = (f x₁) x₂

theorem blt_extension_cont_left {D₁ : Type u_3} [AddCommGroup D₁] [Module ℂ D₁] {D₂ : Type u_4} [AddCommGroup D₂] [Module ℂ D₂] {M₁ : Type u_5} [AddCommGroup M₁] [Module ℂ M₁] [TopologicalSpace M₁] {M₂ : Type u_6} [AddCommGroup M₂] [Module ℂ M₂] [TopologicalSpace M₂] {Z : Type u_7} [AddCommGroup Z] [Module ℂ Z] [TopologicalSpace Z] [T2Space Z] (ι₁ : D₁ →ₗ[ℂ] M₁) (ι₂ : D₂ →ₗ[ℂ] M₂) (hd₁ : Dense (Set.range ⇑ι₁)) (hd₂ : Dense (Set.range ⇑ι₂)) (f : D₁ →ₗ[ℂ] D₂ →ₗ[ℂ] Z) (m₂ : M₂) : Continuous fun (m₁ : M₁) => ((bltExtensionMap ι₁ ι₂ hd₁ hd₂ f) m₁) m₂

theorem blt_extension_cont_right {D₁ : Type u_3} [AddCommGroup D₁] [Module ℂ D₁] {D₂ : Type u_4} [AddCommGroup D₂] [Module ℂ D₂] {M₁ : Type u_5} [AddCommGroup M₁] [Module ℂ M₁] [TopologicalSpace M₁] {M₂ : Type u_6} [AddCommGroup M₂] [Module ℂ M₂] [TopologicalSpace M₂] {Z : Type u_7} [AddCommGroup Z] [Module ℂ Z] [TopologicalSpace Z] [T2Space Z] (ι₁ : D₁ →ₗ[ℂ] M₁) (ι₂ : D₂ →ₗ[ℂ] M₂) (hd₁ : Dense (Set.range ⇑ι₁)) (hd₂ : Dense (Set.range ⇑ι₂)) (f : D₁ →ₗ[ℂ] D₂ →ₗ[ℂ] Z) (m₁ : M₁) : Continuous fun (m₂ : M₂) => ((bltExtensionMap ι₁ ι₂ hd₁ hd₂ f) m₁) m₂

theorem boxtimes_extension_exists (X : Type u_1) [TopologicalSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] [T2Space X] (Y : Type u_2) [TopologicalSpace Y] [LocallyCompactSpace Y] [SecondCountableTopology Y] [T2Space Y] : ∃ (bt : WeakDual ℂ C(X, ℂ) →ₗ[ℂ] WeakDual ℂ C(Y, ℂ) →ₗ[ℂ] WeakDual ℂ C(X × Y, ℂ)), (∀ (μ : X →₀ ℂ) (ν : Y →₀ ℂ), (bt ((concreteDiracEmbed X) μ)) ((concreteDiracEmbed Y) ν) = (concreteDiracEmbed (X × Y)) (((boxtimesAtomic X Y) μ) ν)) ∧ (∀ (ν : WeakDual ℂ C(Y, ℂ)), Continuous fun (μ : WeakDual ℂ C(X, ℂ)) => (bt μ) ν) ∧ ∀ (μ : WeakDual ℂ C(X, ℂ)), Continuous fun (ν : WeakDual ℂ C(Y, ℂ)) => (bt μ) ν

theorem boxtimes_extension_unique (X : Type u_1) [TopologicalSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] [T2Space X] (Y : Type u_2) [TopologicalSpace Y] [LocallyCompactSpace Y] [SecondCountableTopology Y] [T2Space Y] (bt₁ bt₂ : WeakDual ℂ C(X, ℂ) →ₗ[ℂ] WeakDual ℂ C(Y, ℂ) →ₗ[ℂ] WeakDual ℂ C(X × Y, ℂ)) (hext₁ : ∀ (μ : X →₀ ℂ) (ν : Y →₀ ℂ), (bt₁ ((concreteDiracEmbed X) μ)) ((concreteDiracEmbed Y) ν) = (concreteDiracEmbed (X × Y)) (((boxtimesAtomic X Y) μ) ν)) (hext₂ : ∀ (μ : X →₀ ℂ) (ν : Y →₀ ℂ), (bt₂ ((concreteDiracEmbed X) μ)) ((concreteDiracEmbed Y) ν) = (concreteDiracEmbed (X × Y)) (((boxtimesAtomic X Y) μ) ν)) (hcont₁_l : ∀ (ν : WeakDual ℂ C(Y, ℂ)), Continuous fun (μ : WeakDual ℂ C(X, ℂ)) => (bt₁ μ) ν) (hcont₁_r : ∀ (μ : WeakDual ℂ C(X, ℂ)), Continuous fun (ν : WeakDual ℂ C(Y, ℂ)) => (bt₁ μ) ν) (hcont₂_l : ∀ (ν : WeakDual ℂ C(Y, ℂ)), Continuous fun (μ : WeakDual ℂ C(X, ℂ)) => (bt₂ μ) ν) (hcont₂_r : ∀ (μ : WeakDual ℂ C(X, ℂ)), Continuous fun (ν : WeakDual ℂ C(Y, ℂ)) => (bt₂ μ) ν) : bt₁ = bt₂

theorem corollary_3_5 (X : Type u_1) [TopologicalSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] [T2Space X] (Y : Type u_2) [TopologicalSpace Y] [LocallyCompactSpace Y] [SecondCountableTopology Y] [T2Space Y] : (∃ (bt : WeakDual ℂ C(X, ℂ) →ₗ[ℂ] WeakDual ℂ C(Y, ℂ) →ₗ[ℂ] WeakDual ℂ C(X × Y, ℂ)), (∀ (μ : X →₀ ℂ) (ν : Y →₀ ℂ), (bt ((concreteDiracEmbed X) μ)) ((concreteDiracEmbed Y) ν) = (concreteDiracEmbed (X × Y)) (((boxtimesAtomic X Y) μ) ν)) ∧ (∀ (ν : WeakDual ℂ C(Y, ℂ)), Continuous fun (μ : WeakDual ℂ C(X, ℂ)) => (bt μ) ν) ∧ ∀ (μ : WeakDual ℂ C(X, ℂ)), Continuous fun (ν : WeakDual ℂ C(Y, ℂ)) => (bt μ) ν) ∧ ∀ (bt₁ bt₂ : WeakDual ℂ C(X, ℂ) →ₗ[ℂ] WeakDual ℂ C(Y, ℂ) →ₗ[ℂ] WeakDual ℂ C(X × Y, ℂ)), (∀ (μ : X →₀ ℂ) (ν : Y →₀ ℂ), (bt₁ ((concreteDiracEmbed X) μ)) ((concreteDiracEmbed Y) ν) = (concreteDiracEmbed (X × Y)) (((boxtimesAtomic X Y) μ) ν)) → (∀ (μ : X →₀ ℂ) (ν : Y →₀ ℂ), (bt₂ ((concreteDiracEmbed X) μ)) ((concreteDiracEmbed Y) ν) = (concreteDiracEmbed (X × Y)) (((boxtimesAtomic X Y) μ) ν)) → (∀ (ν : WeakDual ℂ C(Y, ℂ)), Continuous fun (μ : WeakDual ℂ C(X, ℂ)) => (bt₁ μ) ν) → (∀ (μ : WeakDual ℂ C(X, ℂ)), Continuous fun (ν : WeakDual ℂ C(Y, ℂ)) => (bt₁ μ) ν) → (∀ (ν : WeakDual ℂ C(Y, ℂ)), Continuous fun (μ : WeakDual ℂ C(X, ℂ)) => (bt₂ μ) ν) → (∀ (μ : WeakDual ℂ C(X, ℂ)), Continuous fun (ν : WeakDual ℂ C(Y, ℂ)) => (bt₂ μ) ν) → bt₁ = bt₂