OAI/Geometry/RCD/Transport/MidpointMinMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Both endpoint masses in the midpoint estimate

  1. theorem OAI.RegularPointCoordinates.midpoint_root_bound_to_min_mass line 13

    Source documentation

    Keeping the smaller endpoint mass preserves the factor two needed for the isodiametric argument with reflected sets.

    theorem midpoint_root_bound_to_min_mass {n : ℕ} (hn : 0 < n)
    {a b c d : ℝ≥0∞}
    (h : c*(a^(1/(n:ℝ))+b^(1/(n:ℝ))) ≤ d^(1/(n:ℝ))) :
    (2*c)^n*min a b ≤ d := by
…