OAI/Combinatorics/GotsmanLinial/BlockCoupling.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The finite block coupling

Normalize a nonnegative matrix of block masses, identify its two binomial marginals, and reflect its first index. The low-degree block vanishing gives the one-sided displacement bound required by the finite coupling lemma.

  1. def OAI.LeanBlast.GotsmanLinial.normalizedPairWeight line 21

    Source documentation

    Normalize finite two-index masses by their total mass.

    noncomputable def normalizedPairWeight {α β : Type*}
    (B : α → β → ℝ) (Z : ℝ) (t : α × β) : ℝ :=
…
  2. theorem OAI.LeanBlast.GotsmanLinial.normalizedPairWeight_nonneg line 25
  3. theorem OAI.LeanBlast.GotsmanLinial.normalizedPairWeight_row line 30
  4. theorem OAI.LeanBlast.GotsmanLinial.normalizedPairWeight_column line 35
  5. theorem OAI.LeanBlast.GotsmanLinial.normalizedPairWeight_expect_fst line 41

    Source documentation

    First-coordinate expectations are computed from the row sums.

    theorem normalizedPairWeight_expect_fst {α β : Type*} [Fintype α] [Fintype β]
    (B : α → β → ℝ) (Z : ℝ) (φ : α → ℝ) :
    (∑ t : α × β, normalizedPairWeight B Z t * φ t.1) =
      ∑ r : α, ((∑ s : β, B r s) / Z) * φ r := by
…

    Mentions: OAI.LeanBlast.GotsmanLinial.normalizedPairWeight

  6. theorem OAI.LeanBlast.GotsmanLinial.normalizedPairWeight_expect_snd line 52

    Source documentation

    Second-coordinate expectations are computed from the column sums.

    theorem normalizedPairWeight_expect_snd {α β : Type*} [Fintype α] [Fintype β]
    (B : α → β → ℝ) (Z : ℝ) (φ : β → ℝ) :
    (∑ t : α × β, normalizedPairWeight B Z t * φ t.2) =
      ∑ s : β, ((∑ r : α, B r s) / Z) * φ s := by
…

    Mentions: OAI.LeanBlast.GotsmanLinial.normalizedPairWeight

  7. theorem OAI.LeanBlast.GotsmanLinial.binomial_block_coupling_bound line 64

    Source documentation

    Finite masses with binomial row and column sums, supported above the anti-diagonal r+s=n-d, have the required centered quadratic bound.

    theorem binomial_block_coupling_bound
    (n d : ℕ) (B : Fin (n + 1) → Fin (n + 1) → ℝ)
    (hB : ∀ r s, 0 ≤ B r s)
    (hrow : ∀ r, (∑ s : Fin (n + 1), B r s) = (n.choose r.val : ℝ))
    (hcol : ∀ s, (∑ r : Fin (n + 1), B r s) = (n.choose s.val : ℝ))
    (hvanish : ∀ r s, r.val + s.val < n - d → B r s = 0) :
    (∑ r : Fin (n + 1), ∑ s : Fin (n + 1),
      ((s.val : ℝ) + (r.val : ℝ) - (n : ℝ)) ^ 2 * B r s) ≤
        4 * (d : ℝ) * Real.sqrt (n : ℝ) * (2 : ℝ) ^ n := by
…
  8. def OAI.LeanBlast.GotsmanLinial.blockCouplingWeight line 137

    Source documentation

    The actual finite probability weights supplied by the Hilbert--Schmidt blocks of an operator in a binomial orthogonal grading.

    noncomputable def blockCouplingWeight {n : ℕ} {ι : Type*} [Fintype ι]
    (P : Fin (n + 1) → Matrix ι ι ℂ) (H : Matrix ι ι ℂ)
    (t : Fin (n + 1) × Fin (n + 1)) : ℝ :=
…
  9. theorem OAI.LeanBlast.GotsmanLinial.blockCouplingWeight_nonneg line 142
  10. theorem OAI.LeanBlast.GotsmanLinial.blockCouplingWeight_fst_marginal line 149

    Source documentation

    The first block index has the binomial distribution.

    theorem blockCouplingWeight_fst_marginal {n : ℕ} {ι : Type*}
    [Fintype ι] [DecidableEq ι]
    {P : Fin (n + 1) → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P)
    (H : Matrix ι ι ℂ) (hH : H.conjTranspose * H = 1)
    (hmult : ∀ k, hsNormSq (P k) = (n.choose k.val : ℝ))
    (r : Fin (n + 1)) :
    (∑ s : Fin (n + 1), blockCouplingWeight P H (r, s)) = binomialWeight n r := by
…

    Mentions: OAI.LeanBlast.GotsmanLinial.OrthogonalProjectionFamily, OAI.LeanBlast.GotsmanLinial.hsNormSq, OAI.LeanBlast.GotsmanLinial.blockCouplingWeight, OAI.LeanBlast.GotsmanLinial.binomialWeight

  11. theorem OAI.LeanBlast.GotsmanLinial.blockCouplingWeight_snd_marginal line 161

    Source documentation

    The second block index has the same binomial distribution.

    theorem blockCouplingWeight_snd_marginal {n : ℕ} {ι : Type*}
    [Fintype ι] [DecidableEq ι]
    {P : Fin (n + 1) → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P)
    (H : Matrix ι ι ℂ) (hH : H * H.conjTranspose = 1)
    (hmult : ∀ k, hsNormSq (P k) = (n.choose k.val : ℝ))
    (s : Fin (n + 1)) :
    (∑ r : Fin (n + 1), blockCouplingWeight P H (r, s)) = binomialWeight n s := by
