OAI/Combinatorics/ThinTrees/Normalization/Packing.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Normalization packing.

  1. lemma OAI.AlgorithmicThinTrees.Normalization.covariance_posSemidef line 14
  2. lemma OAI.AlgorithmicThinTrees.Normalization.covariance_embedding line 22
  3. structure OAI.AlgorithmicThinTrees.Normalization.ContainedPacking line 32
  4. def OAI.AlgorithmicThinTrees.Normalization.ContainedPacking.full line 42
  5. lemma OAI.AlgorithmicThinTrees.Normalization.ContainedPacking.extra_posSemidef line 46
  6. lemma OAI.AlgorithmicThinTrees.Normalization.ContainedPacking.covariance_posDef line 54
  7. lemma OAI.AlgorithmicThinTrees.Normalization.ContainedPacking.objective_nonneg line 59
  8. lemma OAI.AlgorithmicThinTrees.Normalization.ContainedPacking.initial_gap line 77