OAI/MathematicalPhysics/Boltzmann/Branching/FiveGainConvergence.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Identification of the five actual thermal transitions with the analytic path

  1. def OAI.BoltzmannNonuniqueness.FiveGainMap.cycleFive line 20
  2. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.cycleFive_apply line 22
  3. def OAI.BoltzmannNonuniqueness.FiveGainMap.controlBlocks line 27
  4. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.controlBlocks_eq line 30
  5. def OAI.BoltzmannNonuniqueness.FiveGainMap.actualNext line 32
  6. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.actualNext_controlBlock line 36
  7. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.actualPath_eq_thermalPath line 47
  8. def OAI.BoltzmannNonuniqueness.FiveGainMap.stageValidity line 62
  9. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.stageValidity_le_one line 67
  10. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.coreDensity_eq_stage line 73
  11. def OAI.BoltzmannNonuniqueness.FiveGainMap.pathValidity line 85
  12. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.pathValidity_le_one line 88
  13. def OAI.BoltzmannNonuniqueness.FiveGainMap.actualDensity line 114
  14. def OAI.BoltzmannNonuniqueness.FiveGainMap.actualFiveIntegrand line 119
  15. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.actualFiveIntegrand_eq line 126
  16. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.actualFiveIntegrand_measurable line 185
  17. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.actual_five_core_integral line 205
  18. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.actualFiveIntegrand_zero_outside line 251
  19. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.actualFiveIntegrand_eq_indicator line 283
  20. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.actual_five_core_masked_tendsto line 315
  21. def OAI.BoltzmannNonuniqueness.FiveGainMap.actualPathWeight line 383
  22. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.actualPathWeight_le_one line 388
  23. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.weighted_five_integrand line 395
  24. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.actual_weighted_five_integral line 414
  25. def OAI.BoltzmannNonuniqueness.FiveGainMap.retainedPath line 489
  26. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.retainedPath_stageGood line 496
  27. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.retainedPath_density_support line 502
  28. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.retained_integrand_zero_outside line 521
  29. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.retained_integral_eq_box line 563
  30. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.actual_five_retained_tendsto line 582
  31. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.thermalPath_succ line 636
  32. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.thermalPath_succ_time line 644
  33. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.thermalPath_succ_velocity line 650
  34. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.actualPathWeight_factor_ne_zero line 658
  35. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.actualPathWeight_retained line 674

    Source documentation

    Any additional spatial masks are permitted: only their nonzero support matters.

    theorem actualPathWeight_retained (colors : Fin 5 → Bool) (α γ a T b Vmax : ℝ)
    (env : ThermalEnvironment) (weight : Fin 5 → Published.KineticPhase → ℝ≥0∞)
    (hweight : ∀ i z, weight i z ≠ 0 →
      z.1.1 ∈ Icc a T ∧ ‖z.2‖ ≤ Vmax ∧ b ≤ ‖transverse z.2‖)
    (hinit : ‖WithLp.toLp 2 env.2.2.2.2‖ ≤ Vmax ∧
      b ≤ ‖transverse (WithLp.toLp 2 env.2.2.2.2)‖)
    {q : ThermalControls} (hqt : q ∈ controlDomain)
    (hw : actualPathWeight colors α γ env weight q ≠ 0) :
    retainedPath colors α γ a T b Vmax env q := by
…

    Mentions: OAI.BoltzmannNonuniqueness.FiveGainMap.ThermalEnvironment, OAI.BoltzmannNonuniqueness.Published.KineticPhase, OAI.BoltzmannNonuniqueness.FiveGainMap.ThermalControls, OAI.BoltzmannNonuniqueness.FiveGainMap.controlDomain, OAI.BoltzmannNonuniqueness.FiveGainMap.actualPathWeight, OAI.BoltzmannNonuniqueness.FiveGainMap.retainedPath

  36. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.thermal_widths_eventually_small line 719
  37. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.actual_weighted_five_tendsto line 736