OAI/Probability/RadialTransition/InitialSlopes.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RadialTransition.phaseSlope line 10
  2. def OAI.RadialTransition.phaseCenter line 11
  3. def OAI.RadialTransition.targetSlope line 12
  4. def OAI.RadialTransition.phaseWindow line 13
  5. def OAI.RadialTransition.HasPhaseGroups line 15
  6. lemma OAI.RadialTransition.support_energy_small line 20
  7. lemma OAI.RadialTransition.phase_generator_distance line 34
  8. lemma OAI.RadialTransition.phase_groups_of_generators line 69