…

    Mentions: OAI.LeanBlast.GotsmanLinial.OrthogonalProjectionFamily, OAI.LeanBlast.GotsmanLinial.hsNormSq, OAI.LeanBlast.GotsmanLinial.blockCouplingWeight, OAI.LeanBlast.GotsmanLinial.binomialWeight

  12. theorem OAI.LeanBlast.GotsmanLinial.sum_blockCouplingWeight line 174

    Source documentation

    Unitarity and the grading multiplicities make the block weights a probability distribution without any additional normalization assumption.

    theorem sum_blockCouplingWeight {n : ℕ} {ι : Type*}
    [Fintype ι] [DecidableEq ι]
    {P : Fin (n + 1) → Matrix ι ι ℂ} (hP : OrthogonalProjectionFamily P)
    (H : Matrix ι ι ℂ) (hH : H.conjTranspose * H = 1)
    (hmult : ∀ k, hsNormSq (P k) = (n.choose k.val : ℝ)) :
    (∑ t : Fin (n + 1) × Fin (n + 1), blockCouplingWeight P H t) = 1 := by
…

    Mentions: OAI.LeanBlast.GotsmanLinial.OrthogonalProjectionFamily, OAI.LeanBlast.GotsmanLinial.hsNormSq, OAI.LeanBlast.GotsmanLinial.blockCouplingWeight

  13. theorem OAI.LeanBlast.GotsmanLinial.blockCouplingWeight_support line 185

    Source documentation

    A nonzero block probability lies on or above the required anti-diagonal.

    theorem blockCouplingWeight_support {n d : ℕ} {ι : Type*} [Fintype ι]
    (P : Fin (n + 1) → Matrix ι ι ℂ) (H : Matrix ι ι ℂ)
    (hvanish : ∀ r s, r.val + s.val < n - d → P s * H * P r = 0)
    (r s : Fin (n + 1)) (ht : blockCouplingWeight P H (r, s) ≠ 0) :
    n - d ≤ r.val + s.val := by
…

    Mentions: OAI.LeanBlast.GotsmanLinial.blockCouplingWeight

  14. theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_centeredGrading_anticommutator_le line 199

    Source documentation

    The spectral block coupling bounds the actual centered grading anticommutator. Its hypotheses are the orthogonal grading, its binomial multiplicities, unitarity, and the separately proved low-degree vanishing.

    theorem hsNormSq_centeredGrading_anticommutator_le {ι : Type*}
    [Fintype ι] [DecidableEq ι]
    (n d : ℕ) (P : Fin (n + 1) → Matrix ι ι ℂ)
    (hP : OrthogonalProjectionFamily P) (H : Matrix ι ι ℂ)
    (hleft : H.conjTranspose * H = 1) (hright : H * H.conjTranspose = 1)
    (hmult : ∀ k, hsNormSq (P k) = (n.choose k.val : ℝ))
    (hvanish : ∀ r s, r.val + s.val < n - d → P s * H * P r = 0) :
    hsNormSq (centeredGrading P * H + H * centeredGrading P) ≤
      4 * (d : ℝ) * Real.sqrt (n : ℝ) * (2 : ℝ) ^ n := by
…

    Mentions: OAI.LeanBlast.GotsmanLinial.OrthogonalProjectionFamily, OAI.LeanBlast.GotsmanLinial.hsNormSq, OAI.LeanBlast.GotsmanLinial.centeredGrading

  15. theorem OAI.LeanBlast.GotsmanLinial.hsNormSq_centeredGrading_anticommutator_le_of_trace line 221

    Source documentation

    Trace-multiplicity form, for direct use with finite-dimensional orthogonal projections whose ranks have already been computed.

    theorem hsNormSq_centeredGrading_anticommutator_le_of_trace {ι : Type*}
    [Fintype ι] [DecidableEq ι]
    (n d : ℕ) (P : Fin (n + 1) → Matrix ι ι ℂ)
    (hP : OrthogonalProjectionFamily P) (H : Matrix ι ι ℂ)
    (hleft : H.conjTranspose * H = 1) (hright : H * H.conjTranspose = 1)
    (htrace : ∀ k, (Matrix.trace (P k)).re = (n.choose k.val : ℝ))
    (hvanish : ∀ r s, r.val + s.val < n - d → P s * H * P r = 0) :
    hsNormSq (centeredGrading P * H + H * centeredGrading P) ≤
      4 * (d : ℝ) * Real.sqrt (n : ℝ) * (2 : ℝ) ^ n := by
…

    Mentions: OAI.LeanBlast.GotsmanLinial.OrthogonalProjectionFamily, OAI.LeanBlast.GotsmanLinial.hsNormSq, OAI.LeanBlast.GotsmanLinial.centeredGrading