`OAI/Geometry/RCD/Transport/ResolvedSubplanEntropyBounds.lean`

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Mass-dependent bounds for the actual resolved branch entropy

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.resolved_subplan_entropy_bounds line 18