Kernels as a module #
Mathlib makes Kernel α β an additive monoid, adding rows pointwise. This file adds the scalar
action, row by row, of any R acting on ℝ≥0∞ through a scalar tower, as mathlib does for
Measure β, so that Kernel α β is a module over ℝ≥0∞. A finite family of kernels averaged
over a latent index by weights c is then the sum ∑ i, c i • κ i, whose row at a is
∑ i, c i • κ i a by sum_apply and smul_apply. Finite kernels are closed under finite sums
and finite multiples. [UPSTREAM] candidate for Mathlib/Probability/Kernel/Defs.lean.
@[instance_reducible]
noncomputable instance
ProbabilityTheory.Kernel.instSMul
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{R : Type u_4}
[SMul R ENNReal]
[IsScalarTower R ENNReal ENNReal]
:
SMul R (Kernel α β)
Equations
- ProbabilityTheory.Kernel.instSMul = { smul := fun (c : R) (κ : ProbabilityTheory.Kernel α β) => { toFun := c • ⇑κ, measurable' := ⋯ } }
instance
ProbabilityTheory.Kernel.instIsSMulApplyMeasure_linglib
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{R : Type u_4}
[SMul R ENNReal]
[IsScalarTower R ENNReal ENNReal]
:
IsSMulApply R (Kernel α β) α (MeasureTheory.Measure β)
instance
ProbabilityTheory.Kernel.instSMulCommClassOfENNReal_linglib
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{R : Type u_4}
{R' : Type u_5}
[SMul R ENNReal]
[IsScalarTower R ENNReal ENNReal]
[SMul R' ENNReal]
[IsScalarTower R' ENNReal ENNReal]
[SMulCommClass R R' ENNReal]
:
SMulCommClass R R' (Kernel α β)
instance
ProbabilityTheory.Kernel.instIsScalarTowerOfENNReal_linglib
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{R : Type u_4}
{R' : Type u_5}
[SMul R ENNReal]
[IsScalarTower R ENNReal ENNReal]
[SMul R' ENNReal]
[IsScalarTower R' ENNReal ENNReal]
[SMul R R']
[IsScalarTower R R' ENNReal]
:
IsScalarTower R R' (Kernel α β)
@[instance_reducible]
noncomputable instance
ProbabilityTheory.Kernel.instModule
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{R : Type u_4}
[Semiring R]
[Module R ENNReal]
[IsScalarTower R ENNReal ENNReal]
:
Module R (Kernel α β)
Equations
- ProbabilityTheory.Kernel.instModule = { toSMul := ProbabilityTheory.Kernel.instSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }
theorem
ProbabilityTheory.IsFiniteKernel.smul_of_ne_top
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(κ : Kernel α β)
[IsFiniteKernel κ]
{c : ENNReal}
(hc : c ≠ ⊤)
:
IsFiniteKernel (c • κ)
A finite multiple of a finite kernel is a finite kernel.
theorem
ProbabilityTheory.IsFiniteKernel.finsetSum
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
{κs : ι → Kernel α β}
(I : Finset ι)
(h : ∀ i ∈ I, IsFiniteKernel (κs i))
:
IsFiniteKernel (∑ i ∈ I, κs i)