OAI/Combinatorics/ThinTrees/Normalization/Descent.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Normalization descent.

  1. def OAI.AlgorithmicThinTrees.Normalization.covariance line 22
  2. def OAI.AlgorithmicThinTrees.Normalization.leverage line 25
  3. def OAI.AlgorithmicThinTrees.Normalization.objective line 28
  4. def OAI.AlgorithmicThinTrees.Normalization.shrink line 31
  5. lemma OAI.AlgorithmicThinTrees.Normalization.shrink_pos line 35
  6. lemma OAI.AlgorithmicThinTrees.Normalization.covariance_shrink line 45
  7. lemma OAI.AlgorithmicThinTrees.Normalization.log_shrink_sum line 62
  8. lemma OAI.AlgorithmicThinTrees.Normalization.det_rank_one line 75
  9. lemma OAI.AlgorithmicThinTrees.Normalization.det_shrink line 88
  10. lemma OAI.AlgorithmicThinTrees.Normalization.leverage_test line 96
  11. lemma OAI.AlgorithmicThinTrees.Normalization.neg_log_one_sub line 105
  12. lemma OAI.AlgorithmicThinTrees.Normalization.objective_drop line 115
  13. lemma OAI.AlgorithmicThinTrees.Normalization.logdet_le_trace line 149
  14. structure OAI.AlgorithmicThinTrees.Normalization.BasisPacking line 162
  15. def OAI.AlgorithmicThinTrees.Normalization.BasisPacking.matrices line 170
  16. def OAI.AlgorithmicThinTrees.Normalization.BasisPacking.logWeights line 171
  17. lemma OAI.AlgorithmicThinTrees.Normalization.BasisPacking.covariance_eq line 175
  18. lemma OAI.AlgorithmicThinTrees.Normalization.BasisPacking.covariance_posDef line 185
  19. lemma OAI.AlgorithmicThinTrees.Normalization.BasisPacking.objective_nonneg line 190
  20. lemma OAI.AlgorithmicThinTrees.Normalization.BasisPacking.initial_gap line 203