OAI/MathematicalPhysics/Boltzmann/Approximation/DormantConstruction.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.exists_dormant_approximation_family line 23

   Source documentation

   A uniform interval and actual zero-seed solutions, retaining the quadratic hot estimate needed in the small-time separation argument.

   theorem exists_dormant_approximation_family (hcarleman : Published.GPV2009CarlemanInput)
       {s₀ η K α γ d₀ q : ℝ}
       (hs₀ : 0 < s₀) (hsmax : s₀ ≤ 1/8) (hη : 0 < η) (hηmax : η ≤ Real.log 2)
       (hK : 0 ≤ K) (hα : 0 < α) (hαmax : α ≤ 1/4) (hγ : 0 < γ)
       (hd₀ : 0 < d₀) (hd₀max : d₀ ≤ 1) (hwidth : d₀*(1/8:ℝ)^10 ≤ 1/64)
       (hsmall : JetComparisonCoefficient.coefficient K*d₀*s₀^9 ≤ 1)
       (hq₁ : 1 < q) (hq₂ : q < 2) :
       ∃ T : ℝ, 0 < T ∧ T ≤ 1/32 ∧
         ∃ F : ∀ N, BelowCap.Approximation s₀ η K α γ d₀ q T N,
           (∀ N, (F N).coefficient = 0) ∧
           ∀ N t, t ∈ Icc 0 T → PhaseEssSup.size (fun p => (F N).solution.value (t,p)-
             ∑' i, rebuilt s₀ η K α γ d₀ q (N+1) (damping q (N+1) (F N).amplitude)
   …

   Mentions: OAI.BoltzmannNonuniqueness.Published.GPV2009CarlemanInput, OAI.BoltzmannNonuniqueness.JetComparisonCoefficient.coefficient, OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.Approximation, OAI.BoltzmannNonuniqueness.PhaseEssSup.size, OAI.BoltzmannNonuniqueness.JetCopyDatum.rebuilt

2. structure OAI.BoltzmannNonuniqueness.JetCopyDatum.DormantFamily line 101
3. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.exists_dormant_family line 108
4. structure OAI.BoltzmannNonuniqueness.JetCopyDatum.DormantLimit line 149
5. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.DormantFamily.exists_limit line 159
6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.DormantFamily.hot_le line 202
7. def OAI.BoltzmannNonuniqueness.JetCopyDatum.dormantMajorant line 236
8. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.dormantMajorant_measurable line 240
9. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.DormantFamily.central_bound line 246
10. def OAI.BoltzmannNonuniqueness.JetCopyDatum.kineticDilation line 300
11. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.kineticDilation_quasiMeasurePreserving line 303
12. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.dormantMajorant_dilation line 331
13. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.dormantMajorant_dilation_tendsto line 343
14. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.DormantLimit.central_bound line 370
15. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.DormantLimit.scaled_central_bound line 431