OAI/Geometry/RCD/Metric/EndpointWeightApproximation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

L1 endpoint approximation under a common marginal bound

A bounded continuous path weight can be multiplied by an integrable endpoint observable. Approximation errors are uniform over all plans whose selected marginal is dominated by twice the same finite measure.

  1. theorem OAI.RegularPointCoordinates.integrable_endpoint_of_domination line 19
  2. theorem OAI.RegularPointCoordinates.integral_endpoint_weight_error line 26