OAI/Analysis/C0Absorption/Localization.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.C0Absorption.dist_le_of_local_interval line 13
  2. theorem OAI.C0Absorption.lipschitzOn_convex_of_local line 43
  3. theorem OAI.C0Absorption.lipschitz_convex_subtype_of_local line 71
  4. theorem OAI.C0Absorption.eventually_zero_of_not_tsupport line 95
  5. theorem OAI.C0Absorption.disjoint_supports_signed_lipschitz line 100
  6. theorem OAI.C0Absorption.nested_supports_signed_lipschitz line 141
  7. def OAI.C0Absorption.chi line 217
  8. def OAI.C0Absorption.cutoff line 219
  9. def OAI.C0Absorption.localG line 222
  10. def OAI.C0Absorption.localR line 225
  11. theorem OAI.C0Absorption.cutoff_nonneg line 228
  12. theorem OAI.C0Absorption.cutoff_le_one line 234
  13. theorem OAI.C0Absorption.localR_eq line 240
  14. theorem OAI.C0Absorption.localG_eq line 245
  15. theorem OAI.C0Absorption.cutoff_eq_zero line 249
  16. theorem OAI.C0Absorption.dist_lt_of_cutoff_ne_zero line 255
  17. theorem OAI.C0Absorption.localG_plateau line 260
  18. theorem OAI.C0Absorption.chi_lipschitz line 265
  19. theorem OAI.C0Absorption.cutoff_dist_le line 274
  20. theorem OAI.C0Absorption.localR_sup_lip line 289
  21. theorem OAI.C0Absorption.localR_lipschitz line 303
  22. theorem OAI.C0Absorption.localG_lipschitz line 345
  23. theorem OAI.C0Absorption.localG_sup line 354
  24. theorem OAI.C0Absorption.localR_sup line 371
  25. def OAI.C0Absorption.localGLinear line 380
  26. def OAI.C0Absorption.localRLinear line 386
  27. theorem OAI.C0Absorption.localRLinear_apply line 389
  28. def OAI.C0Absorption.localOp line 392
  29. theorem OAI.C0Absorption.localOp_nonzero_old line 395
  30. theorem OAI.C0Absorption.localOp_support line 412
  31. theorem OAI.C0Absorption.localR_support_ball line 420
  32. theorem OAI.C0Absorption.localOp_support_bound line 431