OAI/Probability/SKFluctuations/WeightCongrAt.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Weight Congr At.

  1. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.weight_congr_at line 23
  2. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.finite_stability line 43
  3. def OAI.SKFluctuations.Hierarchy.HeatJet.gradientPair line 127
  4. def OAI.SKFluctuations.Hierarchy.HeatJet.potentialEnergy line 129
  5. theorem OAI.SKFluctuations.Hierarchy.HeatJet.smoothGradientPair line 132
  6. theorem OAI.SKFluctuations.Hierarchy.HeatJet.smoothPotentialEnergy line 134
  7. theorem OAI.SKFluctuations.Hierarchy.HeatJet.testRate_sub line 139
  8. theorem OAI.SKFluctuations.Hierarchy.HeatJet.potentialRate_sub line 148
  9. theorem OAI.SKFluctuations.Hierarchy.HeatJet.testedTrace_eq_rate line 157
  10. theorem OAI.SKFluctuations.Hierarchy.HeatJet.clockDerivative_eq_rate line 167
  11. theorem OAI.SKFluctuations.Hierarchy.HeatJet.mass_transfer_cancellation line 181
  12. def OAI.SKFluctuations.Hierarchy.HeatJet.massSplit line 208
  13. def OAI.SKFluctuations.Hierarchy.HeatJet.massSplitResponse line 213
  14. theorem OAI.SKFluctuations.Hierarchy.HeatJet.hasDerivAt_massSplit line 222
  15. theorem OAI.SKFluctuations.Hierarchy.HeatJet.continuous_massSplit line 247
  16. theorem OAI.SKFluctuations.Hierarchy.HeatJet.massSplit_zero line 255
  17. theorem OAI.SKFluctuations.Hierarchy.HeatJet.massSplit_terminal line 260
  18. theorem OAI.SKFluctuations.Hierarchy.HeatJet.clockPotentialDerivative_eq_rate line 274
  19. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_dynamic_clockContinuation line 293
  20. theorem OAI.SKFluctuations.Hierarchy.clockTest_abs_le line 333
  21. theorem OAI.SKFluctuations.Hierarchy.clockGradient_abs_le line 340
  22. theorem OAI.SKFluctuations.Hierarchy.HeatJet.gradientPair_abs_le line 363
  23. theorem OAI.SKFluctuations.Hierarchy.HeatJet.potentialEnergy_abs_le line 372
  24. theorem OAI.SKFluctuations.Hierarchy.HeatJet.mass_transfer_abs_le line 380
  25. theorem OAI.SKFluctuations.Hierarchy.dynamic_clockContinuation_continuous line 412
  26. def OAI.SKFluctuations.Hierarchy.HeatJet.potentialSplit line 425
  27. def OAI.SKFluctuations.Hierarchy.HeatJet.potentialSplitResponse line 429
  28. theorem OAI.SKFluctuations.Hierarchy.HeatJet.hasDerivAt_potentialSplit line 434
  29. theorem OAI.SKFluctuations.Hierarchy.HeatJet.continuous_potentialSplit line 455
  30. theorem OAI.SKFluctuations.Hierarchy.HeatJet.potentialSplit_zero line 460
  31. theorem OAI.SKFluctuations.Hierarchy.HeatJet.potentialSplit_terminal line 465
  32. theorem OAI.SKFluctuations.Hierarchy.HeatJet.potentialSplitResponse_abs_le line 473
  33. theorem OAI.SKFluctuations.Hierarchy.HeatJet.potential_mass_difference line 488
  34. theorem OAI.SKFluctuations.Hierarchy.HeatJet.massSplitResponse_abs_le line 510
  35. theorem OAI.SKFluctuations.Hierarchy.HeatJet.clock_mass_difference line 543
  36. theorem OAI.SKFluctuations.Hierarchy.replicaFeatureJet_G_abs_le line 570
  37. theorem OAI.SKFluctuations.Hierarchy.replicaFeatureJet_A₁_abs_le line 579
  38. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.massSplitResponse_abs_le line 595
  39. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.mass_difference line 610