OAI/Analysis/LipschitzEquivalence/RadialBudget.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LipschitzCounterexample.RadialBudget.c line 11
  2. def OAI.LipschitzCounterexample.RadialBudget.cutoff line 12
  3. def OAI.LipschitzCounterexample.RadialBudget.gamma line 14
  4. def OAI.LipschitzCounterexample.RadialBudget.potential line 16
  5. theorem OAI.LipschitzCounterexample.RadialBudget.c_pos line 18
  6. theorem OAI.LipschitzCounterexample.RadialBudget.cutoff_pos line 19
  7. theorem OAI.LipschitzCounterexample.RadialBudget.cutoff_lt_one line 20
  8. theorem OAI.LipschitzCounterexample.RadialBudget.log_bound line 24
  9. theorem OAI.LipschitzCounterexample.RadialBudget.gamma_formula line 28
  10. theorem OAI.LipschitzCounterexample.RadialBudget.gamma_nonneg line 31
  11. theorem OAI.LipschitzCounterexample.RadialBudget.denominator_deriv line 37
  12. theorem OAI.LipschitzCounterexample.RadialBudget.denominator_monotone line 45
  13. theorem OAI.LipschitzCounterexample.RadialBudget.gamma_antitone line 55
  14. theorem OAI.LipschitzCounterexample.RadialBudget.potential_nonneg line 66
  15. theorem OAI.LipschitzCounterexample.RadialBudget.potential_le line 74
  16. theorem OAI.LipschitzCounterexample.RadialBudget.potential_deriv line 83
  17. theorem OAI.LipschitzCounterexample.RadialBudget.weighted_formula line 93
  18. theorem OAI.LipschitzCounterexample.RadialBudget.primitive_integral line 98
  19. theorem OAI.LipschitzCounterexample.RadialBudget.step_interior line 113
  20. theorem OAI.LipschitzCounterexample.RadialBudget.step_zero line 136
  21. theorem OAI.LipschitzCounterexample.RadialBudget.step line 151
  22. theorem OAI.LipschitzCounterexample.RadialBudget.partial_budget line 170
  23. theorem OAI.LipschitzCounterexample.RadialBudget.budget line 178