OAI/Dynamics/EntropyCounterexample/PredictionModelBridge.lean
11 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Problem340.ambientClockGate_model_eqline 13 - def
OAI.Problem340.PredictionModelBridge.modelEmbeddingline 20 - theorem
OAI.Problem340.PredictionModelBridge.modelEmbedding_mem_cylinderline 23 - theorem
OAI.Problem340.PredictionModelBridge.semiconj_predictionline 27 - theorem
OAI.Problem340.PredictionModelBridge.predictedClock_eqline 39 - def
OAI.Problem340.PredictionModelBridge.affineEmbeddingline 46 - theorem
OAI.Problem340.PredictionModelBridge.contDiff_affineEmbeddingline 49 - theorem
OAI.Problem340.PredictionModelBridge.affineEmbedding_mem_cylinderline 52 - theorem
OAI.Problem340.PredictionModelBridge.predictedClock_affine_eqline 56 - theorem
OAI.Problem340.PredictionModelBridge.contDiff_predictedClock_affineline 63 - theorem
OAI.Problem340.PredictionModelBridge.exists_predictedClock_affine_derivative_boundline 70