OAI/Probability/Ballisticity/Estimates/ObservedPotential.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.observedPotential line 17
  2. lemma OAI.DirectionalTransience.observedPotential_nonneg' line 20
  3. lemma OAI.DirectionalTransience.observedPotential_le line 25
  4. lemma OAI.DirectionalTransience.measurable_observedPotential line 28
  5. lemma OAI.DirectionalTransience.integrable_observedPotential line 32
  6. lemma OAI.DirectionalTransience.observedPotential_upper_start line 42
  7. lemma OAI.DirectionalTransience.observedPotential_lower_start line 49
  8. lemma OAI.DirectionalTransience.observedPotential_scaled_clip line 56
  9. lemma OAI.DirectionalTransience.observedPotential_lower_gain line 70
  10. lemma OAI.DirectionalTransience.observedPotential_above_floor line 76
  11. lemma OAI.DirectionalTransience.boundaryData_endpoints line 82
  12. lemma OAI.DirectionalTransience.selectedBoundaryData_endpoints line 87
  13. theorem OAI.DirectionalTransience.shared_boundary_potential_drift line 93