HistoryWeightNormalization.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exact survival-factor conversion for finite branching histories

theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.history_survival_normalization line 14

Source documentation

The potential changes Markov survival at rate λ into the original loss survival at rate ν.

theorem history_survival_normalization (a b : ℝ) {rate loss : ℝ → ℝ}
    (hrate : IntervalIntegrable rate volume a b) (hloss : IntervalIntegrable loss volume a b) :
    Real.exp (∫ s in a..b, rate s-loss s)*Real.exp (-(∫ s in a..b, rate s)) =
      Real.exp (-(∫ s in a..b, loss s)) := by
…

Mentions: OAI.BoltzmannNonuniqueness.loss

theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.history_survival_split line 23

Source documentation

Splitting a survival interval at collision times multiplies the survival factors.

theorem history_survival_split {a b c : ℝ} {loss : ℝ → ℝ}
    (hab : IntervalIntegrable loss volume a b) (hbc : IntervalIntegrable loss volume b c) :
    Real.exp (-(∫ s in a..b, loss s))*Real.exp (-(∫ s in b..c, loss s)) =
      Real.exp (-(∫ s in a..c, loss s)) := by
…

Mentions: OAI.BoltzmannNonuniqueness.loss