OAI/MathematicalPhysics/Boltzmann/Compactness/ContinuationAdmissibility.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Pasting a local solution to a global admissible continuation

  1. def OAI.BoltzmannNonuniqueness.continuedEvolution line 18
  2. theorem OAI.BoltzmannNonuniqueness.continuedEvolution_of_le line 21
  3. theorem OAI.BoltzmannNonuniqueness.continuedEvolution_of_gt line 24
  4. theorem OAI.BoltzmannNonuniqueness.AdmissibleLocal.continued_initial line 31
  5. theorem OAI.BoltzmannNonuniqueness.AdmissibleLocal.continued_finite_each_time line 36
  6. theorem OAI.BoltzmannNonuniqueness.AdmissibleLocal.continued_momentum line 46
  7. theorem OAI.BoltzmannNonuniqueness.AdmissibleLocal.continued_energy line 57
  8. theorem OAI.BoltzmannNonuniqueness.AdmissibleLocal.continued_uniform_moment line 67
  9. theorem OAI.BoltzmannNonuniqueness.lintegral_Icc_split line 100
  10. theorem OAI.BoltzmannNonuniqueness.lintegral_translate_interval line 108
  11. theorem OAI.BoltzmannNonuniqueness.AdmissibleLocal.continued_dissipation_before line 123
  12. theorem OAI.BoltzmannNonuniqueness.AdmissibleLocal.continued_dissipation_after line 130
  13. theorem OAI.BoltzmannNonuniqueness.AdmissibleLocal.continued_entropy line 147
  14. theorem OAI.BoltzmannNonuniqueness.continued_integrableOn line 184
  15. theorem OAI.BoltzmannNonuniqueness.continued_property_ae line 206
  16. theorem OAI.BoltzmannNonuniqueness.LocalMildSolution.divide_relativeDensity_integrable line 225
  17. theorem OAI.BoltzmannNonuniqueness.AdmissibleLocal.continued_collision_fibers line 251
  18. theorem OAI.BoltzmannNonuniqueness.AdmissibleLocal.continued_gain_integrable line 269
  19. theorem OAI.BoltzmannNonuniqueness.AdmissibleLocal.continued_loss_integrable line 278
  20. theorem OAI.BoltzmannNonuniqueness.continued_renormalizedIntegrand line 304
  21. theorem OAI.BoltzmannNonuniqueness.AdmissibleLocal.continued_renormalized_integrable line 318
  22. theorem OAI.BoltzmannNonuniqueness.AdmissibleLocal.continued_renormalized_equation line 333
  23. theorem OAI.BoltzmannNonuniqueness.continued_massIntegrand line 372
  24. theorem OAI.BoltzmannNonuniqueness.AdmissibleLocal.continued_mass_integrable line 386
  25. theorem OAI.BoltzmannNonuniqueness.AdmissibleLocal.continued_mass_equation line 402
  26. theorem OAI.BoltzmannNonuniqueness.AdmissibleLocal.continued_measurable line 441
  27. theorem OAI.BoltzmannNonuniqueness.AdmissibleLocal.continued_weak_continuity line 493
  28. theorem OAI.BoltzmannNonuniqueness.AdmissibleLocal.continued_strongEarly line 540
  29. theorem OAI.BoltzmannNonuniqueness.AdmissibleLocal.continued_admissible line 572
  30. theorem OAI.BoltzmannNonuniqueness.AdmissibleLocal.exists_global_extension line 593

    Source documentation

    A periodic global continuation retains the local solution pointwise through its endpoint, preserving strong early regularity and any separation.

    theorem exists_global_extension (S : AdmissibleLocal T f₀ F)
    (hperiodic : PeriodicExistenceInput) :
    ∃ G : Evolution, AdmissibleGlobal f₀ G ∧ StrongEarly T G ∧
      ∀ t ∈ Icc 0 T, G t = F t := by
…

    Mentions: OAI.BoltzmannNonuniqueness.AdmissibleLocal, OAI.BoltzmannNonuniqueness.PeriodicExistenceInput, OAI.BoltzmannNonuniqueness.Evolution, OAI.BoltzmannNonuniqueness.AdmissibleGlobal, OAI.BoltzmannNonuniqueness.StrongEarly