OAI/Analysis/RCDHeat/LastTimeBins.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: LastTimeBins, LogBinLimit, NoBranchAtTime, AePathEquality, Nonbranching.

  1. lemma OAI.RegularPointCoordinates.exists_uniform_time_bin line 20
  2. lemma OAI.RegularPointCoordinates.tendsto_log_bin_budget line 76
  3. lemma OAI.RegularPointCoordinates.normalized_cut_density_bound line 106
  4. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.coupled_branch_mass_zero line 122
  5. lemma OAI.RegularPointCoordinates.ae_path_eq_of_ae_eval_lt_one line 274
  6. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compressed_optimal_plan_no_interior_branching line 323