OAI/MathematicalPhysics/Boltzmann/Branching/CausalConvolution.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The causal resolvent is a finite characteristic integral

  1. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.causal_convolution line 14
  2. theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.transportResolvent_eq line 40

    Source documentation

    Finite-time formula for exactly the Euclidean resolvent appearing in the published GLPS hypothesis. No time differentiability is used here.

    theorem transportResolvent_eq {r : Published.KineticPhase → ℝ}
    (hr : ∀ z, z.1.1 < 0 → r z = 0) (z : Published.KineticPhase) (ht : 0 ≤ z.1.1) :
    Published.transportResolvent r z =
      ∫ t in 0..z.1.1, Real.exp (-(z.1.1-t))*r ((t,z.1.2-(z.1.1-t) • z.2),z.2) := by
…

    Mentions: OAI.BoltzmannNonuniqueness.Published.KineticPhase, OAI.BoltzmannNonuniqueness.Published.transportResolvent