OAI/Probability/SATComputability/InterpolationUpper.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.upperDatum_integrable_norm line 18
2. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.datumRoot_integrable_firstMoment line 31
3. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.upperCountMean_bound_firstMoment line 54
4. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.integrable_mixedLogAvg line 104
5. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.integrable_mixedNormalizedAvg line 128
6. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.integrable_mixedLeafAvg line 149
7. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.integral_mixedLogAvg_negative_tail line 168
8. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.integrable_insertionPoint line 201
9. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.integral_expected_insertionPoint line 218
10. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.integratedMixedLeaf_identity line 237
11. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.insertionCoefficient_combination_nonneg line 260
12. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.expected_insertionCoefficient_nonneg line 278
13. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.integratedMixedLeaf_combination_nonneg line 299
14. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.mixedQMoment_combination_nonneg line 321
15. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.integral_mixedLog_combination_nonpos line 342
16. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.integrable_mixedEnergyAvg line 374
17. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.integral_mixedNormalizedAvg_limit line 392
18. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.integral_mixedEnergy_combination_nonpos line 423
19. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.integral_mixedRoot_combination_nonpos line 471
20. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.freshRoot_mean_sub_firstMoment line 492
21. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.freshRoot_replacement_firstMoment line 534
22. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.datumRoot_conditional_replacement_firstMoment line 562
23. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.upperCountMean_replacement_firstMoment line 594
24. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.upperPoissonCount_bound_firstMoment line 645
25. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.allocatedDatumRoot_integrable line 681
26. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.upperAllocated_integrable line 708
27. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.upperAllocatedMean line 734
28. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.upperCountMean_separable line 777
29. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.activeCountMean_bound line 801
30. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.upperSelectedCountMean_bound line 843
31. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.upperPoisson_cavity_separable line 870
32. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.upperCountMean_real_firstMoment line 901
33. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.upperCountMean_real_terminal line 967
34. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.activeCountMean_site line 1008
35. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.finiteTrial_upper_fixedField line 1066
36. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.PrescribedTree.finiteTrial_pressure_le line 1129
37. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.finiteHierarchy_pressure_le line 1176
38. lemma OAI.FixedClauseThreshold.Computability.PositiveInterpolation.pressure_le_functional line 1194