OAI/Analysis/PathSelection/LossPullbacks.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Discrete and logarithmic loss pullbacks, summable majorants and derivative transfer.

  1. lemma OAI.DegeneratingTrees.summable_comp_four line 15
  2. lemma OAI.DegeneratingTrees.dyadic_span_bound line 37
  3. lemma OAI.DegeneratingTrees.admissible_max_of_shell_bounds line 62
  4. lemma OAI.DegeneratingTrees.admissible_pullback_of_shell_control line 83
  5. lemma OAI.DegeneratingTrees.summable_comp_mod line 113
  6. lemma OAI.DegeneratingTrees.summable_shell_window line 128
  7. theorem OAI.DegeneratingTrees.log_scale_shell_control line 152
  8. lemma OAI.DegeneratingTrees.summable_strict_majorant line 247
  9. theorem OAI.DegeneratingTrees.AdmissibleAngularLoss.pullback_log_scale line 300
  10. def OAI.DegeneratingTrees.dyadicLossIndex line 384
  11. lemma OAI.DegeneratingTrees.tendsto_dyadicLossIndex line 386
  12. lemma OAI.DegeneratingTrees.dyadicLossIndex_shell line 390
  13. lemma OAI.DegeneratingTrees.admissible_dyadic_step line 413
  14. theorem OAI.DegeneratingTrees.admissible_strict_absorption line 438
  15. lemma OAI.DegeneratingTrees.logarithmic_clock_slopes line 461
  16. theorem OAI.DegeneratingTrees.AdmissibleAngularLoss.pullback_log_derivative line 479
  17. lemma OAI.DegeneratingTrees.logarithmic_clock_slopes_pos line 498
  18. lemma OAI.DegeneratingTrees.unit_to_dyadic_shells line 516
  19. theorem OAI.DegeneratingTrees.strict_loss_from_unit_shells line 528