OAI/MathematicalPhysics/Boltzmann/Approximation/PositiveSourceFormula.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Positive gain comparison retaining the principal input action

  1. theorem OAI.BoltzmannNonuniqueness.chartGain_le_principal_add_remainders line 33
  2. def OAI.BoltzmannNonuniqueness.positiveDensityMeasure line 67
  3. theorem OAI.BoltzmannNonuniqueness.positiveDensityMeasure_finite line 70
  4. theorem OAI.BoltzmannNonuniqueness.positiveDensityMeasure_integral line 75
  5. def OAI.BoltzmannNonuniqueness.TransportPrimitive.positiveDifference line 96
  6. def OAI.BoltzmannNonuniqueness.TransportPrimitive.positiveDifferenceDamping line 98
  7. def OAI.BoltzmannNonuniqueness.TransportPrimitive.positiveDifferenceForcing line 101
  8. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.positiveDifference_derivative_identity line 104
  9. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.positiveDifference_damping_nonneg line 115
  10. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.positiveDifference_forcing_bound line 122
  11. theorem OAI.BoltzmannNonuniqueness.Compactness.positive_smooth_compact_approximation line 169
  12. theorem OAI.BoltzmannNonuniqueness.Compactness.finite_measure_eq_of_positive_smooth_tests line 203
  13. def OAI.BoltzmannNonuniqueness.positiveReflectionTest line 266
  14. theorem OAI.BoltzmannNonuniqueness.positiveReflectionTest_measurable line 270
  15. theorem OAI.BoltzmannNonuniqueness.sphereBallLift_radialReflection line 277
  16. theorem OAI.BoltzmannNonuniqueness.north_reflection_radial_integrand line 286
  17. theorem OAI.BoltzmannNonuniqueness.positive_hemisphere_reflection line 312
  18. abbrev OAI.BoltzmannNonuniqueness.Compactness.PositivePhaseTest line 354
  19. instance OAI.BoltzmannNonuniqueness.Compactness.(instance at line 358) line 358
  20. instance OAI.BoltzmannNonuniqueness.Compactness.(instance at line 361) line 361
  21. def OAI.BoltzmannNonuniqueness.Compactness.positivePhaseSeq line 364
  22. def OAI.BoltzmannNonuniqueness.Compactness.positivePhaseTest line 367
  23. theorem OAI.BoltzmannNonuniqueness.Compactness.positivePhaseTest_smooth line 370
  24. theorem OAI.BoltzmannNonuniqueness.Compactness.positivePhaseTest_compact line 374
  25. theorem OAI.BoltzmannNonuniqueness.Compactness.positivePhaseTest_nonneg line 378
  26. theorem OAI.BoltzmannNonuniqueness.Compactness.finite_phase_measure_eq_of_countable_tests line 382
  27. theorem OAI.BoltzmannNonuniqueness.PositiveMeasureHistories.comp_mono_measure line 440
  28. def OAI.BoltzmannNonuniqueness.PositiveMeasureHistories.historySum line 447
  29. theorem OAI.BoltzmannNonuniqueness.PositiveMeasureHistories.historySum_le line 451
  30. theorem OAI.BoltzmannNonuniqueness.PositiveMeasureHistories.historySum_succ line 457
  31. theorem OAI.BoltzmannNonuniqueness.PositiveMeasureHistories.historySum_eq_sum line 483
  32. theorem OAI.BoltzmannNonuniqueness.PositiveMeasureHistories.finite_histories_le line 489
  33. theorem OAI.BoltzmannNonuniqueness.PositiveMeasureHistories.endpoint_histories_le line 495
  34. def OAI.BoltzmannNonuniqueness.positiveSourceKernel line 519
  35. instance OAI.BoltzmannNonuniqueness.positiveSourceKernel_sFinite line 523
  36. theorem OAI.BoltzmannNonuniqueness.positiveSourceKernel_comp_density line 532
  37. theorem OAI.BoltzmannNonuniqueness.PositiveMeasureHistories.restrict_kernel_comp line 572
  38. theorem OAI.BoltzmannNonuniqueness.PositiveMeasureHistories.restricted_source_renewal line 582
  39. theorem OAI.BoltzmannNonuniqueness.PositiveMeasureHistories.finite_occupation_histories line 595
  40. theorem OAI.BoltzmannNonuniqueness.positiveDensityMeasure_restrict line 623
  41. theorem OAI.BoltzmannNonuniqueness.positiveDensityMeasure_map_symm line 632
  42. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.min_difference_le_positiveDifference line 664
  43. theorem OAI.BoltzmannNonuniqueness.Published.positive_integral_limit line 708
  44. theorem OAI.BoltzmannNonuniqueness.Cap.positive_fraction_loss_scaling line 745
  45. theorem OAI.BoltzmannNonuniqueness.positiveSourceKernel_lintegral line 790
  46. theorem OAI.BoltzmannNonuniqueness.positiveSourceKernel_one_lintegral line 803