OAI/Probability/SKGap/Matrix/FixedNormRecipeEvent.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGapCutoff.Recipe.physicalNormBound line 14
  2. lemma OAI.SKGapCutoff.Recipe.physicalNormBound_pos line 16
  3. theorem OAI.SKGapCutoff.Recipe.gaussian_fixed_norm_recipe_probability line 20
  4. def OAI.SKGapCutoff.GapBridge.restrictUpper line 59
  5. lemma OAI.SKGapCutoff.GapBridge.measurable_restrictUpper line 62
  6. lemma OAI.SKGapCutoff.GapBridge.coupling_restrictUpper line 65
  7. def OAI.SKGapCutoff.GapBridge.edgeInteraction line 75
  8. lemma OAI.SKGapCutoff.GapBridge.edgeInteraction_restrictUpper line 77
  9. lemma OAI.SKGapCutoff.GapBridge.coupling_symmetric line 80
  10. lemma OAI.SKGapCutoff.GapBridge.coupling_diagonal line 87
  11. lemma OAI.SKGapCutoff.GapBridge.hamiltonian_zero line 90
  12. lemma OAI.SKGapCutoff.GapBridge.weight_zero line 96
  13. lemma OAI.SKGapCutoff.GapBridge.partition_zero line 100
  14. lemma OAI.SKGapCutoff.GapBridge.mass_zero line 104
  15. lemma OAI.SKGapCutoff.GapBridge.expectation_zero line 109
  16. lemma OAI.SKGapCutoff.GapBridge.variance_zero line 113
  17. lemma OAI.SKGapCutoff.GapBridge.flip_eq line 117
  18. def OAI.SKGapCutoff.GapBridge.pairConditional line 119
  19. lemma OAI.SKGapCutoff.GapBridge.conditionalExpectation_zero line 124
  20. lemma OAI.SKGapCutoff.GapBridge.pairConditional_flip line 130
  21. lemma OAI.SKGapCutoff.GapBridge.flipRate_complement line 135
  22. lemma OAI.SKGapCutoff.GapBridge.flipRate_eq_mass line 140
  23. lemma OAI.SKGapCutoff.GapBridge.pairConditional_residual line 149
  24. lemma OAI.SKGapCutoff.GapBridge.conditional_variance_projection line 158
  25. theorem OAI.SKGapCutoff.GapBridge.dirichlet_zero line 175
  26. theorem OAI.SKGapCutoff.GapBridge.measurePreserving_restrictUpper line 189
  27. lemma OAI.SKGapCutoff.GapBridge.continuous_coupling line 199
  28. lemma OAI.SKGapCutoff.GapBridge.poincare_iff_hasGap line 215
  29. lemma OAI.SKGapCutoff.GapBridge.measurableSet_poincareEvent line 223
  30. theorem OAI.SKGapCutoff.GapBridge.probability_poincare_eq line 232
  31. theorem OAI.SKGapCutoff.GapBridge.quenchedGap_iff_edgePoincare line 242