OAI/Probability/SKFluctuations/ParametricTestLimit.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Parametric Test Limit.

  1. theorem OAI.SKFluctuations.Hierarchy.derivative_secant_error line 19
  2. theorem OAI.SKFluctuations.Hierarchy.uniformCauchySeqOn_parameter_derivative line 32
  3. theorem OAI.SKFluctuations.Hierarchy.lipschitz_derivative_remainder line 83
  4. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_limit_of_lipschitz_derivative line 104
  5. theorem OAI.SKFluctuations.Hierarchy.HeatJet.evolve_time_stability line 137
  6. def OAI.SKFluctuations.Hierarchy.HeatClock.scaleTime line 158
  7. def OAI.SKFluctuations.Hierarchy.scaleTimes line 161
  8. theorem OAI.SKFluctuations.Hierarchy.scaleTimes_nil line 164
  9. theorem OAI.SKFluctuations.Hierarchy.scaleTimes_cons line 165
  10. theorem OAI.SKFluctuations.Hierarchy.scaleTimes_append line 167
  11. theorem OAI.SKFluctuations.Hierarchy.HeatJet.schedule_scale_time_stability line 170
  12. def OAI.SKFluctuations.Hierarchy.PositiveMassProfile.affine line 199
  13. theorem OAI.SKFluctuations.Hierarchy.PositiveMassProfile.grid_affine line 204
  14. def OAI.SKFluctuations.Hierarchy.NonnegativeMassProfile.affine line 229
  15. theorem OAI.SKFluctuations.Hierarchy.NonnegativeMassProfile.cappedApprox_affine line 234
  16. def OAI.SKFluctuations.Hierarchy.CoupledHeatClock.scaleTime line 238
  17. theorem OAI.SKFluctuations.Hierarchy.coupled_scale_left line 241
  18. theorem OAI.SKFluctuations.Hierarchy.coupled_scale_right line 247
  19. theorem OAI.SKFluctuations.Hierarchy.coupled_scale_cost line 253
  20. theorem OAI.SKFluctuations.Hierarchy.dyadicLowerSum_mono line 264
  21. theorem OAI.SKFluctuations.Hierarchy.HeatJet.capped_scaled_mass_comparison line 270
  22. theorem OAI.SKFluctuations.Hierarchy.HeatJet.profile_affine_comparison line 286
  23. theorem OAI.SKFluctuations.Hierarchy.monotone_shift_integral_bound line 336
  24. theorem OAI.SKFluctuations.Hierarchy.monotone_affine_l1_bound line 355
  25. theorem OAI.SKFluctuations.Hierarchy.HeatJet.profile_window_stability line 396
  26. def OAI.SKFluctuations.Hierarchy.PositiveMassProfile.linearGrid line 415
  27. theorem OAI.SKFluctuations.Hierarchy.PositiveMassProfile.linearGrid_add line 419
  28. def OAI.SKFluctuations.Hierarchy.HeatClock.pieces line 430
  29. theorem OAI.SKFluctuations.Hierarchy.HeatJet.schedule_replicate line 433
  30. def OAI.SKFluctuations.Hierarchy.PositiveMassProfile.linearCoupled line 450
  31. theorem OAI.SKFluctuations.Hierarchy.PositiveMassProfile.linearCoupled_left line 455
  32. theorem OAI.SKFluctuations.Hierarchy.PositiveMassProfile.linearCoupled_right line 462
  33. theorem OAI.SKFluctuations.Hierarchy.PositiveMassProfile.linearCoupled_cost line 469
  34. theorem OAI.SKFluctuations.Hierarchy.HeatJet.linear_block_comparison line 488
  35. theorem OAI.SKFluctuations.Hierarchy.HeatJet.linear_refinement_comparison line 501
  36. theorem OAI.SKFluctuations.Hierarchy.PositiveMassProfile.grid_eq_linear line 545
  37. theorem OAI.SKFluctuations.Hierarchy.HeatJet.linear_grid_error line 559
  38. theorem OAI.SKFluctuations.Hierarchy.HeatJet.capped_linear_error line 605
  39. theorem OAI.SKFluctuations.Hierarchy.HeatJet.multiple_grid_tendsto line 624