JetEnvelopeTimeIntegral.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

The transported core is dominated by an admissible Gaussian sheet

def OAI.BoltzmannNonuniqueness.JetCoreSheet.amplitude line 23
theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.amplitude_nonneg line 26
theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.parameter_bound line 32
theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.measure_domination line 44
theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.normalized_gain_bound line 67
theorem OAI.BoltzmannNonuniqueness.JetCoreSheet.gain_bound line 85
theorem OAI.BoltzmannNonuniqueness.JetCutoffSupersolution.ae_supersolution line 119
theorem OAI.BoltzmannNonuniqueness.JetIntegralSupersolution.integral_from_right_trace line 161

theorem OAI.BoltzmannNonuniqueness.JetIntegralSupersolution.cutoff_integral_bound line 200

Source documentation

This is the integral supersolution used to dominate each positive Picard iterate. Integrability of the gain is the only trajectory hypothesis.

theorem cutoff_integral_bound {K α γ s d t : ℝ} (hK : 0 ≤ K) (hα : 0 ≤ α)
    (hγ : 0 ≤ γ) (hs : 0 < s) (hd : 0 < d) (ht : 0 < t) (htmax : t ≤ 1)
    (hε : JetSupersolution.epsilon K s d ≤ 1) (η b : ℝ) (label : Bool) (p : JetPrototype.Phase)
    (hgi : IntervalIntegrable (fun r => CollisionCutoff.gain b
      (fun v => JetSupersolution.U η K α γ s d r label ((JetBarrier.flight r p).1, v)) p.2) volume 0 t) :
    density η K α γ s d label p +
      (∫ r in 0..t, CollisionCutoff.gain b
        (fun v => JetSupersolution.U η K α γ s d r label ((JetBarrier.flight r p).1, v)) p.2) ≤
      JetSupersolution.along η K α γ s d label p t := by
…

Mentions: OAI.BoltzmannNonuniqueness.JetSupersolution.epsilon, OAI.BoltzmannNonuniqueness.JetPrototype.Phase, OAI.BoltzmannNonuniqueness.CollisionCutoff.gain, OAI.BoltzmannNonuniqueness.JetSupersolution.U, OAI.BoltzmannNonuniqueness.JetBarrier.flight, OAI.BoltzmannNonuniqueness.JetSupersolution.along

def OAI.BoltzmannNonuniqueness.JetPicardComparison.attenuation line 241
theorem OAI.BoltzmannNonuniqueness.JetPicardComparison.attenuation_nonneg line 244
theorem OAI.BoltzmannNonuniqueness.JetPicardComparison.attenuation_le_one line 247
def OAI.BoltzmannNonuniqueness.JetPicardComparison.alongStep line 255
def OAI.BoltzmannNonuniqueness.JetPicardComparison.step line 261
def OAI.BoltzmannNonuniqueness.JetPicardComparison.picard line 265
theorem OAI.BoltzmannNonuniqueness.JetPicardComparison.gain_nonneg line 270
theorem OAI.BoltzmannNonuniqueness.JetPicardComparison.alongStep_nonneg line 276
theorem OAI.BoltzmannNonuniqueness.JetPicardComparison.picard_nonneg line 285
theorem OAI.BoltzmannNonuniqueness.JetPicardComparison.cutoff_mono line 296
theorem OAI.BoltzmannNonuniqueness.JetPicardComparison.alongStep_le line 316

theorem OAI.BoltzmannNonuniqueness.JetPicardComparison.picard_le line 356

Source documentation

Every positive Picard iterate is controlled independently of the supplied nonnegative loss. The hypotheses describe only measurability and finite integrals of the actual iteration, not an assumed comparison principle.

theorem picard_le {K α γ s d T : ℝ} (hK : 0 ≤ K) (hα : 0 ≤ α) (hγ : 0 ≤ γ)
    (hs : 0 < s) (hd : 0 < d) (hT : T ≤ 1) (hε : JetSupersolution.epsilon K s d ≤ 1)
    (η b : ℝ) (a : Bool) (ν : ℕ → ℝ → JetPrototype.Phase → ℝ)
    (hν : ∀ n r, r ∈ Icc 0 T → ∀ p, 0 ≤ ν n r p)
    (hcm : ∀ n r, r ∈ Ioc 0 T → ∀ x : Space,
      Measurable (fun v => picard η K α γ s d b a ν n r (x, v)))
    (hci : ∀ n t, t ∈ Ioc 0 T → ∀ p : JetPrototype.Phase,
      IntervalIntegrable (fun r => attenuation (ν n) r t p * CollisionCutoff.gain b
        (fun v => picard η K α γ s d b a ν n r ((JetBarrier.flight r p).1, v)) p.2) volume 0 t)
    (hUi : ∀ t, t ∈ Ioc 0 T → ∀ p : JetPrototype.Phase,
      IntervalIntegrable (fun r => CollisionCutoff.gain b
        (fun v => JetSupersolution.U η K α γ s d r a ((JetBarrier.flight r p).1, v)) p.2) volume 0 t) :
…

Mentions: OAI.BoltzmannNonuniqueness.JetSupersolution.epsilon, OAI.BoltzmannNonuniqueness.JetPrototype.Phase, OAI.BoltzmannNonuniqueness.JetPicardComparison.picard, OAI.BoltzmannNonuniqueness.JetPicardComparison.attenuation, OAI.BoltzmannNonuniqueness.CollisionCutoff.gain, OAI.BoltzmannNonuniqueness.JetBarrier.flight, OAI.BoltzmannNonuniqueness.JetSupersolution.U

def OAI.BoltzmannNonuniqueness.JetEnvelopeTimeIntegral.positiveGain line 404
theorem OAI.BoltzmannNonuniqueness.JetEnvelopeTimeIntegral.positiveGain_eq line 408
theorem OAI.BoltzmannNonuniqueness.JetEnvelopeTimeIntegral.measurable_positiveGain line 416
theorem OAI.BoltzmannNonuniqueness.JetEnvelopeTimeIntegral.gain_integrable line 441

theorem OAI.BoltzmannNonuniqueness.JetEnvelopeTimeIntegral.picard_le line 463

Source documentation

The explicit supersolution integrability condition in the Picard comparison is discharged. Only regularity of the iterates themselves remains to be supplied by the local construction.

theorem picard_le {K α γ s d T : ℝ} (hK : 0 ≤ K) (hα : 0 ≤ α) (hγ : 0 ≤ γ)
    (hs : 0 < s) (hd : 0 < d) (hT : T ≤ 1) (hε : JetSupersolution.epsilon K s d ≤ 1)
    (η b : ℝ) (a : Bool) (ν : ℕ → ℝ → JetPrototype.Phase → ℝ)
    (hν : ∀ n r, r ∈ Icc 0 T → ∀ p, 0 ≤ ν n r p)
    (hcm : ∀ n r, r ∈ Ioc 0 T → ∀ x : Space,
      Measurable (fun v => JetPicardComparison.picard η K α γ s d b a ν n r (x, v)))
    (hci : ∀ n t, t ∈ Ioc 0 T → ∀ p : JetPrototype.Phase,
      IntervalIntegrable (fun r => JetPicardComparison.attenuation (ν n) r t p * CollisionCutoff.gain b
        (fun v => JetPicardComparison.picard η K α γ s d b a ν n r
          ((JetBarrier.flight r p).1, v)) p.2) volume 0 t) :
    ∀ n t, t ∈ Ioc 0 T → ∀ p,
      JetPicardComparison.picard η K α γ s d b a ν n t p ≤ JetSupersolution.U η K α γ s d t a p :=
…