AsymmetricMidpoint.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Midpoint transport with separately controlled endpoint densities

The distance-Laplacian construction needs concentration of one endpoint at a pole. Equal endpoint bounds lose all control in that limit. Here the actual CD inequality retains the two inverse density powers separately.

theorem OAI.RegularPointCoordinates.cd_midpoint_renyi_lower_asymmetric line 21
theorem OAI.RegularPointCoordinates.FullCD.exists_midpoint_ac_support_bound_asymmetric line 63
def OAI.RegularPointCoordinates.midpointSupportFactor line 102
Source documentation
The volume factor from the two separately bounded endpoint densities.
```
noncomputable def midpointSupportFactor (K : ℝ) (n : ℕ) (D : ℝ)
    (C₀ C₁ : ℝ≥0∞) : ℝ≥0∞ :=
…
```
theorem OAI.RegularPointCoordinates.midpointSupportFactor_scale line 106