OAI/Analysis/SegmentLenses/Radial.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Radial midpoint estimates and endpoint asymmetry

  1. def OAI.SegmentLenses.FiniteLaw.blend line 22
  2. theorem OAI.SegmentLenses.FiniteLaw.blend_expect line 29
  3. theorem OAI.SegmentLenses.norm_center_average line 39
  4. theorem OAI.SegmentLenses.norm_displacement_average line 46
  5. theorem OAI.SegmentLenses.finite_unequal_radius_tail line 57
  6. theorem OAI.SegmentLenses.completed_unequal_radius_tail line 145
  7. theorem OAI.SegmentLenses.averaged_tail_bound line 176
  8. theorem OAI.SegmentLenses.norm_center_le_average line 202
  9. theorem OAI.SegmentLenses.sharp_radial_comparison line 216
  10. theorem OAI.SegmentLenses.radial_tail_bound line 228
  11. theorem OAI.SegmentLenses.original_coefficient_average line 236
  12. theorem OAI.SegmentLenses.strong_finite_head_average line 254
  13. theorem OAI.SegmentLenses.strong_predual_averaged_witness line 277
  14. theorem OAI.SegmentLenses.strong_predual_all_radius_average line 307
  15. theorem OAI.SegmentLenses.strong_fullDual_all_radius_average_of_reflexive line 317