OAI/Probability/InvariantIsing/Magnetic/MagneticPopulationContinuity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Continuity in positive field populations, with the same finite field alphabet and a bound independent of all optimizing parameters.

  1. theorem OAI.InvariantIsing.finiteMagneticFunctional_population_le line 12
  2. theorem OAI.InvariantIsing.finiteMagneticFunctional_tendsto_populations line 27