OAI/Geometry/RCD/Metric/ShiftedRadonSum.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Integrating two full Bochner density contributions

  1. theorem OAI.RegularPointCoordinates.integral_shifted_radon_sum_le line 14