FiniteChannelSchur.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

From two-split kernels to channel estimates

The channel input may be signed: the estimates here therefore also apply when the transition probabilities have been centered in their residue coordinate. No probabilistic or analytic estimate is assumed implicitly.

theorem OAI.JointDickman.weighted_product_cauchy line 17

theorem OAI.JointDickman.finiteKernelAction_quadratic_bound line 31

Source documentation

The quadratic-form version of the weighted Schur bound.

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

Mentions: OAI.JointDickman.finiteKernelAction

theorem OAI.JointDickman.finiteChannel_square_of_kernel_rows line 88

Source documentation

A bound for the two-split kernel controls the original channel. Unlike a marginal estimate, this applies to signed, centered channels.

theorem finiteChannel_square_of_kernel_rows {Ω A : Type*} [Fintype Ω] [Fintype A]
    (w : Ω → ℝ) (μ : A → ℝ) (p : Ω → A → ℝ)
    (hw : ∀ s, 0 ≤ w s) (hμ : ∀ a, 0 < μ a) {C : ℝ} (hC : 0 ≤ C)
    (hrow : ∀ a, (∑ b, μ b * |finiteTwoSplitKernel w μ p a b|) ≤ C)
    (f : Ω → ℝ) :
    (∑ a, μ a * finiteChannel w μ p f a ^ 2) ≤ C * ∑ s, w s * f s ^ 2 := by
…

Mentions: OAI.JointDickman.finiteTwoSplitKernel, OAI.JointDickman.finiteChannel