OAI/Probability/FKMaps/MarkedBounds.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FKCRT.TreeCoding.marked_exp_vanish line 10
2. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.marked_short_unconditional_bound line 24
3. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.uniform_mark_noise line 48

   Source documentation

   Random marks are negligible relative to their conditional path means, uniformly over vertices.

   lemma CriticalEvenOffspring.uniform_mark_noise (p : CriticalEvenOffspring)
       {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
       {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P)
       (κ : ℕ → Measure A) [∀ k,IsProbabilityMeasure (κ k)]
       (b : (ℕ×ℕ) → A → ℝ) (hb : ∀ z,Measurable (b z)) {R : ℝ} (hR : 0 < R)
       (hbound : ∀ z a,|b z a| ≤ R) {ε : ℝ} (hε : 0 < ε) :
       Tendsto (fun n => (p.markedCodeLaw κ n).real {x | ∃ v : Fin (2*n+2),
         ε*Real.sqrt ((2*n+1:ℕ):ℝ) < |markedSpineSum b x.1 (by omega : v.val ≤ 2*n+1) x.2-
           codeSpineSum (fun z => ∫ a,b z a ∂κ z.1) x.1 v.val|}) atTop (𝓝 0) := by
   …

   Mentions: OAI.FKCRT.TreeCoding.CriticalEvenOffspring, OAI.FKCRT.TreeCoding.markedSpineSum, OAI.FKCRT.TreeCoding.codeSpineSum

4. lemma OAI.FKCRT.TreeCoding.markMean_bound line 113
5. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.uniform_bounded_marked_spine line 121

   Source documentation

   The bounded marked theorem with the source's genuine spine mean.

   theorem CriticalEvenOffspring.uniform_bounded_marked_spine (p : CriticalEvenOffspring)
       {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
       {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P)
       (κ : ℕ → Measure A) [∀ k,IsProbabilityMeasure (κ k)]
       (b : (ℕ×ℕ) → A → ℝ) (hb : ∀ z,Measurable (b z)) {R : ℝ} (hR : 0 < R)
       (hbound : ∀ z a,|b z a| ≤ R) {ε : ℝ} (hε : 0 < ε) :
       Tendsto (fun n => (p.markedCodeLaw κ n).real {x | ∃ v : Fin (2*n+2),
         ε*Real.sqrt ((2*n+1:ℕ):ℝ) < |markedSpineSum b x.1 (by omega : v.val ≤ 2*n+1) x.2-
           (∫ z,∫ a,b z a ∂κ z.1 ∂p.spineLaw)*height x.1.val v.val|}) atTop (𝓝 0) := by
   …

   Mentions: OAI.FKCRT.TreeCoding.CriticalEvenOffspring, OAI.FKCRT.TreeCoding.markedSpineSum, OAI.FKCRT.TreeCoding.height

6. def OAI.FKCRT.TreeCoding.markedTrunc line 170
7. lemma OAI.FKCRT.TreeCoding.measurable_markedTrunc line 173
8. lemma OAI.FKCRT.TreeCoding.markedTrunc_bound line 180
9. lemma OAI.FKCRT.TreeCoding.markedTrunc_mean line 184
10. lemma OAI.FKCRT.TreeCoding.markedSpineSum_sub line 190
11. lemma OAI.FKCRT.TreeCoding.markedSpineSum_abs_dom line 197
12. lemma OAI.FKCRT.TreeCoding.marked_spine_tail_control line 204
13. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.uniform_integrable_marked_spine line 267

    Source documentation

    The source's full uniform marked ancestral theorem, under the actual conditional independent-mark law, with only the offspring second moment.

    theorem CriticalEvenOffspring.uniform_integrable_marked_spine (p : CriticalEvenOffspring)
        {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
        {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P)
        {A : Type*} [MeasurableSpace A] (κ : ℕ → Measure A) [∀ k,IsProbabilityMeasure (κ k)]
        (b : (ℕ×ℕ) → A → ℝ) (hbmeas : ∀ z,Measurable (b z)) (hb : ∀ z a,|b z a| ≤ z.1) {ε : ℝ} (hε : 0 < ε) :
        Tendsto (fun n => (p.markedCodeLaw κ n).real {x | ∃ v : Fin (2*n+1),
          ε*Real.sqrt ((2*n+1:ℕ):ℝ) < |markedSpineSum b x.1 v.isLt.le x.2-
            (∫ z,∫ a,b z a ∂κ z.1 ∂p.spineLaw)*height x.1.val v.val|})
          atTop (𝓝 0) := by
    …

    Mentions: OAI.FKCRT.TreeCoding.CriticalEvenOffspring, OAI.FKCRT.TreeCoding.markedSpineSum, OAI.FKCRT.TreeCoding.height