AnchorDiagonalTotal.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Summing the code-preserving diagonal after counterpart normalization

abbrev OAI.Ostmann.AnchorMatchings line 12

theorem OAI.Ostmann.anchor_preserving_diagonal_total line 19

Source documentation

The external pivot count is canceled before counting code-preserving matchings. No unnormalized error is multiplied by the pivot population.

theorem anchor_preserving_diagonal_total {n m : ℕ} {P : Type*} [Fintype P]
    (α : Fin n → ℤ) (hα : ∀ j, α j = 1 ∨ α j = -1)
    (F : AnchorMatchings α m → P → ℂ) (C E T Δ κ : ℝ)
    (hC : 0 ≤ C) (hE : 0 ≤ E) (hP : (Fintype.card P : ℝ) ≤ Real.exp (T + κ))
    (hF : ∀ e p, ‖F e p‖ ≤ C * Real.exp (-(T + Δ)) * E) :
    ‖∑ e, ∑ p, F e p‖ ≤ ((2 * m : ℕ) : ℝ) ^ (2 ^ n * m) * C * Real.exp (κ - Δ) * E := by
…

Mentions: OAI.Ostmann.AnchorMatchings

theorem OAI.Ostmann.matching_harmonic_entropy line 38

Source documentation

The original harmonic normalizer provides exactly the L^(-rm) needed to turn matching multiplicity into z^(rm), with m/L ≤ z.

theorem matching_harmonic_entropy (N m : ℕ) (L z C : ℝ)
    (hL : 0 < L) (hz : 0 < z) (hm : (m : ℝ) ≤ z * L) :
    ((2 * m : ℕ) : ℝ) ^ N * (L⁻¹ ^ N * Real.exp (C * N)) ≤
      Real.exp ((Real.log z + (Real.log 2 + C)) * N) := by
…