OAI/Analysis/RecursivePotentials/EquivalentNorms.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RecursivePotentials.weaklyNull_of_square_sum_bound line 13
  2. lemma OAI.RecursivePotentials.WeaklyNull.quotient_tendsto line 41
  3. lemma OAI.RecursivePotentials.WeaklyNull.approximate_cofinite line 55
  4. lemma OAI.RecursivePotentials.EquivalentNorm.upper_pos line 78
  5. lemma OAI.RecursivePotentials.EquivalentNorm.nonneg line 80
  6. lemma OAI.RecursivePotentials.EquivalentNorm.pos line 82
  7. lemma OAI.RecursivePotentials.EquivalentNorm.eq_zero_iff line 85
  8. lemma OAI.RecursivePotentials.EquivalentNorm.sub_le line 92
  9. lemma OAI.RecursivePotentials.EquivalentNorm.lipschitz_estimate line 97
  10. lemma OAI.RecursivePotentials.EquivalentNorm.exists_unit line 106
  11. lemma OAI.RecursivePotentials.EquivalentNorm.inner_nonempty line 114
  12. lemma OAI.RecursivePotentials.EquivalentNorm.inner_bddBelow line 120
  13. lemma OAI.RecursivePotentials.EquivalentNorm.inner_lower line 126
  14. lemma OAI.RecursivePotentials.EquivalentNorm.inner_upper line 132
  15. lemma OAI.RecursivePotentials.EquivalentNorm.modulus_le_sup line 141
  16. lemma OAI.RecursivePotentials.EquivalentNorm.witness line 155
  17. lemma OAI.RecursivePotentials.EquivalentNorm.extend_radius line 168
  18. lemma OAI.RecursivePotentials.EquivalentNorm.long_perturbation line 183
  19. lemma OAI.RecursivePotentials.EquivalentNorm.bounded_tree_step line 206
  20. theorem OAI.RecursivePotentials.bounded_trees_modulus_le_zero line 261
  21. theorem OAI.RecursivePotentials.bounded_trees_not_AUC line 316
  22. lemma OAI.RecursivePotentials.FiniteRootedTree.normSum_emb_siblings line 332
  23. lemma OAI.RecursivePotentials.weaklyNull_of_finsupp_bound line 344
  24. def OAI.RecursivePotentials.TreeSpace.basisVector line 380
  25. lemma OAI.RecursivePotentials.TreeSpace.basisVector_norm line 382
  26. lemma OAI.RecursivePotentials.TreeSpace.siblings_weaklyNull line 387
  27. def OAI.RecursivePotentials.TreeSpace.pathVector line 414
  28. lemma OAI.RecursivePotentials.TreeSpace.pathVector_norm line 416
  29. lemma OAI.RecursivePotentials.TreeSpace.pathVector_step line 421
  30. def OAI.RecursivePotentials.sequenceChildren line 436
  31. lemma OAI.RecursivePotentials.sequenceChildren_spec line 440
  32. lemma OAI.RecursivePotentials.XSigma_path_increments line 446
  33. theorem OAI.RecursivePotentials.XSigma_no_equivalent_AUC line 459
  34. def OAI.RecursivePotentials.TreeSpace.cutPathVector line 481
  35. lemma OAI.RecursivePotentials.TreeSpace.cutPathVector_norm line 483
  36. lemma OAI.RecursivePotentials.TreeSpace.cutPathVector_step line 488
  37. def OAI.RecursivePotentials.ZeroTreeSpace.basisVector line 509
  38. def OAI.RecursivePotentials.ZeroTreeSpace.pathVector line 514
  39. lemma OAI.RecursivePotentials.ZeroTreeSpace.inclusion_basisVector line 517
  40. lemma OAI.RecursivePotentials.ZeroTreeSpace.inclusion_pathVector line 523
  41. lemma OAI.RecursivePotentials.ZeroTreeSpace.basisVector_norm line 527
  42. lemma OAI.RecursivePotentials.ZeroTreeSpace.pathVector_norm line 532
  43. lemma OAI.RecursivePotentials.ZeroTreeSpace.pathVector_step line 537
  44. lemma OAI.RecursivePotentials.ZeroTreeSpace.siblings_weaklyNull line 543
  45. def OAI.RecursivePotentials.joinedNode line 584
  46. lemma OAI.RecursivePotentials.joinedNode_ne_root line 587
  47. lemma OAI.RecursivePotentials.joinedNode_parent line 590
  48. def OAI.RecursivePotentials.joinedChildren line 601
  49. lemma OAI.RecursivePotentials.joinedChildren_spec line 610
  50. lemma OAI.RecursivePotentials.XJoined_path_increments line 615
  51. lemma OAI.RecursivePotentials.XZero_path_increments line 630
  52. theorem OAI.RecursivePotentials.XJoined_no_equivalent_AUC line 645
  53. theorem OAI.RecursivePotentials.XZero_no_equivalent_AUC line 658
  54. lemma OAI.RecursivePotentials.EquivalentNorm.continuous line 675
  55. lemma OAI.RecursivePotentials.EquivalentNorm.norming_functional line 684
  56. lemma OAI.RecursivePotentials.EquivalentNorm.modulus_nonneg line 705
  57. theorem OAI.RecursivePotentials.bounded_trees_modulus_eq_zero line 729
  58. theorem OAI.RecursivePotentials.XSigma_one_sided_modulus_zero line 744
  59. theorem OAI.RecursivePotentials.XJoined_one_sided_modulus_zero line 761
  60. theorem OAI.RecursivePotentials.XZero_one_sided_modulus_zero line 777
  61. lemma OAI.RecursivePotentials.weighted_square_bound line 793