OAI/Geometry/RCD/Transport/AsymmetricMidpointReplacement.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Replacing a midpoint region with unequal endpoint bounds

The replacement is an actual subplan with the original endpoint marginals. Its lower support-volume bound retains each endpoint density, so it can be used when only the source bound stays finite in a concentration limit.

  1. theorem OAI.RegularPointCoordinates.FullCD.replace_midpoint_region_asymmetric line 20