OAI/Probability/CriticalZ3/Resampling.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteResampling.lower line 18
2. def OAI.FiniteResampling.upper line 19
3. theorem OAI.FiniteResampling.lower_le line 21
4. theorem OAI.FiniteResampling.le_upper line 23
5. theorem OAI.FiniteResampling.le_lower line 25
6. theorem OAI.FiniteResampling.upper_le line 27
7. theorem OAI.FiniteResampling.lower_le_upper line 29
8. structure OAI.FiniteResampling.Transition line 33
9. def OAI.FiniteResampling.Transition.act line 40
10. theorem OAI.FiniteResampling.Transition.act_const line 43
11. theorem OAI.FiniteResampling.Transition.act_mono line 47
12. theorem OAI.FiniteResampling.Transition.lower_le_act line 51
13. theorem OAI.FiniteResampling.Transition.act_le_upper line 55
14. theorem OAI.FiniteResampling.Transition.lower_le_lower_act line 59
15. theorem OAI.FiniteResampling.Transition.upper_act_le_upper line 62
16. theorem OAI.FiniteResampling.Transition.common_atom_bounds line 66

    Source documentation

    Subtracting the same atom from each row exposes a nonnegative remainder.

    theorem common_atom_bounds (z : I) (a : ℝ) (ha : ∀ i, a ≤ K.weight i z)
        (f : I → ℝ) (i : I) :
        a * f z + (1-a) * lower f ≤ K.act f i ∧
          K.act f i ≤ a * f z + (1-a) * upper f := by
    …

    Mentions: OAI.FiniteResampling.lower, OAI.FiniteResampling.upper

17. theorem OAI.FiniteResampling.Transition.oscillation_contract line 90
18. theorem OAI.FiniteResampling.Transition.iterates_tendsto_constant line 99

    Source documentation

    All finite transition iterates converge to a constant when every row shares one positive atom. Zero-probability states are permitted and not discarded.

    theorem iterates_tendsto_constant (z : I) (a : ℝ) (ha0 : 0 < a) (ha1 : a ≤ 1)
        (ha : ∀ i, a ≤ K.weight i z) (f : I → ℝ) :
        ∃ c : ℝ, lower f ≤ c ∧ c ≤ upper f ∧
          ∀ i, Tendsto (fun n : ℕ => ((K.act)^[n] f) i) atTop (nhds c) := by
    …

    Mentions: OAI.FiniteResampling.lower, OAI.FiniteResampling.upper