Abstract measures on topological spaces

We define an "abstract measure" on X, with values in a normed ring R, to be an R-linear functional on continuous maps X → R. This is an important construction in p-adic analysis (where the Iwasawa algebra is defined as the space of abstract measures on ℤ_[p] with values in ℚ_[p]).

Basic definitions

def AbstractMeasure (X : Type u_1) (R : Type u_3) (E : Type u_4) [TopologicalSpace X] [AddCommGroup E] [TopologicalSpace E] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Module R E] : Type (max (max u_3 u_1) u_4)

The space of E-valued measures on X, i.e. continuous linear maps C(X, R) → E. (The case R = E is the most important case.)

This is the same space C(X, R) →L[R] E, but we do not want it to inherit the default (norm) topology, so we make a type synonym.

Equations

• AbstractMeasure X R E = (C(X, R) →L[R] E)

def AbstractMeasure.«termD(_,_)» : Lean.ParserDescr

The space of E-valued measures on X, i.e. continuous linear maps C(X, R) → E. (The case R = E is the most important case.)

This is the same space C(X, R) →L[R] E, but we do not want it to inherit the default (norm) topology, so we make a type synonym.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance AbstractMeasure.instFunLikeContinuousMap {X : Type u_1} {R : Type u_3} {E : Type u_4} [TopologicalSpace X] [AddCommGroup E] [TopologicalSpace E] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Module R E] : FunLike (AbstractMeasure X R E) C(X, R) E

Inherit FunLike structure from C(X, R) →L[R] E.

Equations

• AbstractMeasure.instFunLikeContinuousMap = { coe := AbstractMeasure.instFunLikeContinuousMap._aux_1, coe_injective := ⋯ }

instance AbstractMeasure.instContinuousLinearMapClassContinuousMap {X : Type u_1} {R : Type u_3} {E : Type u_4} [TopologicalSpace X] [AddCommGroup E] [TopologicalSpace E] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Module R E] : ContinuousLinearMapClass (AbstractMeasure X R E) R C(X, R) E

Inherit ContinuousLinearMapClass structure from C(X, R) →L[R] E.

@[instance_reducible]

instance AbstractMeasure.instAddCommGroup {X : Type u_1} {R : Type u_3} {E : Type u_4} [TopologicalSpace X] [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Module R E] : AddCommGroup (AbstractMeasure X R E)

Inherit AddCommGroup structure from C(X, R) →L[R] E.

Equations

• One or more equations did not get rendered due to their size.

instance AbstractMeasure.isAddApply {X : Type u_1} {R : Type u_3} {E : Type u_4} [TopologicalSpace X] [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Module R E] : IsAddApply (AbstractMeasure X R E) C(X, R) E

@[instance_reducible]

instance AbstractMeasure.instModule {X : Type u_1} {R : Type u_3} {E : Type u_4} [TopologicalSpace X] [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Module R E] [ContinuousSMul R E] : Module R (AbstractMeasure X R E)

Inherit R-module structure from C(X, R) →L[R] E.

Equations

• AbstractMeasure.instModule = { smul := AbstractMeasure.instModule._aux_1, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

instance AbstractMeasure.isSMulApply {X : Type u_1} {R : Type u_3} {E : Type u_4} [TopologicalSpace X] [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Module R E] [ContinuousSMul R E] : IsSMulApply R (AbstractMeasure X R E) C(X, R) E

def AbstractMeasure.toCLMEquiv {X : Type u_1} {R : Type u_3} {E : Type u_4} [TopologicalSpace X] [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Module R E] [ContinuousSMul R E] : AbstractMeasure X R E ≃ₗ[R] C(X, R) →L[R] E

The defining equivalence between measures and continuous linear maps on continuous functions.

Equations

• AbstractMeasure.toCLMEquiv = LinearEquiv.refl R (AbstractMeasure X R E)

@[simp]

theorem AbstractMeasure.coe_toCLMEquiv {X : Type u_1} {R : Type u_3} {E : Type u_4} [TopologicalSpace X] [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Module R E] [ContinuousSMul R E] (μ : AbstractMeasure X R E) (f : C(X, R)) : (toCLMEquiv μ) f = μ f

@[simp]

theorem AbstractMeasure.coe_symm_toCLMEquiv {X : Type u_1} {R : Type u_3} {E : Type u_4} [TopologicalSpace X] [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Module R E] [ContinuousSMul R E] (L : C(X, R) →L[R] E) (f : C(X, R)) : (toCLMEquiv.symm L) f = L f

def AbstractMeasure.dirac {X : Type u_1} (R : Type u_3) [TopologicalSpace X] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] (x : X) : AbstractMeasure X R R

The Dirac measure, "evaluation at x".

Equations

