OAI/Probability/ParisiFinite/OrdinaryInverseSpecial.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

Ordinary Inverse Special.

  1. theorem OAI.SeedInitialization.ordinary_inverse_special line 20
  2. def OAI.SeedInitialization.leading line 48
  3. theorem OAI.SeedInitialization.norm_leading line 51
  4. def OAI.SeedInitialization.leadingCoefficient line 54
  5. theorem OAI.SeedInitialization.norm_leadingCoefficient line 58
  6. theorem OAI.SeedInitialization.address_remainder_bound line 64
  7. theorem OAI.PointedTree.rootZ_WZ_vac_pair line 89
  8. theorem OAI.PointedTree.inner_rootY_WZ_rootZ_WZ line 94
  9. theorem OAI.PointedTree.norm_inner_high_leading line 106
  10. theorem OAI.SeedInitialization.norm_inner_address_bound line 122
  11. theorem OAI.SeedInitialization.gaussian_decay line 136
  12. def OAI.SeedInitialization.actualV line 147
  13. theorem OAI.SeedInitialization.norm_actualV line 150
  14. theorem OAI.SeedInitialization.actualV_eq line 153
  15. theorem OAI.SeedInitialization.norm_actualV_sub_initial_le line 158
  16. theorem OAI.SeedInitialization.tendsto_actualV_sub_initial line 175
  17. theorem OAI.SeedInitialization.tendsto_center_gap line 181
  18. def OAI.SeedInitialization.actualAddress line 200
  19. theorem OAI.SeedInitialization.norm_actualAddress line 203
  20. theorem OAI.SeedInitialization.tendsto_high_address_inner line 206
  21. theorem OAI.CoherentFock.tendsto_inner_coherent_escape line 237
  22. theorem OAI.CoherentFock.tendsto_inner_pre_coherent_escape line 256
  23. theorem OAI.CoherentFock.tendsto_inner_coherent_escape_all line 267
  24. theorem OAI.PointedTree.inner_spinPair_right line 298
  25. theorem OAI.PointedTree.tendsto_inner_rootZ_WZ_escape line 303
  26. theorem OAI.PointedTree.tendsto_inner_rootY_WZ_escape line 313
  27. theorem OAI.SeedInitialization.tendsto_norm_scaled_unit line 328
  28. theorem OAI.SeedInitialization.tendsto_inner_high line 338
  29. theorem OAI.SeedInitialization.tendsto_inner_actualLeading line 345
  30. theorem OAI.SeedInitialization.tendsto_inner_actualAddress line 351
  31. theorem OAI.CoherentFock.norm_coe_le_mass line 372
  32. theorem OAI.CoherentFock.norm_spinCoe_le_mass line 379
  33. theorem OAI.CoherentFock.tendsto_inner_coe_coherent_uniform line 385
  34. theorem OAI.CoherentFock.tendsto_inner_spinCoe_rootZ_uniform line 402
  35. theorem OAI.CoherentFock.tendsto_inner_spinCoe_rootY_uniform line 420
  36. theorem OAI.SeedInitialization.norm_inner_spinCoe_address_bound line 443
  37. theorem OAI.SeedInitialization.norm_inner_spinCoe_address_bound_of_mass line 451
  38. theorem OAI.SeedInitialization.tendsto_inner_high_uniform line 459
  39. theorem OAI.SeedInitialization.tendsto_inner_address_uniform line 469
  40. theorem OAI.SeedInitialization.cos_delta_error line 502
  41. theorem OAI.SeedInitialization.ordinaryCoefficient_error line 511
  42. theorem OAI.SeedInitialization.ordinary_component_error line 516
  43. theorem OAI.SeedInitialization.initial_forward_error line 523
  44. theorem OAI.SeedInitialization.initial_insertion_error line 538
  45. def OAI.SeedInitialization.ordinaryDisplacement line 557
  46. theorem OAI.SeedInitialization.ordinaryDisplacement_error_eq line 560
  47. theorem OAI.SeedInitialization.norm_ordinaryDisplacement_error line 569
  48. theorem OAI.SeedInitialization.tendsto_ordinaryDisplacement_error line 579
  49. theorem OAI.SeedInitialization.ordinaryDisplacement_bounded line 586
  50. theorem OAI.PointedTree.symmetry_rootX line 604
  51. def OAI.PointedTree.EvenUnitary.rootX line 616
  52. theorem OAI.SeedInitialization.odd_real_smul line 626
  53. theorem OAI.SeedInitialization.odd_actualV line 630
  54. theorem OAI.SeedInitialization.odd_initialDirection line 634
  55. def OAI.SeedInitialization.specialUnitary line 638
  56. theorem OAI.SeedInitialization.specialUnitary_apply line 643
  57. theorem OAI.SeedInitialization.initialMap_eq_ordinary line 647
  58. theorem OAI.SeedInitialization.actualAddress_odd line 656
  59. def OAI.SeedInitialization.addressMode line 675
  60. theorem OAI.SeedInitialization.norm_addressMode line 678
  61. theorem OAI.SeedInitialization.addressMode_odd line 681