OAI/Probability/ParisiFinite/LowVector.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Low Vector.

  1. def OAI.SeedInitialization.lowVector line 20
  2. theorem OAI.SeedInitialization.norm_lowVector line 23
  3. theorem OAI.SeedInitialization.ordinary_insertion_eq line 26
  4. theorem OAI.SeedInitialization.inner_lowVector_initial line 37
  5. theorem OAI.SeedInitialization.tendsto_norm_ordinaryDisplacement line 49
  6. def OAI.SeedInitialization.initializedInsertion line 63
  7. theorem OAI.SeedInitialization.initializedInsertion_coe line 66
  8. theorem OAI.SeedInitialization.norm_initializedInsertion line 73
  9. theorem OAI.SeedInitialization.initializedInsertion_error line 76
  10. theorem OAI.SeedInitialization.tendsto_initializedInsertion_error line 86
  11. theorem OAI.SeedInitialization.tendsto_lowVector_initial line 95
  12. theorem OAI.SeedInitialization.tendsto_initialized_initial line 110
  13. theorem OAI.SeedInitialization.tendsto_initial_visibility line 129
  14. theorem OAI.SeedInitialization.initial_visibility_nonzero line 145
  15. def OAI.SeedInitialization.preVacuum line 157
  16. theorem OAI.SeedInitialization.spinCoe_preVacuum line 159
  17. theorem OAI.SeedInitialization.spinMass_preVacuum line 165
  18. theorem OAI.SeedInitialization.radius_preVacuum line 170
  19. def OAI.SeedInitialization.preLow line 173
  20. theorem OAI.SeedInitialization.spinCoe_preLow line 175
  21. theorem OAI.SeedInitialization.mass_preLow line 178
  22. theorem OAI.SeedInitialization.radius_preLow line 184
  23. theorem OAI.SeedInitialization.bounded_preLow line 188
  24. theorem OAI.SeedInitialization.tendsto_inner_low_high line 196
  25. theorem OAI.SeedInitialization.tendsto_inner_low_address line 203
  26. theorem OAI.SeedInitialization.tendsto_inner_error_unit line 212
  27. theorem OAI.SeedInitialization.tendsto_initialized_high line 221
  28. theorem OAI.SeedInitialization.tendsto_initialized_address line 231
  29. theorem OAI.SeedInitialization.inner_lowVector_creation line 246
  30. theorem OAI.SeedInitialization.tendsto_displacement_initialized line 258
  31. theorem OAI.SeedInitialization.tendsto_low_rootShift line 274
  32. theorem OAI.SeedInitialization.tendsto_initialized_rootShift line 291
  33. theorem OAI.SeedInitialization.tendsto_initialized_treeEnergy line 304
  34. theorem OAI.SeedInitialization.tendsto_initialization_ordinaryValue line 314
  35. theorem OAI.ForwardControl.scaled_residual_bound line 331
  36. theorem OAI.ForwardControl.actual_scaled_flip_bound line 353
  37. theorem OAI.CoherentFock.WZ_difference_le line 370
  38. theorem OAI.CoherentFock.tailBound_le_second line 387
  39. theorem OAI.CoherentFock.WZ_spinCoe_sub_le line 395
  40. theorem OAI.CoherentFock.WZ_spinCoe_difference line 412
  41. theorem OAI.ForwardControl.actual_scaled_flip_tendsto line 434
  42. theorem OAI.CoherentFock.echo_ordinary_error line 459
  43. theorem OAI.CoherentFock.tendsto_moving_corrected_echo line 478
  44. def OAI.CoherentFock.spinPacket line 503
  45. theorem OAI.CoherentFock.inner_spinPacket line 506
  46. theorem OAI.CoherentFock.inner_spinPacket_creation line 521
  47. theorem OAI.CoherentFock.tendsto_norm_sq_of_inner line 532
  48. theorem OAI.CoherentFock.tendsto_kernel_of_gram line 540
  49. theorem OAI.CoherentFock.tendsto_inner_spinPacket line 553
  50. theorem OAI.CoherentFock.tendsto_inner_spinPacket_creation line 574
  51. theorem OAI.CoherentFock.analyticAt_norm_sq_of_inner line 599
  52. theorem OAI.CoherentFock.analyticAt_kernel_of_gram line 608
  53. theorem OAI.CoherentFock.analyticAt_phase_of_gram line 619
  54. theorem OAI.CoherentFock.analyticAt_inner_spinPacket line 631
  55. theorem OAI.CoherentFock.spinPacket_apply line 659
  56. theorem OAI.CoherentFock.spinPacket_smul line 663
  57. theorem OAI.CoherentFock.spinPacket_sum line 668
  58. theorem OAI.CoherentFock.act_spinPacket line 674
  59. theorem OAI.CoherentFock.WZ_spinPacket line 681