OAI/Probability/SKFluctuations/CavityMixedInsertion.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Cavity Mixed Insertion.

  1. def OAI.SKFluctuations.Cavity.cutLowError line 21
  2. theorem OAI.SKFluctuations.Cavity.cutFullVariance_biaffine line 24
  3. theorem OAI.SKFluctuations.Cavity.mixed_cutDisorderExpect line 37
  4. theorem OAI.SKFluctuations.Cavity.third_low_remainder line 86
  5. theorem OAI.SKFluctuations.Cavity.mixed_jet_integral line 114
  6. theorem OAI.SKFluctuations.Cavity.third_low_mixed_remainder line 122
  7. def OAI.SKFluctuations.Cavity.thirdProductJet line 145
  8. theorem OAI.SKFluctuations.Cavity.thirdProductJet_hasDerivAt line 150
  9. def OAI.SKFluctuations.Cavity.cutLowJet line 165
  10. def OAI.SKFluctuations.Cavity.cutMixedJet line 173
  11. theorem OAI.SKFluctuations.Cavity.cutFullVariance_continuous_l line 180
  12. theorem OAI.SKFluctuations.Cavity.cutFullVariance_continuous_t line 186
  13. theorem OAI.SKFluctuations.Cavity.cutLowJet_continuous_l line 192
  14. theorem OAI.SKFluctuations.Cavity.cutLowJet_continuous_t line 200
  15. theorem OAI.SKFluctuations.Cavity.cutMixedJet_continuous_t line 208
  16. theorem OAI.SKFluctuations.Cavity.cutLowJet_zero line 216
  17. theorem OAI.SKFluctuations.Cavity.cutLowJet_hasDerivAt_l line 233
  18. theorem OAI.SKFluctuations.Cavity.cutLowJet_hasDerivAt_t line 265
  19. theorem OAI.SKFluctuations.Cavity.cutDisorderExpect_third_remainder line 298
  20. theorem OAI.SKFluctuations.Hierarchy.ClockTree.disorderExpect_one line 331
  21. theorem OAI.SKFluctuations.Cavity.cutFullVariance_scalar_endpoint line 342
  22. theorem OAI.SKFluctuations.Cavity.cutDisorderExpect_scalar_product line 351
  23. theorem OAI.SKFluctuations.Cavity.cutDisorderExpect_rest_endpoint line 374
  24. theorem OAI.SKFluctuations.Cavity.cutDisorderExpect_site_endpoint line 387
  25. theorem OAI.SKFluctuations.Cavity.cutDisorderExpect_centered_endpoint line 400
  26. def OAI.SKFluctuations.Cavity.productJet3 line 425
  27. theorem OAI.SKFluctuations.Cavity.productJet3_hasDerivAt line 432
  28. theorem OAI.SKFluctuations.Cavity.productJet3_hasDerivAt_right line 447
  29. theorem OAI.SKFluctuations.Cavity.productJet3_continuous line 458
  30. theorem OAI.SKFluctuations.Cavity.derivative_zero_of_zero line 463
  31. theorem OAI.SKFluctuations.Cavity.thirdJet_zero_of_zero line 474
  32. def OAI.SKFluctuations.Cavity.cutCenteredJet line 503
  33. def OAI.SKFluctuations.Cavity.cutCenteredMixedJet line 511
  34. theorem OAI.SKFluctuations.Cavity.cutCenteredJet_continuous_l line 518
  35. theorem OAI.SKFluctuations.Cavity.cutCenteredJet_continuous_t line 525
  36. theorem OAI.SKFluctuations.Cavity.cutCenteredMixedJet_continuous_t line 531
  37. theorem OAI.SKFluctuations.Cavity.cutCenteredJet_hasDerivAt_l line 543
  38. theorem OAI.SKFluctuations.Cavity.cutCenteredJet_hasDerivAt_t line 552
  39. theorem OAI.SKFluctuations.Cavity.cutCenteredJet_zero_endpoint line 560
  40. theorem OAI.SKFluctuations.Cavity.cutCenteredJet_third_mixed_remainder line 573
  41. theorem OAI.SKFluctuations.Cavity.second_jet_remainder line 607
  42. theorem OAI.SKFluctuations.Cavity.first_jet_remainder line 628
  43. def OAI.SKFluctuations.Hierarchy.ClockPolynomial.finiteIterInsert line 644