OAI/MathematicalPhysics/Boltzmann/Approximation/CapWeightedNonlinearLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Identification of the actual cap-family weak pair limit

  1. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.TightCapFamily.exists_nonlinear_weak_limit line 20

    Source documentation

    The velocity-averaging step identifies the genuine nonlinear pair product.

    theorem TightCapFamily.exists_nonlinear_weak_limit
    (hcarleman : Published.GPV2009CarlemanInput) (hGLPS : Published.GLPS1988Proposition3)
    (hDP : Published.DunfordPettis1940Theorem321)
    {s₀ η K α γ d₀ q : ℝ} (F : TightCapFamily s₀ η K α γ d₀ q)
    (hq₁ : 1 < q) (hq₂ : q < 2) :
    ∃ (φ : ℕ → ℕ) (g : (ℝ × Position) × Velocity → ℝ), StrictMono φ ∧
      Published.WeakL1Converges ((AnnularEnvelope.timePositionVolume F.time).prod volume)
        (fun n => torusPhysical q (F.approximation (φ n)).solution.value) g ∧
      Published.WeakL1Converges ((AnnularEnvelope.timePositionVolume F.time).prod volume)
        (fun n => CollisionCompactness.pairProduct
          (torusPhysical q (F.approximation (φ n)).solution.value))
        (CollisionCompactness.pairProduct g) ∧
…

    Mentions: OAI.BoltzmannNonuniqueness.Published.GPV2009CarlemanInput, OAI.BoltzmannNonuniqueness.Published.GLPS1988Proposition3, OAI.BoltzmannNonuniqueness.Published.DunfordPettis1940Theorem321, OAI.BoltzmannNonuniqueness.JetCopyDatum.TightCapFamily, OAI.BoltzmannNonuniqueness.Position, OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.Published.WeakL1Converges, OAI.BoltzmannNonuniqueness.AnnularEnvelope.timePositionVolume, OAI.BoltzmannNonuniqueness.JetCopyDatum.torusPhysical, OAI.BoltzmannNonuniqueness.CollisionCompactness.pairProduct

  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.TightCapFamily.exists_weighted_nonlinear_weak_limit line 121