OAI/Geometry/CylinderCovering/Rational/DictionaryCoefficients.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RationalDictionary.coefficientBaseDomain_measurable line 13
  2. lemma OAI.RationalDictionary.labelMap_coefficientBaseDomain_iff line 22
  3. lemma OAI.RationalDictionary.labelMap_coefficientBaseDomain line 35
  4. lemma OAI.RationalDictionary.coefficientBaseDomain_area line 46
  5. lemma OAI.RationalDictionary.energyDensity_dictionary line 57
  6. lemma OAI.RationalDictionary.energy_dictionary line 67
  7. lemma OAI.RationalDictionary.ceiling_dictionary_integral line 83
  8. lemma OAI.RationalDictionary.half_tendsto_right line 105
  9. lemma OAI.RationalDictionary.coefficientFactor_tendsto line 115
  10. lemma OAI.RationalDictionary.c0_cube line 121
  11. lemma OAI.RationalDictionary.c0_fifth line 126
  12. lemma OAI.RationalDictionary.uncenteredEnergy_tendsto line 131
  13. lemma OAI.RationalDictionary.uncenteredCeiling_tendsto line 146
  14. lemma OAI.RationalDictionary.coefficientGap_tendsto line 159
  15. lemma OAI.RationalDictionary.exists_positive_coefficientGap line 166
  16. theorem OAI.RationalDictionary.coefficient_limits line 173