OAI/Analysis/RCDHeat/NormalizedSubplan.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: NormalizedSubplan, OriginalPlanCompression, FiniteCDCompressedPlan, HereditaryCD, EvaluationFactor.

  1. theorem OAI.RegularPointCoordinates.optimalPlan_normalized_subplan line 21
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.optimal_plan_ac_marginal_compression line 70
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.exists_bounded_compression_fullCD_plan line 166
  4. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compressed_optimal_plan_fullCD line 212
  5. lemma OAI.RegularPointCoordinates.NoncollapsedRCD.evaluation_conditionalPair_diagonal line 275
  6. lemma OAI.RegularPointCoordinates.NoncollapsedRCD.compressed_plan_evaluation_set_factor line 341