• AbstractMeasure.dirac R x = AbstractMeasure.toCLMEquiv.symm (ContinuousMap.evalCLM R x)

@[simp]

theorem AbstractMeasure.dirac_apply {X : Type u_1} {R : Type u_3} [TopologicalSpace X] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] (x : X) (f : C(X, R)) : (dirac R x) f = f x

def AbstractMeasure.map {X : Type u_1} {Y : Type u_2} {R : Type u_3} {E : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Module R E] [ContinuousSMul R E] (f : C(X, Y)) : AbstractMeasure X R E →ₗ[R] AbstractMeasure Y R E

Measures can be pushed forward (R-linearly) along continuous maps.

Equations

• AbstractMeasure.map f = { toFun := fun (μ : AbstractMeasure X R E) => μ ∘SL ContinuousMap.compCLM R R f, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem AbstractMeasure.map_apply {X : Type u_1} {Y : Type u_2} {R : Type u_3} {E : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Module R E] [ContinuousSMul R E] (f : C(X, Y)) (μ : AbstractMeasure X R E) (g : C(Y, R)) : ((map f) μ) g = μ (g.comp f)

@[simp]

theorem AbstractMeasure.map_map {X : Type u_1} {Y : Type u_2} {R : Type u_3} {E : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Module R E] [ContinuousSMul R E] {Z : Type u_5} [TopologicalSpace Z] (f : C(X, Y)) (g : C(Y, Z)) (μ : AbstractMeasure X R E) : (map g) ((map f) μ) = (map (g.comp f)) μ

@[simp]

theorem AbstractMeasure.map_id {X : Type u_1} {R : Type u_3} {E : Type u_4} [TopologicalSpace X] [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Module R E] [ContinuousSMul R E] (μ : AbstractMeasure X R E) : (map (ContinuousMap.id X)) μ = μ

@[simp]

theorem AbstractMeasure.map_dirac {X : Type u_1} {Y : Type u_2} {R : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] (f : C(X, Y)) (x : X) : (map f) (dirac R x) = dirac R (f x)

Product structure

def AbstractMeasure.contractSnd {X : Type u_1} {Y : Type u_2} {R : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] : AbstractMeasure Y R R →ₗ[R] C(X × Y, R) →ₗ[R] C(X, R)

Send a measure ν on Y and a function f on X × Y to the function on X given by x ↦ ν (f (x, ·)), or more suggestively, x ↦ ∫ f(x, y) dμ(y).

Equations

• AbstractMeasure.contractSnd = LinearMap.mk₂ R (fun (ν : AbstractMeasure Y R R) (f : C(X × Y, R)) => (↑ν).comp f.curry) ⋯ ⋯ ⋯ ⋯

def AbstractMeasure.contractFst {X : Type u_1} {Y : Type u_2} {R : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] : AbstractMeasure X R R →ₗ[R] C(X × Y, R) →ₗ[R] C(Y, R)

Send a measure μ on X and a function f on X × Y to the function on Y given by y ↦ μ (f (·, y)), or more suggestively, y ↦ ∫ f(x, y) dμ(x).

Equations

• AbstractMeasure.contractFst = LinearMap.lcomp R C(Y, R) ↑(ContinuousMap.compCLM R R ContinuousMap.prodSwap) ∘ₗ AbstractMeasure.contractSnd

@[simp]

theorem AbstractMeasure.contractFst_apply {X : Type u_1} {Y : Type u_2} {R : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] (μ : AbstractMeasure X R R) (f : C(X × Y, R)) (y : Y) : ((contractFst μ) f) y = μ { toFun := fun (x : X) => f (x, y), continuous_toFun := ⋯ }

@[simp]

theorem AbstractMeasure.contractSnd_apply {X : Type u_1} {Y : Type u_2} {R : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] (ν : AbstractMeasure Y R R) (f : C(X × Y, R)) (x : X) : ((contractSnd ν) f) x = ν { toFun := fun (y : Y) => f (x, y), continuous_toFun := ⋯ }

theorem AbstractMeasure.contractFst_dirac {X : Type u_1} {Y : Type u_2} {R : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] (x : X) (y : Y) (f : C(X × Y, R)) : ((contractFst (dirac R x)) f) y = f (x, y)

theorem AbstractMeasure.contractSnd_dirac {X : Type u_1} {Y : Type u_2} {R : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] (x : X) (y : Y) (f : C(X × Y, R)) : ((contractSnd (dirac R y)) f) x = f (x, y)

def AbstractMeasure.contractSndCLM {X : Type u_1} {Y : Type u_2} {R : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [LocallyCompactSpace X] [LocallyCompactSpace Y] : AbstractMeasure Y R R →ₗ[R] C(X × Y, R) →L[R] C(X, R)

AbstractMeasure.contractSnd bundled with continuity in the function argument.

Equations

• AbstractMeasure.contractSndCLM = { toFun := fun (ν : AbstractMeasure Y R R) => { toLinearMap := AbstractMeasure.contractSnd ν, cont := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

def AbstractMeasure.contractFstCLM {X : Type u_1} {Y : Type u_2} {R : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [LocallyCompactSpace X] [LocallyCompactSpace Y] : AbstractMeasure X R R →ₗ[R] C(X × Y, R) →L[R] C(Y, R)

AbstractMeasure.contractFst bundled with continuity in the function argument.

Equations

• AbstractMeasure.contractFstCLM = ContinuousLinearMap.lcomp C(Y, R) (ContinuousMap.compCLM R R ContinuousMap.prodSwap) ∘ₗ AbstractMeasure.contractSndCLM

def AbstractMeasure.prodMk {X : Type u_1} {Y : Type u_2} {R : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [LocallyCompactSpace X] [LocallyCompactSpace Y] : AbstractMeasure X R R →ₗ[R] AbstractMeasure Y R R →ₗ[R] AbstractMeasure (X × Y) R R

"Left-handed" version of the natural product map on measures (acting on functions as first integrating along X, and then integrating the result along Y).

Equations

• AbstractMeasure.prodMk = ContinuousLinearMap.llcomp R C(X × Y, R) C(Y, R) R ∘ₗ AbstractMeasure.contractFstCLM

@[simp]

theorem AbstractMeasure.prodMk_apply {X : Type u_1} {Y : Type u_2} {R : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] (μ : AbstractMeasure X R R) (ν : AbstractMeasure Y R R) [LocallyCompactSpace X] [LocallyCompactSpace Y] (f : C(X × Y, R)) : ((prodMk μ) ν) f = ν ((contractFst μ) f)

theorem AbstractMeasure.prodMk_prod_apply {X : Type u_1} {Y : Type u_2} {R : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] (μ : AbstractMeasure X R R) (ν : AbstractMeasure Y R R) [LocallyCompactSpace X] [LocallyCompactSpace Y] (f : C(X, R)) (g : C(Y, R)) : ((prodMk μ) ν) (f.comp ContinuousMap.fst * g.comp ContinuousMap.snd) = μ f * ν g

On functions of the form (x, y) ↦ f x * g y, the measure prodMk μ ν agrees with the algebraic tensor product of μ and ν.

def AbstractMeasure.prodMk' {X : Type u_1} {Y : Type u_2} {R : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [LocallyCompactSpace X] [LocallyCompactSpace Y] : AbstractMeasure X R R →ₗ[R] AbstractMeasure Y R R →ₗ[R] AbstractMeasure (X × Y) R R

"Right-handed" version of the natural product map on measures (acting on functions as first integrating along Y, and then integrating the result along X).

Equations

• AbstractMeasure.prodMk' = (ContinuousLinearMap.llcomp R C(X × Y, R) C(X, R) R ∘ₗ AbstractMeasure.contractSndCLM).flip

@[simp]

theorem AbstractMeasure.prodMk'_apply {X : Type u_1} {Y : Type u_2} {R : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] (μ : AbstractMeasure X R R) (ν : AbstractMeasure Y R R) [LocallyCompactSpace X] [LocallyCompactSpace Y] (f : C(X × Y, R)) : ((prodMk' μ) ν) f = μ ((contractSnd ν) f)

theorem AbstractMeasure.prodMk'_flip {X : Type u_1} {Y : Type u_2} {R : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] (μ : AbstractMeasure X R R) (ν : AbstractMeasure Y R R) [LocallyCompactSpace X] [LocallyCompactSpace Y] (f : C(X × Y, R)) : ((prodMk' μ) ν) f = ((prodMk ν) μ) (f.comp ContinuousMap.prodSwap)

theorem AbstractMeasure.prodMk'_prod_apply {X : Type u_1} {Y : Type u_2} {R : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] (μ : AbstractMeasure X R R) (ν : AbstractMeasure Y R R) [LocallyCompactSpace X] [LocallyCompactSpace Y] (f : C(X, R)) (g : C(Y, R)) : ((prodMk' μ) ν) (f.comp ContinuousMap.fst * g.comp ContinuousMap.snd) = μ f * ν g

theorem AbstractMeasure.prodMk_eq_prodMk' {X : Type u_1} {Y : Type u_2} {R : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] (μ : AbstractMeasure X R R) (ν : AbstractMeasure Y R R) [CompactSpace X] [CompactSpace Y] [T2Space X] [T2Space Y] [TotallyDisconnectedSpace X] [T0Space R] : (prodMk μ) ν = (prodMk' μ) ν

For profinite spaces, the two product structures on measures agree.