OAI/Probability/InvariantIsing/Magnetic/MagneticSlabZero.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Relative derivative bounds for the ordinary Gaussian root step. No positive cascade exponent is needed at this level.

  1. lemma OAI.InvariantIsing.magneticScalarSlabJet_zero_third_relative line 14
  2. lemma OAI.InvariantIsing.magneticScalarSlabJet_zero_fourth_relative line 38
  3. lemma OAI.InvariantIsing.magneticScalarInverse_zero_weighted_second_bound line 69