OAI/MathematicalPhysics/Heisenberg/FiniteTilt.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Heisenberg.Selection.weightedTailline 11 - def
OAI.Heisenberg.Selection.tiltPartitionline 14 - def
OAI.Heisenberg.Selection.tiltLowerMassline 16 - lemma
OAI.Heisenberg.Selection.tail_le_partitionline 19 - lemma
OAI.Heisenberg.Selection.tiltPartition_posline 26 - lemma
OAI.Heisenberg.Selection.tilt_tail_denominatorline 33 - lemma
OAI.Heisenberg.Selection.tilt_lower_numeratorline 44 - theorem
OAI.Heisenberg.Selection.tilt_tail_boundline 55 - lemma
OAI.Heisenberg.Selection.tilt_mean_lowerline 71