OAI/Probability/SKGap/Localization/LiteralInitialSystem.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.Recipe.initialU line 16
2. def OAI.SKGapCutoff.Recipe.initialP line 19
3. lemma OAI.SKGapCutoff.Recipe.ratio_dz_phi line 22
4. lemma OAI.SKGapCutoff.Recipe.initialP_ratio line 31
5. lemma OAI.SKGapCutoff.Recipe.literalInitial_partial_source line 38
6. lemma OAI.SKGapCutoff.Recipe.literalInitial_field line 49
7. lemma OAI.SKGapCutoff.Recipe.initial_scalar_equation line 64
8. lemma OAI.SKGapCutoff.Recipe.fixed_root_ratio_regular line 86
9. lemma OAI.SKGapCutoff.Recipe.SegmentRegular.coefficientBound line 99
10. lemma OAI.SKGapCutoff.Recipe.fixed_root_kernel_coefficientBound line 112
11. lemma OAI.SKGapCutoff.Recipe.fixed_root_ratio_coefficientBound line 125
12. def OAI.SKGapCutoff.Recipe.kernelSmallBudget line 148
13. def OAI.SKGapCutoff.Recipe.ratioSmallBudget line 150
14. lemma OAI.SKGapCutoff.Recipe.kernelSmallBudget_nonneg line 152
15. lemma OAI.SKGapCutoff.Recipe.ratioSmallBudget_nonneg line 156
16. lemma OAI.SKGapCutoff.Recipe.initial_kernel_bound line 161
17. lemma OAI.SKGapCutoff.Recipe.initial_ratio_bound line 170
18. lemma OAI.SKGapCutoff.Recipe.initialU_small line 178
19. lemma OAI.SKGapCutoff.Recipe.initialP_small line 186
20. lemma OAI.SKGapCutoff.Recipe.scaledMean_norm line 200
21. lemma OAI.SKGapCutoff.Recipe.logSlope_ratio line 212