FiniteChannels.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Finite smoothing channels

Nonnegative transition probabilities and a uniform output mass bound imply the weighted square-norm estimate for finite smoothing channels.

def OAI.JointDickman.finiteChannel line 22
def OAI.JointDickman.finiteChannelAdjoint line 25

theorem OAI.JointDickman.finiteChannel_adjoint line 29

Source documentation

Exact weighted adjoint identity, before any norm estimate.

theorem finiteChannel_adjoint (w : Ω → ℝ) (μ : A → ℝ) (p : Ω → A → ℝ)
    (hμ : ∀ a, μ a ≠ 0) (f : Ω → ℝ) (g : A → ℝ) :
    (∑ a, μ a * finiteChannel w μ p f a * g a) =
      ∑ s, w s * f s * finiteChannelAdjoint p g s := by
…

Mentions: OAI.JointDickman.finiteChannel, OAI.JointDickman.finiteChannelAdjoint

theorem OAI.JointDickman.channel_cell_square line 42

theorem OAI.JointDickman.finiteChannel_square_bound line 57

Source documentation

The first channel bound follows just from its output marginal and its subprobability row sums. This is a weighted finite Schur bound.

theorem finiteChannel_square_bound (w : Ω → ℝ) (μ : A → ℝ) (p : Ω → A → ℝ)
    (hw : ∀ s, 0 ≤ w s) (hμ : ∀ a, 0 < μ a) (hp : ∀ s a, 0 ≤ p s a)
    {C : ℝ} (hC : 0 ≤ C)
    (hmarginal : ∀ a, (∑ s, w s * p s a) ≤ C * μ a)
    (hrow : ∀ s, (∑ a, p s a) ≤ 1) (f : Ω → ℝ) :
    (∑ a, μ a * finiteChannel w μ p f a ^ 2) ≤ C * ∑ s, w s * f s ^ 2 := by
…

Mentions: OAI.JointDickman.finiteChannel

def OAI.JointDickman.finiteTwoSplitKernel line 91
Source documentation
The two-split kernel, expressed without an assumed adjoint theorem.
```
noncomputable def finiteTwoSplitKernel (w : Ω → ℝ) (μ : A → ℝ)
    (p : Ω → A → ℝ) (a b : A) : ℝ :=
…
```
theorem OAI.JointDickman.finiteTwoSplitKernel_symm line 96

def OAI.JointDickman.finiteKernelAction line 107

Source documentation

Integral action of a kernel on a finite space with atom masses μ.

noncomputable def finiteKernelAction (μ : A → ℝ) (K : A → A → ℝ)
    (g : A → ℝ) (a : A) : ℝ := ∑ b, μ b * K a b * g b

theorem OAI.JointDickman.finiteTwoSplitKernel_action line 111
Source documentation
The two-split kernel is exactly the channel followed by its adjoint.
```
theorem finiteTwoSplitKernel_action (w : Ω → ℝ) (μ : A → ℝ)
    (p : Ω → A → ℝ) (hμ : ∀ a, μ a ≠ 0) (g : A → ℝ) (a : A) :
    finiteKernelAction μ (finiteTwoSplitKernel w μ p) g a =
      finiteChannel w μ p (finiteChannelAdjoint p g) a := by
…
```
Mentions: OAI.JointDickman.finiteKernelAction, OAI.JointDickman.finiteTwoSplitKernel, OAI.JointDickman.finiteChannel, OAI.JointDickman.finiteChannelAdjoint

theorem OAI.JointDickman.finiteKernelAction_square_bound line 127

Source documentation

Two weighted absolute row/column estimates give a finite Schur bound. This form also applies to signed differences of probability kernels.

theorem finiteKernelAction_square_bound (μ : A → ℝ) (K : A → A → ℝ)
    (hμ : ∀ a, 0 ≤ μ a) {C : ℝ} (hC : 0 ≤ C)
    (hrow : ∀ a, (∑ b, μ b * |K a b|) ≤ C)
    (hcol : ∀ b, (∑ a, μ a * |K a b|) ≤ C) (g : A → ℝ) :
    (∑ a, μ a * finiteKernelAction μ K g a ^ 2) ≤
      C ^ 2 * ∑ a, μ a * g a ^ 2 := by
…

Mentions: OAI.JointDickman.finiteKernelAction