OAI/Probability/GaussianInformation/Dyadic/ChartGeometry.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RepeatedLocalization.eCoordinate line 11
  2. def OAI.RepeatedLocalization.eChart line 13
  3. lemma OAI.RepeatedLocalization.norm_eCoordinate_le_half line 16
  4. lemma OAI.RepeatedLocalization.chart_height_lipschitz line 35
  5. lemma OAI.RepeatedLocalization.eChart_dist_le line 60
  6. def OAI.RepeatedLocalization.firstCoordinates line 74
  7. lemma OAI.RepeatedLocalization.firstCoordinates_lipschitz line 77
  8. def OAI.RepeatedLocalization.normalizedChart line 89
  9. lemma OAI.RepeatedLocalization.normalizedChart_norm_le line 92
  10. lemma OAI.RepeatedLocalization.normalizedChart_measurable line 115
  11. def OAI.RepeatedLocalization.normalizedGridBase line 120
  12. lemma OAI.RepeatedLocalization.normalizedGrid_mem_iff line 123
  13. lemma OAI.RepeatedLocalization.normalizedGrid_valid_of_inter line 154
  14. lemma OAI.RepeatedLocalization.normalizedGrid_child_mem line 179
  15. lemma OAI.RepeatedLocalization.measure_normalizedGrid_le line 195
  16. def OAI.RepeatedLocalization.DyadicSpread line 223
  17. lemma OAI.RepeatedLocalization.DyadicSpread.child_floor line 227
  18. def OAI.RepeatedLocalization.gridConstant line 241
  19. def OAI.RepeatedLocalization.tubeConstant line 242
  20. lemma OAI.RepeatedLocalization.gridConstant_nonneg line 244
  21. lemma OAI.RepeatedLocalization.tubeConstant_ge_one line 245
  22. lemma OAI.RepeatedLocalization.dyadic_tube_tail line 249