OAI/Analysis/RecursivePotentials/ZeroRootGeometry.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.RecursivePotentials.(instance at line 13) line 13
  2. theorem OAI.RecursivePotentials.XSigma_averaged_modulus line 19
  3. theorem OAI.RecursivePotentials.XJoined_averaged_modulus line 23
  4. lemma OAI.RecursivePotentials.ZeroTreeVector.norm_eq_common line 31
  5. lemma OAI.RecursivePotentials.ZeroTreeVector.norm_eq_second line 33
  6. lemma OAI.RecursivePotentials.ZeroTreeVector.inclusion_apply line 39
  7. lemma OAI.RecursivePotentials.ZeroTreeVector.norm_inclusion line 41
  8. lemma OAI.RecursivePotentials.ZeroTreeVector.inclusion_projection line 45
  9. lemma OAI.RecursivePotentials.ZeroTreeVector.projection_idem line 48
  10. lemma OAI.RecursivePotentials.ZeroTreeVector.projection_contracts line 54
  11. lemma OAI.RecursivePotentials.ZeroTreeSpace.inclusion_coe line 68
  12. lemma OAI.RecursivePotentials.ZeroTreeSpace.norm_inclusion line 72
  13. lemma OAI.RecursivePotentials.ZeroTreeSpace.inclusion_injective line 79
  14. lemma OAI.RecursivePotentials.ZeroTreeSpace.root_zero line 87
  15. theorem OAI.RecursivePotentials.ZeroTreeSpace.norm_eq_common line 94
  16. lemma OAI.RecursivePotentials.ZeroTreeSpace.projection_coe line 103
  17. lemma OAI.RecursivePotentials.ZeroTreeSpace.inclusion_projection line 108
  18. lemma OAI.RecursivePotentials.ZeroTreeSpace.projection_contracts line 115
  19. lemma OAI.RecursivePotentials.ZeroTreeSpace.projection_idem line 121
  20. lemma OAI.RecursivePotentials.ZeroTreeSpace.include_tail line 126
  21. theorem OAI.RecursivePotentials.ZeroTreeSpace.homogeneous_cubic line 131
  22. theorem OAI.RecursivePotentials.XZero_homogeneous_cubic line 152
  23. lemma OAI.RecursivePotentials.ZeroTreeVector.not_finite_dimensional line 162
  24. lemma OAI.RecursivePotentials.ZeroTreeSpace.continuous_P line 178
  25. lemma OAI.RecursivePotentials.ZeroTreeSpace.continuous_Q line 181
  26. lemma OAI.RecursivePotentials.ZeroTreeSpace.coordinate_projection line 184
  27. lemma OAI.RecursivePotentials.ZeroTreeSpace.tail_closed line 190
  28. def OAI.RecursivePotentials.ZeroTreeSpace.headCoordinates line 193
  29. lemma OAI.RecursivePotentials.ZeroTreeSpace.tail_eq_coordinate_kernel line 196
  30. lemma OAI.RecursivePotentials.ZeroTreeSpace.tail_finite_codimension line 213
  31. theorem OAI.RecursivePotentials.ZeroTreeSpace.finite_tail_dense line 218
  32. theorem OAI.RecursivePotentials.ZeroTreeSpace.not_finite_dimensional line 239
  33. lemma OAI.RecursivePotentials.FiniteRootedTree.depth_le_of_mem_ancestors line 253
  34. lemma OAI.RecursivePotentials.FiniteRootedTree.parent_ancestors_injective line 267
  35. def OAI.RecursivePotentials.FiniteRootedTree.path line 290
  36. lemma OAI.RecursivePotentials.FiniteRootedTree.path_apply line 292
  37. lemma OAI.RecursivePotentials.FiniteRootedTree.path_nonneg line 297
  38. lemma OAI.RecursivePotentials.FiniteRootedTree.path_root line 301
  39. lemma OAI.RecursivePotentials.FiniteRootedTree.path_upper line 304
  40. lemma OAI.RecursivePotentials.FiniteRootedTree.GlobalUpper.zero line 337
  41. theorem OAI.RecursivePotentials.FiniteRootedTree.path_fields line 342
  42. lemma OAI.RecursivePotentials.FiniteRootedTree.normSum_path line 350
  43. lemma OAI.RecursivePotentials.FiniteRootedTree.path_step line 354
  44. lemma OAI.RecursivePotentials.FiniteRootedTree.child_not_mem_ancestors line 370
  45. lemma OAI.RecursivePotentials.FiniteRootedTree.child_function_zero_on_ancestors line 378
  46. lemma OAI.RecursivePotentials.FiniteRootedTree.attached_upper line 384
  47. lemma OAI.RecursivePotentials.FiniteRootedTree.sum_sq_le_support line 414
  48. lemma OAI.RecursivePotentials.FiniteRootedTree.positivePart_sq_le line 426
  49. theorem OAI.RecursivePotentials.FiniteRootedTree.normSum_siblings_le line 432
  50. lemma OAI.RecursivePotentials.FiniteRootedTree.twice_coordinate_le_normSum line 487
  51. lemma OAI.RecursivePotentials.FiniteRootedTree.normSum_single line 503
  52. def OAI.RecursivePotentials.FiniteRootedTree.cutPath line 517
  53. lemma OAI.RecursivePotentials.FiniteRootedTree.cutPath_root line 519
  54. lemma OAI.RecursivePotentials.FiniteRootedTree.normSum_cutPath line 522
  55. lemma OAI.RecursivePotentials.FiniteRootedTree.cutPath_step line 544