OAI/Computability/MinUncut/Estimates/TableLawPacking.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MinUncut.FiniteGaussian.sourceTableline 15 - lemma
OAI.MinUncut.FiniteGaussian.sourceTable_packedline 18 - lemma
OAI.MinUncut.FiniteGaussian.table_integral_packline 23 - lemma
OAI.MinUncut.FiniteGaussian.sourceTest_integrableline 44 - lemma
OAI.MinUncut.FiniteGaussian.sourceTest_inner_integrableline 52 - lemma
OAI.MinUncut.FiniteGaussian.sourceTest_outer_integrableline 64 - lemma
OAI.MinUncut.FiniteGaussian.table_integral_productline 77