OAI/Probability/SLE/Gauge/SerpentineCenteredMass.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The stopped physical experiment under the actual finite centered law. Both its mass and its successful completion are observable at the front.

  1. lemma OAI.SLEExactGauge.Serpentine.experimentSteps_add_one line 17
  2. lemma OAI.SLEExactGauge.Serpentine.experiment_front_eq line 29
  3. lemma OAI.SLEExactGauge.Serpentine.exponential_prefactor_quadratic_cost line 37
  4. theorem OAI.SLEExactGauge.Serpentine.uniform_serpentine_centered_stopped_mass line 51