OAI/Algebra/DepthFive/FirstTraceBound.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Problem335.FirstMoment.CompositionIndex line 11
2. abbrev OAI.Problem335.FirstMoment.Source line 14
3. def OAI.Problem335.FirstMoment.mass line 22

   Source documentation

   The squared normalized coefficient of one squarefree path.

   def mass {a b : ℕ} (s : P → Finset V) (z : P → Finset U)
       (i : Source V U a b) (p : P) : ℝ :=
   …

   Mentions: OAI.Problem335.FirstMoment.Source

4. lemma OAI.Problem335.FirstMoment.mass_nonneg line 27
5. lemma OAI.Problem335.FirstMoment.card_source line 32
6. lemma OAI.Problem335.FirstMoment.composition_card_pos line 37
7. lemma OAI.Problem335.FirstMoment.sum_mass line 45
8. def OAI.Problem335.FirstMoment.loss line 71

   Source documentation

   Exact first-moment loss, deliberately kept separate from asymptotic parameter estimates.

   def loss (a v b u k m : ℕ) : ℝ :=
   …

9. def OAI.Problem335.FirstMoment.mean line 75
10. theorem OAI.Problem335.FirstMoment.sum_mass_lower line 80

    Source documentation

    Sum the concrete occupation lower bound over every path and every source basis vector. The number of paths is counted exactly, not estimated.

    theorem sum_mass_lower {a b k m : ℕ} (s : P → Finset V) (z : P → Finset U)
        (hs : ∀ p, (s p).card = k) (hz : ∀ p, (z p).card = m)
        (ha : 0 < a) (hb : 0 < b) (hka : 2 * k ≤ a) (hmb : 2 * m ≤ b) :
        (Fintype.card (Source V U a b) : ℝ) * Fintype.card P *
          mean a (Fintype.card V) b (Fintype.card U) k m *
            Real.exp (-loss a (Fintype.card V) b (Fintype.card U) k m) ≤
          ∑ i : Source V U a b, ∑ p, mass s z i p := by
    …

    Mentions: OAI.Problem335.FirstMoment.Source, OAI.Problem335.FirstMoment.mean, OAI.Problem335.FirstMoment.loss, OAI.Problem335.FirstMoment.mass

11. theorem OAI.Problem335.FirstMoment.real_first_trace_lower line 111

    Source documentation

    First Gram-trace lower bound for a real square-root occupation path matrix. The disjointness premise permits arbitrary targets for zero-mass invalid paths.

    theorem real_first_trace_lower {J : Type*} [Fintype J] [DecidableEq J]
        {a b k m : ℕ} (s : P → Finset V) (z : P → Finset U)
        (hs : ∀ p, (s p).card = k) (hz : ∀ p, (z p).card = m)
        (ha : 0 < a) (hb : 0 < b) (hka : 2 * k ≤ a) (hmb : 2 * m ≤ b)
        (shift : Source V U a b → P → J)
        (hdisjoint : ∀ i p q, p ≠ q → shift i p = shift i q →
          mass s z i p = 0 ∨ mass s z i q = 0) :
        let A := pathShiftMatrix shift (fun i p => Real.sqrt (mass s z i p))
    …

    Mentions: OAI.Problem335.FirstMoment.Source, OAI.Problem335.FirstMoment.mass, OAI.Problem335.pathShiftMatrix

12. theorem OAI.Problem335.FirstMoment.complex_first_trace_lower line 128

    Source documentation

    The same first-moment estimate for the genuine complex adjoint.

    theorem complex_first_trace_lower {J : Type*} [Fintype J] [DecidableEq J]
        {a b k m : ℕ} (s : P → Finset V) (z : P → Finset U)
        (hs : ∀ p, (s p).card = k) (hz : ∀ p, (z p).card = m)
        (ha : 0 < a) (hb : 0 < b) (hka : 2 * k ≤ a) (hmb : 2 * m ≤ b)
        (shift : Source V U a b → P → J)
        (hdisjoint : ∀ i p q, p ≠ q → shift i p = shift i q →
          mass s z i p = 0 ∨ mass s z i q = 0) :
        let A := pathShiftMatrix shift (fun i p => (Real.sqrt (mass s z i p) : ℂ))
    …

    Mentions: OAI.Problem335.FirstMoment.Source, OAI.Problem335.FirstMoment.mass, OAI.Problem335.pathShiftMatrix