OAI/Algebra/DepthFive/FirstTraceNonnegative.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem335.pathShiftMatrix_first_trace_lower line 15

   Source documentation

   Nonnegative path coefficients suffice for a first-moment lower bound. Unlike the exact identity, this does not require disjoint path shifts.

   theorem pathShiftMatrix_first_trace_lower
       (shift : I → P → J) (weight : I → P → ℝ)
       (hw : ∀ i p, 0 ≤ weight i p) :
       (∑ i, ∑ p, weight i p ^ 2) ≤
         Matrix.trace ((pathShiftMatrix shift weight).transpose *
           pathShiftMatrix shift weight) := by
   …

   Mentions: OAI.Problem335.pathShiftMatrix

2. theorem OAI.Problem335.complex_path_first_trace_lower_nonnegative line 38

   Source documentation

   Real nonnegative path coefficients give the same lower bound in the genuine complex Gram trace.

   theorem complex_path_first_trace_lower_nonnegative
       (shift : I → P → J) (weight : I → P → ℝ)
       (hw : ∀ i p, 0 ≤ weight i p) :
       let A := pathShiftMatrix shift (fun i p => (weight i p : ℂ))
   …

   Mentions: OAI.Problem335.pathShiftMatrix

3. theorem OAI.Problem335.complex_path_first_trace_lower_of_average line 49

   Source documentation

   A uniform source-average path-mass lower bound gives the expected dimension times path-count lower bound for the complex first trace.

   theorem complex_path_first_trace_lower_of_average [Nonempty I]
       (shift : I → P → J) (weight : I → P → ℝ) (L : ℝ)
       (hw : ∀ i p, 0 ≤ weight i p)
       (hmean : ∀ p, L ≤ (∑ i, weight i p ^ 2) / (Fintype.card I : ℝ)) :
       let A := pathShiftMatrix shift (fun i p => (weight i p : ℂ))
   …

   Mentions: OAI.Problem335.pathShiftMatrix