OAI/Probability/SKFluctuations/ScalarProfileConcat.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Scalar Profile Concat.

  1. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfile_nonexpansive line 20
  2. theorem OAI.SKFluctuations.Hierarchy.HeatJet.multiple_grid_error line 27
  3. theorem OAI.SKFluctuations.Hierarchy.scalarProfile_multiple_concat line 42
  4. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfile_zero line 72
  5. theorem OAI.SKFluctuations.Hierarchy.scalarProfile_concat_stability line 80
  6. theorem OAI.SKFluctuations.Hierarchy.OrderedSteps.prefixOrdered line 110
  7. theorem OAI.SKFluctuations.Hierarchy.HeatJet.capped_diagonal_grid_error line 116
  8. theorem OAI.SKFluctuations.Hierarchy.HeatJet.capped_grid_tendstoUniformly line 126
  9. theorem OAI.SKFluctuations.Hierarchy.HeatJet.capped_test_parameter_bound line 140
  10. theorem OAI.SKFluctuations.Hierarchy.HeatJet.capped_test_parameter_cauchy line 153
  11. def OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfileTest line 166
  12. theorem OAI.SKFluctuations.Hierarchy.HeatJet.schedule_perturb_zero_A line 170
  13. theorem OAI.SKFluctuations.Hierarchy.HeatJet.capped_test_cauchy line 176
  14. theorem OAI.SKFluctuations.Hierarchy.HeatJet.capped_test_tendstoUniformly line 182
  15. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfile_terminal_deriv line 193
  16. def OAI.SKFluctuations.Hierarchy.HeatJet.withTest line 214
  17. theorem OAI.SKFluctuations.Hierarchy.prefixTest_subtract line 218
  18. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfileValue_congr_potential line 232
  19. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfileTest_congr line 239
  20. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfileTest_nonneg line 245
  21. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfileTest_abs_le line 256
  22. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfileTest_sub line 267
  23. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfileTest_affine line 283
  24. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfileTest_stability line 298
  25. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfile_perturb_zero line 325
  26. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfileTest_perturb_zero line 333
  27. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfile_terminal_deriv_zero line 342
  28. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfile_terminal_taylor line 350
  29. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfile_response_error line 370
  30. def OAI.SKFluctuations.Hierarchy.HeatJet.OrderedHessian line 399
  31. theorem OAI.SKFluctuations.Hierarchy.HeatJet.OrderedHessian.evolve line 402
  32. theorem OAI.SKFluctuations.Hierarchy.HeatJet.schedule_ordered_hessian line 423
  33. theorem OAI.SKFluctuations.Hierarchy.HeatJet.OrderedHessian.time_stability line 440
  34. theorem OAI.SKFluctuations.Hierarchy.orderedSteps_scaleTimes line 457
  35. theorem OAI.SKFluctuations.Hierarchy.HeatJet.schedule_ordered_time_stability line 466
  36. theorem OAI.SKFluctuations.Hierarchy.HeatJet.capped_scaled_mass_comparison_general line 501
  37. theorem OAI.SKFluctuations.Hierarchy.HeatJet.profile_affine_comparison_general line 519
  38. theorem OAI.SKFluctuations.Hierarchy.HeatJet.profile_window_stability_general line 558
  39. theorem OAI.SKFluctuations.Hierarchy.continuous_of_uniform_response line 577
  40. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfileValue_window_continuous line 598
  41. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfileTest_window_continuous line 622
  42. theorem OAI.SKFluctuations.Hierarchy.continuous_boundedProfile_test line 645