OAI/Dynamics/StandardMap/EndpointObservations.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StandardMapEntropy.shortfallObservationFunction line 11
  2. lemma OAI.StandardMapEntropy.shortfallObservationFunction_lipschitz line 12
  3. lemma OAI.StandardMapEntropy.testObservation_zero line 14
  4. lemma OAI.StandardMapEntropy.shortfallObservationFunction_zero line 15
  5. structure OAI.StandardMapEntropy.EndpointObservation line 16
  6. def OAI.StandardMapEntropy.EndpointObservation.value line 25
  7. def OAI.StandardMapEntropy.testEndpoint line 27
  8. def OAI.StandardMapEntropy.shortfallEndpoint line 38
  9. lemma OAI.StandardMapEntropy.testEndpoint_value line 47
  10. lemma OAI.StandardMapEntropy.shortfallEndpoint_value line 48
  11. def OAI.StandardMapEntropy.EndpointObservation.inWindow line 50
  12. def OAI.StandardMapEntropy.intervalInWindow line 53
  13. lemma OAI.StandardMapEntropy.testEndpoint_inWindow line 55
  14. lemma OAI.StandardMapEntropy.shortfallEndpoint_inWindow line 60
  15. def OAI.StandardMapEntropy.endpointBridgeEvent line 62
  16. def OAI.StandardMapEntropy.CriticalScaleSequence.LimitLaws.selected line 65
  17. lemma OAI.StandardMapEntropy.CriticalScaleSequence.endpoint_bridge_null line 67