OAI/Probability/InvariantIsing/Cavity/CavityContinuousCutoff.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Bounded continuous cutoffs of the actual cavity factor. The radius cutoff equals one on the inner ball and vanishes outside the next ball.

  1. def OAI.InvariantIsing.cavityFactorSize line 16
  2. lemma OAI.InvariantIsing.cavityFactorSize_nonneg line 20
  3. lemma OAI.InvariantIsing.continuous_cavityLogFactor line 25
  4. def OAI.InvariantIsing.cavityCappedFactor line 31
  5. def OAI.InvariantIsing.cavityContinuousFactor line 41
  6. lemma OAI.InvariantIsing.continuous_cavityContinuousFactor line 46
  7. lemma OAI.InvariantIsing.cavityContinuousFactor_nonneg line 52
  8. lemma OAI.InvariantIsing.cavityContinuousFactor_le line 58
  9. def OAI.InvariantIsing.cavityBoundedFactor line 75
  10. lemma OAI.InvariantIsing.cavityContinuousFactor_lower_on_ball line 84
  11. theorem OAI.InvariantIsing.cavity_continuous_factor_normalizer_lower line 96
  12. abbrev OAI.InvariantIsing.CavityFactorBlocks line 126
  13. lemma OAI.InvariantIsing.continuous_cavityJointLogFactor line 129
  14. def OAI.InvariantIsing.cavityJointCappedFactor line 135
  15. def OAI.InvariantIsing.cavityJointCutoffFactor line 144
  16. lemma OAI.InvariantIsing.cavityJointCutoffFactor_eq line 159