OAI/Dynamics/EntropyCounterexample/ConcreteInputRegularity.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem340.ConcreteInputRegularity.Ambient line 12
  2. def OAI.Problem340.ConcreteInputRegularity.preparation line 14
  3. def OAI.Problem340.ConcreteInputRegularity.predictedClock line 16
  4. def OAI.Problem340.ConcreteInputRegularity.angular line 19
  5. def OAI.Problem340.ConcreteInputRegularity.ambientInput line 22
  6. theorem OAI.Problem340.ConcreteInputRegularity.predictor_preserves_norm line 25
  7. theorem OAI.Problem340.ConcreteInputRegularity.exists_contDiffOn_ambientInput_product line 30
  8. theorem OAI.Problem340.ConcreteInputRegularity.exists_contDiffOn_ambientInput line 121
  9. theorem OAI.Problem340.ConcreteInputRegularity.ambientInput_eq_zero_of_preparation_eq_zero line 130
  10. theorem OAI.Problem340.ConcreteInputRegularity.ambientInput_eq_zero_of_not_mem line 135
  11. theorem OAI.Problem340.ConcreteInputRegularity.horizontal_sphereOfComplex line 143
  12. theorem OAI.Problem340.ConcreteInputRegularity.phase_complexSphereHomeomorph line 154
  13. theorem OAI.Problem340.ConcreteInputRegularity.cutoff_complexSphereHomeomorph line 168
  14. theorem OAI.Problem340.ConcreteInputRegularity.angular_modelEmbedding line 180
  15. theorem OAI.Problem340.ConcreteInputRegularity.predictedClock_modelEmbedding line 188
  16. theorem OAI.Problem340.ConcreteInputRegularity.summand_modelEmbedding line 199
  17. theorem OAI.Problem340.ConcreteInputRegularity.ambientInput_modelEmbedding line 213
  18. theorem OAI.Problem340.ConcreteInputRegularity.continuous_modelEmbedding line 223
  19. theorem OAI.Problem340.ConcreteInputRegularity.exists_regular_baseInput line 227