OAI/Probability/SKGap/Localization/CompactTube.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SKGap.compact_perturbation_tube line 11
  2. lemma OAI.SKGap.compact_perturbation_tube_norm line 33
  3. def OAI.SKGap.conditionalScalarSize line 60
  4. lemma OAI.SKGap.continuousAt_conditionalSize line 64
  5. lemma OAI.SKGap.continuousAt_augmentedGram line 80
  6. abbrev OAI.SKGap.ScalarTimeDomain line 93
  7. def OAI.SKGap.scalarEqualitySet line 95
  8. def OAI.SKGap.scalarPerturbedPoint line 98
  9. lemma OAI.SKGap.continuous_scalarPerturbedPoint line 101
  10. lemma OAI.SKGap.scalarPerturbedPoint_domain line 106
  11. lemma OAI.SKGap.isCompact_scalarEqualitySet line 109
  12. theorem OAI.SKGap.scalar_conditional_neighborhood line 116