OAI/MathematicalPhysics/Boltzmann/Approximation/CapCoefficientExtraction.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

The actual normalized source is bounded by the positive main action

  1. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.euclideanColdSource line 34
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.euclideanColdSource_measurable line 37
  3. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.normalizedHotSource_le_positive_at line 47
  4. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.normalizedHotSource_le_positive_slab line 122
  5. def OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.positiveSourceError line 183
  6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.positiveSourceError_tendsto_zero line 188
  7. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_euclideanColdSource_bound line 199
  8. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_normalizedHotSource_le_positive line 218
  9. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.normalizedHot_positive_mild line 262
  10. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_boundedHotRatio_positive_mild line 327
  11. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_boundedHotRatio_residual line 388
  12. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.positiveSourceError_ne_top line 451
  13. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.positiveResidualConstant_tendsto line 459
  14. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.attained_time_mul_radius line 487
  15. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.attained_time_mem line 491
  16. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_attained_normalizedHotSource_le_positive line 496
  17. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.two_smul_incomingGain line 560
  18. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.characteristicGain_eq_normal line 576
  19. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.euclideanHot_div_weight_eq_normalized line 613
  20. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.le_half_of_clamp_le_half line 620
  21. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.exists_central_cap_witness line 625
  22. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.normalizedHot_initial_positive_mild line 699
  23. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.exists_tight_cap_family_at line 754
  24. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.positiveMainKernel_fraction_bound line 806
  25. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.eventually_positive_fraction_mass line 815
  26. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.eventually_positive_fraction_bound line 856
  27. structure OAI.BoltzmannNonuniqueness.JetCopyDatum.CapLocalLimit line 936
  28. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.TightCapFamily.exists_limit line 946
  29. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.coefficient_not_tendsto_zero line 996
  30. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_boundedHotRatio_log_residual line 1049
  31. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.eventually_attained_boundedHotRatio_log_residual line 1101
  32. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.AttainedCapSequence.HotLimitExtraction.positive_coefficient_subsequence line 1186