OAI/Probability/ParisiFinite/GramBlock.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Gram Block.

  1. def OAI.SKCavity.GramBlock line 60
  2. lemma OAI.SKCavity.isClosed_GramBlock line 64
  3. lemma OAI.SKCavity.GramArrays_block line 71
  4. lemma OAI.SKCavity.blockSupport_Gram line 74
  5. lemma OAI.SKCavity.support_event_nonempty line 85
  6. def OAI.SKCavity.rowBall line 93
  7. def OAI.SKCavity.blockBall line 96
  8. lemma OAI.SKCavity.isOpen_rowBall line 99
  9. lemma OAI.SKCavity.isOpen_blockBall line 104
  10. lemma OAI.SKCavity.isOpen_patternBlock line 109
  11. lemma OAI.SKCavity.exists_supported_approx_duplication line 115
  12. theorem OAI.SKCavity.exists_supported_duplication_last line 171
  13. def OAI.SKCavity.permBlock line 210
  14. lemma OAI.SKCavity.continuous_permBlock line 213
  15. lemma OAI.SKCavity.blockLaw_map_perm line 217
  16. lemma OAI.SKCavity.permBlock_support line 222
  17. def OAI.SKCavity.headPerm line 232
  18. lemma OAI.SKCavity.headPerm_old line 235
  19. lemma OAI.SKCavity.headPerm_last line 238
  20. theorem OAI.SKCavity.exists_supported_duplication line 245
  21. def OAI.SKCavity.gramForm line 292
  22. def OAI.SKCavity.gramDelta line 295
  23. lemma OAI.SKCavity.gramForm_symm line 297
  24. lemma OAI.SKCavity.gramForm_delta_left line 308
  25. lemma OAI.SKCavity.gramForm_delta_delta line 312
  26. lemma OAI.SKCavity.gramForm_sub_left line 316
  27. lemma OAI.SKCavity.gramForm_sub_right line 320
  28. lemma OAI.SKCavity.gramForm_smul_left line 324
  29. lemma OAI.SKCavity.gramForm_smul_right line 328
  30. lemma OAI.SKCavity.gramForm_sum_left line 340
  31. lemma OAI.SKCavity.gramForm_sum_right line 351
  32. lemma OAI.SKCavity.gramForm_coordinate_sq_le line 364
  33. def OAI.SKCavity.gramCluster line 375
  34. lemma OAI.SKCavity.gramForm_clusters line 377
  35. lemma OAI.SKCavity.gramForm_delta_cluster line 382
  36. lemma OAI.SKCavity.gramCluster_norm_bound line 387
  37. theorem OAI.SKCavity.gram_two_cluster_bound line 405
  38. lemma OAI.SKCavity.duplication_preserves_low line 439
  39. structure OAI.SKCavity.TwoClusters line 460
  40. def OAI.SKCavity.TwoClusters.swap line 481
  41. def OAI.SKCavity.TwoClusters.growLeft line 502
  42. def OAI.SKCavity.TwoClusters.growRight line 561
  43. def OAI.SKCavity.TwoClusters.replicate line 577
  44. theorem OAI.SKCavity.TwoClusters.root_overlap_eq line 584
  45. theorem OAI.SKCavity.supported_triangle_ordered line 604
  46. theorem OAI.SKCavity.supported_triangle_ultrametric line 635