OAI/Probability/ParisiFinite/IdentityErrorFinSumTendsto.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Identity Error Fin Sum Tendsto.

  1. theorem OAI.ForwardControl.identity_error_finSum_tendsto line 38
  2. theorem OAI.ForwardControl.split_forward_tendsto line 49
  3. theorem OAI.PointedTree.actual_direction_from_split line 65
  4. def OAI.FiniteError.envelope line 93
  5. theorem OAI.FiniteError.envelope_nonneg line 95
  6. theorem OAI.FiniteError.le_envelope line 98
  7. theorem OAI.FiniteError.envelope_tendsto_zero line 101
  8. theorem OAI.FiniteError.scaled_envelope_tendsto_zero line 107
  9. theorem OAI.CoherentFock.tail_bounds_of_radius_mass line 125
  10. theorem OAI.PointedTree.packet_forward_of_phases line 140
  11. theorem OAI.PointedTree.packet_root_forward_of_phases line 160
  12. theorem OAI.PointedTree.packet_direction_tendsto line 177
  13. theorem OAI.List.range_map_getD_eq line 210
  14. theorem OAI.List.reverse_range_map_getD_eq line 218
  15. def OAI.PointedTree.pulseSequence line 232
  16. theorem OAI.PointedTree.pulseSequence_clocks line 235
  17. theorem OAI.PointedTree.phase_tendsto_of_scaled line 265
  18. theorem OAI.PointedTree.packet_direction_envelope_tendsto line 274
  19. theorem OAI.PointedTree.packet_zero_clock_from_vacuum line 296
  20. theorem OAI.ForwardControl.scaled_flip_from_limits line 350
  21. theorem OAI.PointedTree.modeFock_probe_insertion line 401
  22. theorem OAI.PointedTree.actual_flip_mode_tendsto line 413
  23. theorem OAI.RootSpin.exists_mixer_frame line 450
  24. theorem OAI.CoherentFock.phaseZ_eq_act_exp line 475
  25. theorem OAI.RootSpin.exp_rotated_Z line 490
  26. theorem OAI.SpinOperators.act_conj_comp line 505
  27. theorem OAI.CoherentFock.probePhase_eq_act_exp line 515
  28. theorem OAI.QuaternionControl.skewX_eq line 533
  29. theorem OAI.QuaternionControl.skewY_eq line 535
  30. theorem OAI.QuaternionControl.skewZ_eq line 537
  31. def OAI.QuaternionControl.axisAngle line 540
  32. def OAI.QuaternionControl.axisProjection line 542
  33. theorem OAI.QuaternionControl.spinGen_eq_rotated line 547
  34. theorem OAI.SpinOperators.act_prod line 570
  35. theorem OAI.QuaternionControl.real_smul_skew line 582
  36. theorem OAI.QuaternionControl.exp_skewX line 588
  37. theorem OAI.QuaternionControl.phase_product_eq line 597
  38. def OAI.PointedTree.projectionPhase line 619
  39. theorem OAI.PointedTree.rotated_coordinate line 622
  40. theorem OAI.PointedTree.selective_phase_control line 631
  41. theorem OAI.CoherentFock.short_large_phase line 672
  42. theorem OAI.CoherentFock.imaginary_projection_difference line 682