OAI/Probability/SKFluctuations/EvalStep.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Eval Step.

  1. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.Placement.eval_step line 20
  2. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.rowList_map_step line 28
  3. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.row_step line 46
  4. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.row_fork line 61
  5. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.fork_derivative_algebra line 85
  6. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.hasDerivAt_expect line 109
  7. def OAI.SKFluctuations.Hierarchy.ReplicaTree.normalizedAttach line 201
  8. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.normalizedAttach_mass line 204
  9. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.normalizedAttach_variation line 210
  10. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.normalizedAttach_leaves line 216
  11. def OAI.SKFluctuations.Hierarchy.ReplicaTree.sourceJet line 224
  12. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.sourceJet_single line 233
  13. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.sourceJet_smooth line 244
  14. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.sourceJet_hasDerivAt line 258
  15. def OAI.SKFluctuations.Hierarchy.ReplicaTree.attachmentCount line 286
  16. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.list_weight_abs_le line 290
  17. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.sourceJet_abs_le line 310
  18. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.sourceJet_two_abs_le line 340
  19. def OAI.SKFluctuations.Hierarchy.ReplicaTree.powerJet line 364
  20. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.powerJet_single line 372
  21. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.powerJet_smooth line 377
  22. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.weighted_expect_hasDerivAt line 392
  23. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.weighted_powerJet_hasDerivAt line 403
  24. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.powerJet_abs_le line 425
  25. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.powerJet_one_eq line 461
  26. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.powerJet_two_eq line 470
  27. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.expect_const line 502
  28. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.sourceJet_constant_one line 508
  29. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.sourceJet_constant_two line 519
  30. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.powerJet_constant_two line 528
  31. theorem OAI.SKFluctuations.Hierarchy.productGaussian_conv line 547
  32. theorem OAI.SKFluctuations.Hierarchy.linearGaussian_conv line 568
  33. theorem OAI.SKFluctuations.Hierarchy.integral_linearGaussian_add line 575
  34. theorem OAI.SKFluctuations.Hierarchy.exp_mul_shiftedContinuation line 592
  35. theorem OAI.SKFluctuations.Hierarchy.shiftedContinuation_linearGaussian_add line 599
  36. theorem OAI.SKFluctuations.Hierarchy.shiftedMean_linearGaussian_add line 619