OAI/Geometry/CAT0Fillings/Slices/NormalBudget.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CAT0Fillings.Slicing.NormalApprox.normal line 18
  2. lemma OAI.CAT0Fillings.Slicing.NormalApprox.integral_zero line 28
  3. lemma OAI.CAT0Fillings.Slicing.NormalApprox.slice_tree line 33
  4. theorem OAI.CAT0Fillings.Slicing.NormalApprox.ae_slice line 38
  5. lemma OAI.CAT0Fillings.Slicing.superlevelSlice_offDomain line 100
  6. lemma OAI.CAT0Fillings.Slicing.superlevelSlice_testClass_continuous line 107
  7. theorem OAI.CAT0Fillings.Slicing.measurableSet_slice_normalApprox line 119
  8. lemma OAI.CAT0Fillings.Slicing.NormalApprox.current line 132
  9. lemma OAI.CAT0Fillings.Slicing.normalApprox_of_integral line 139
  10. lemma OAI.CAT0Fillings.Slicing.normalApprox_zero line 146
  11. def OAI.CAT0Fillings.Slicing.normalSlice line 149
  12. lemma OAI.CAT0Fillings.Slicing.normalSlice_approx line 155
  13. lemma OAI.CAT0Fillings.Slicing.ae_normalSlice_eq line 164
  14. lemma OAI.CAT0Fillings.Slicing.measurable_normalSlice_family line 172
  15. def OAI.CAT0Fillings.Slicing.NormalApproxAt line 199
  16. lemma OAI.CAT0Fillings.Slicing.normalApproxAt_iff_closed line 205
  17. lemma OAI.CAT0Fillings.Slicing.measurableSet_normalApproxAt line 222
  18. def OAI.CAT0Fillings.Slicing.NormalApprox.cost line 234
  19. lemma OAI.CAT0Fillings.Slicing.NormalApprox.cost_spec line 240
  20. lemma OAI.CAT0Fillings.Slicing.NormalApprox.cost_le line 247
  21. lemma OAI.CAT0Fillings.Slicing.measurable_normalApprox_cost line 253
  22. lemma OAI.CAT0Fillings.Slicing.NormalApprox.mass_le_cost line 260
  23. lemma OAI.CAT0Fillings.Slicing.normalApproxAt_zero line 267
  24. lemma OAI.CAT0Fillings.Slicing.NormalApprox.cost_zero line 282
  25. lemma OAI.CAT0Fillings.Slicing.exists_integrable_subsequence_bound line 285