OAI/Probability/GammaPassage/SurvivalRank.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GammaFPP.gammaSurvival_nonneg line 17
2. lemma OAI.GammaFPP.gammaSurvival_measurable line 20
3. lemma OAI.GammaFPP.gammaSurvival_lt_one line 24
4. lemma OAI.GammaFPP.gammaSurvival_lt_iff line 31
5. lemma OAI.GammaFPP.gammaSurvival_rank_zero line 53

   Source documentation

   The exceptional zero-weight endpoint is deliberately outside ranks 0,...,m-1.

   lemma gammaSurvival_rank_zero (hs : 0 < shape) (hr : 0 < rate) (m : ℕ) :
       ⌊(m : ℝ) * gammaSurvival shape rate 0⌋₊ = m := by
   …

   Mentions: OAI.GammaFPP.gammaSurvival

6. lemma OAI.GammaFPP.GammaEnvironment.edge_ae_pos line 63

   Source documentation

   Native Gamma strict positivity transfers through the actual edge marginal.

   lemma edge_ae_pos (h : GammaEnvironment shape rate P τ) (e : PlanarFPP.Edge) :
       ∀ᵐ ω ∂P, 0 < τ e ω := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.PlanarFPP.Edge

7. lemma OAI.GammaFPP.GammaEnvironment.edge_tail_real line 70
8. theorem OAI.GammaFPP.GammaEnvironment.survival_lt_real line 87

   Source documentation

   Strict uniform CDF on the closed parameter interval, proved from actual tails.

   theorem survival_lt_real (h : GammaEnvironment shape rate P τ)
       (hs : 0 < shape) (hr : 0 < rate) (e : PlanarFPP.Edge)
       (u : ℝ) (hu : 0 ≤ u) (hu1 : u ≤ 1) :
       P.real {ω | gammaSurvival shape rate (τ e ω) < u} = u := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.PlanarFPP.Edge, OAI.GammaFPP.gammaSurvival

9. theorem OAI.GammaFPP.GammaEnvironment.survival_bin_real line 110
10. theorem OAI.GammaFPP.GammaEnvironment.survival_rank_real line 131

    Source documentation

    Exact floor-rank law; validity does not require pointwise positive weights.

    theorem survival_rank_real (h : GammaEnvironment shape rate P τ)
        (hs : 0 < shape) (hr : 0 < rate) (e : PlanarFPP.Edge)
        (m i : ℕ) (hm : 0 < m) (hi : i < m) :
        P.real {ω | ⌊(m : ℝ) * gammaSurvival shape rate (τ e ω)⌋₊ = i} = 1/(m : ℝ) := by
    …

    Mentions: OAI.GammaFPP.GammaEnvironment, OAI.PlanarFPP.Edge, OAI.GammaFPP.gammaSurvival

11. theorem OAI.GammaFPP.GammaEnvironment.survival_ranks_ae_lt line 154

    Source documentation

    Every original physical edge has an admissible rank simultaneously a.s. This uses strict positivity, not merely nonnegative support: zero has rank m.

    theorem survival_ranks_ae_lt (h : GammaEnvironment shape rate P τ)
        (hs : 0 < shape) (hr : 0 < rate) (m : ℕ) (hm : 0 < m) :
        ∀ᵐ ω ∂P, ∀ e, ⌊(m : ℝ) * gammaSurvival shape rate (τ e ω)⌋₊ < m := by
    …

    Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.gammaSurvival

12. theorem OAI.GammaFPP.GammaEnvironment.survival_ranks_joint_real line 166

    Source documentation

    Finite joint law from actual iIndepFun, including the empty edge set.

    theorem survival_ranks_joint_real (h : GammaEnvironment shape rate P τ)
        (hs : 0 < shape) (hr : 0 < rate) (S : Finset PlanarFPP.Edge)
        (m : ℕ) (hm : 0 < m) (i : PlanarFPP.Edge → ℕ) (hi : ∀ e ∈ S, i e < m) :
        P.real {ω | ∀ e ∈ S, ⌊(m : ℝ) * gammaSurvival shape rate (τ e ω)⌋₊ = i e} =
          (1/(m : ℝ))^S.card := by
    …

    Mentions: OAI.GammaFPP.GammaEnvironment, OAI.PlanarFPP.Edge, OAI.GammaFPP.gammaSurvival