OAI/LinearAlgebra/MatrixMultiplication/FieldHistory/BranchWeights.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finite extraction histories, inherited masks and recovery bounds.

  1. theorem OAI.MatrixMultiplication.AllFieldHistoryBranchWeights.stageB_branchPopulation_rat line 15
  2. theorem OAI.MatrixMultiplication.AllFieldHistoryBranchWeights.stageB_branchPopulation_real line 23
  3. theorem OAI.MatrixMultiplication.AllFieldHistoryBranchWeights.stageB_branchWeight_rat line 30
  4. theorem OAI.MatrixMultiplication.AllFieldHistoryBranchWeights.stageB_branchWeight_real line 42
  5. theorem OAI.MatrixMultiplication.AllFieldHistoryBranchWeights.shapeCounts_weighted_sum line 54