OAI/Probability/SLE/Multipoint/MultipointInitialParameters.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The source-normalized parameters for the physical multipoint estimate. All constants depend only on the SLE parameter and the finite order.

  1. def OAI.SLEExactGauge.Multipoint.sourceBeta line 15
  2. def OAI.SLEExactGauge.Multipoint.sourceTarget line 17
  3. lemma OAI.SLEExactGauge.Multipoint.source_parameters line 19
  4. lemma OAI.SLEExactGauge.Multipoint.sourceTarget_nonneg line 34
  5. lemma OAI.SLEExactGauge.Multipoint.physical_radius_level_parameters line 39
  6. lemma OAI.SLEExactGauge.Multipoint.physical_switch_level_parameters line 64
  7. lemma OAI.SLEExactGauge.Multipoint.sourceClockLevel_physical_activation line 77
  8. lemma OAI.SLEExactGauge.Multipoint.sourceTarget_coefficient line 92
  9. lemma OAI.SLEExactGauge.Multipoint.source_terminal_exponent line 95
  10. lemma OAI.SLEExactGauge.Multipoint.source_radius_targets_exponential line 101
  11. lemma OAI.SLEExactGauge.Multipoint.source_successBarrier_inv line 110