OAI/Analysis/AncientFlat/Weighted/WeightedDuhamel.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeightedDuhamel.SchwartzConvolution.scaled_weighted_majorant line 17
  2. def OAI.WeightedDuhamel.SchwartzTimeScale.euler line 79
  3. lemma OAI.WeightedDuhamel.SchwartzTimeScale.euler_apply line 85
  4. def OAI.WeightedDuhamel.SchwartzTimeScale.atTime line 88
  5. lemma OAI.WeightedDuhamel.SchwartzTimeScale.hasDerivAt_atTime line 91
  6. lemma OAI.WeightedDuhamel.SchwartzTimeScale.atTime_eq_scaled line 116
  7. lemma OAI.WeightedDuhamel.SourceFrozenCancellation.parameter_envelope line 134
  8. lemma OAI.WeightedDuhamel.SourceFrozenCancellation.parameter_lipschitz_envelope line 146
  9. lemma OAI.WeightedDuhamel.SourceFrozenCancellation.integral_atTime_zero line 157
  10. lemma OAI.WeightedDuhamel.SourceFrozenCancellation.continuous_variable line 164
  11. lemma OAI.WeightedDuhamel.SourceFrozenCancellation.integrable_envelope_power line 171
  12. lemma OAI.WeightedDuhamel.SourceFrozenCancellation.norm_normalized_source_integral line 188
  13. def OAI.WeightedDuhamel.SchwartzDerivatives.iterated line 261
  14. lemma OAI.WeightedDuhamel.SchwartzDerivatives.iterated_coe line 267
  15. lemma OAI.WeightedDuhamel.SchwartzDerivatives.iterated_apply line 278
  16. lemma OAI.WeightedDuhamel.SchwartzDerivatives.integral_fderiv line 288
  17. lemma OAI.WeightedDuhamel.SchwartzDerivatives.integral_iterated line 295
  18. lemma OAI.WeightedDuhamel.ScaledSchwartzConvolution.scaled_decay line 324
  19. lemma OAI.WeightedDuhamel.ScaledSchwartzConvolution.shifted_majorant line 355
  20. def OAI.WeightedDuhamel.ScaledSchwartzConvolution.value line 379
  21. lemma OAI.WeightedDuhamel.ScaledSchwartzConvolution.integrable_integrand line 383
  22. lemma OAI.WeightedDuhamel.ScaledSchwartzConvolution.hasFDerivAt_value line 396
  23. lemma OAI.WeightedDuhamel.ScaledSchwartzConvolution.contDiff_value_nat line 426
  24. lemma OAI.WeightedDuhamel.ScaledSchwartzConvolution.contDiff_value line 437
  25. lemma OAI.WeightedDuhamel.ScaledSchwartzConvolution.fderiv_value line 441
  26. lemma OAI.WeightedDuhamel.ScaledSchwartzConvolution.fderiv_value_apply line 447
  27. lemma OAI.WeightedDuhamel.ScaledSchwartzConvolution.second_fderiv_value_apply line 456
  28. lemma OAI.WeightedDuhamel.ScaledSchwartzConvolution.laplacian_value line 481
  29. lemma OAI.WeightedDuhamel.ScaledSchwartzConvolution.bilaplacian_value line 501
  30. lemma OAI.WeightedDuhamel.ScaledSchwartzConvolution.iteratedFDeriv_value_smul line 515
  31. lemma OAI.WeightedDuhamel.ScaledSchwartzConvolution.iteratedFDeriv_value_smul_apply line 550
  32. lemma OAI.WeightedDuhamel.SourceFrozenScaling.normalized_integral line 564
  33. lemma OAI.WeightedDuhamel.SourceFrozenScaling.dimension_cancel line 585
  34. lemma OAI.WeightedDuhamel.SourceFrozenScaling.normalized_integral_order line 589
  35. def OAI.WeightedDuhamel.SourceFrozenRows.value line 604
  36. def OAI.WeightedDuhamel.SourceFrozenRows.row line 608
  37. lemma OAI.WeightedDuhamel.SourceFrozenRows.radius_bounds line 615
  38. lemma OAI.WeightedDuhamel.SourceFrozenRows.contDiff_value line 623
  39. lemma OAI.WeightedDuhamel.SourceFrozenRows.row_eq line 631
  40. lemma OAI.WeightedDuhamel.SourceFrozenRows.row_normalized line 641
  41. lemma OAI.WeightedDuhamel.SourceFrozenRows.exists_row_holder_bound line 653
  42. lemma OAI.WeightedDuhamel.SourceFrozenRows.exists_row_zero_bound line 686
  43. lemma OAI.WeightedDuhamel.SourceFrozenRows.continuous_row line 716
  44. lemma OAI.WeightedDuhamel.SourceFrozenRows.hasFDerivAt_row line 725
  45. lemma OAI.WeightedDuhamel.SourceFrozenRows.stronglyMeasurable_time_row line 739
  46. lemma OAI.WeightedDuhamel.SourceFrozenRows.radius_weight line 759
  47. lemma OAI.WeightedDuhamel.SourceFrozenRows.integrableOn_lag_rpow line 773
  48. lemma OAI.WeightedDuhamel.SourceFrozenRows.exists_integrable_row_bound line 779
  49. def OAI.WeightedDuhamel.SourceFrozenRows.integralRow line 831
  50. lemma OAI.WeightedDuhamel.SourceFrozenRows.integrableOn_row line 844
  51. lemma OAI.WeightedDuhamel.SourceFrozenRows.continuous_integralRow line 850
  52. lemma OAI.WeightedDuhamel.SourceFrozenRows.hasFDerivAt_integralRow line 864
  53. lemma OAI.WeightedDuhamel.SourceFrozenRows.contDiff_integralRow line 894
  54. def OAI.WeightedDuhamel.SourceFrozenRows.duhamel line 913
  55. lemma OAI.WeightedDuhamel.SourceFrozenRows.duhamel_eq_integralRow_zero line 926
  56. lemma OAI.WeightedDuhamel.SourceFrozenRows.contDiff_duhamel line 941
  57. lemma OAI.WeightedDuhamel.SourceFrozenRows.iteratedFDeriv_duhamel line 952
  58. lemma OAI.WeightedDuhamel.SourceFrozenRows.exists_norm_iteratedFDeriv_duhamel_bound line 968
  59. def OAI.WeightedDuhamel.BetaWeights.density line 980
  60. lemma OAI.WeightedDuhamel.BetaWeights.density_nonneg line 982
  61. lemma OAI.WeightedDuhamel.BetaWeights.intervalIntegrable_one line 985
  62. lemma OAI.WeightedDuhamel.BetaWeights.density_scaled line 1001
  63. lemma OAI.WeightedDuhamel.BetaWeights.intervalIntegrable line 1008
  64. lemma OAI.WeightedDuhamel.BetaWeights.integral_scale line 1020
  65. lemma OAI.WeightedDuhamel.SourceFrozenRows.stronglyMeasurable_time_row_of_stronglyMeasurable line 1045
  66. lemma OAI.WeightedDuhamel.SourceFrozenRows.exists_integrable_row_bound_weighted line 1067
  67. lemma OAI.WeightedDuhamel.WeightedSourceFrozenRows.integrableOn_row line 1152
  68. lemma OAI.WeightedDuhamel.WeightedSourceFrozenRows.continuous_integralRow line 1158
  69. lemma OAI.WeightedDuhamel.WeightedSourceFrozenRows.hasFDerivAt_integralRow line 1172
  70. lemma OAI.WeightedDuhamel.WeightedSourceFrozenRows.contDiff_integralRow line 1202
  71. lemma OAI.WeightedDuhamel.WeightedSourceFrozenRows.duhamel_eq_integralRow_zero line 1216
  72. lemma OAI.WeightedDuhamel.WeightedSourceFrozenRows.contDiff_duhamel line 1231
  73. lemma OAI.WeightedDuhamel.WeightedSourceFrozenRows.iteratedFDeriv_duhamel line 1242
  74. lemma OAI.WeightedDuhamel.WeightedSourceFrozenRows.exists_norm_iteratedFDeriv_duhamel_bound line 1258