MarkedSpines.lean`

44 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.FKCRT.TreeCoding.PlaneTree.Profile.walkSum line 11
lemma OAI.FKCRT.TreeCoding.codeSpineSum_one line 26
lemma OAI.FKCRT.TreeCoding.code_profile_height line 35
lemma OAI.FKCRT.TreeCoding.code_profile_walk line 42
lemma OAI.FKCRT.TreeCoding.code_spine_mirror_identity line 51
Source documentation
Mirror exploration counts the left siblings on exactly the same ancestral path.
```
lemma code_spine_mirror_identity {N : ℕ} (d : Code N) {v : ℕ} (hv : v<N) :
    ∃ w<N,height (PlaneTree.mirrored d).val w=height d.val v ∧
      codeSpineSum (fun z => (z.1:ℝ)) d v=
        (walk d.val v:ℝ)+(walk (PlaneTree.mirrored d).val w:ℝ)+height d.val v := by
…
```
Mentions: OAI.FKCRT.TreeCoding.Code, OAI.FKCRT.TreeCoding.height, OAI.FKCRT.TreeCoding.PlaneTree.mirrored, OAI.FKCRT.TreeCoding.codeSpineSum, OAI.FKCRT.TreeCoding.walk

theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.uniform_degree_spine_limit line 81

Source documentation

Uniform path sum of offspring degrees needs only the original second moment. This is the deterministic two-sided exploration truncation bound, not a third-moment estimate.

theorem CriticalEvenOffspring.uniform_degree_spine_limit (p : CriticalEvenOffspring)
    {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P) {ε : ℝ} (hε : 0<ε) :
    Tendsto (fun n => (p.codeLaw n).real {d | ∃ v<2*n+1,
      ε*Real.sqrt ((2*n+1:ℕ):ℝ)< |codeSpineSum (fun z => (z.1:ℝ)) d v-
        (p.variance+1)*height d.val v|}) atTop (𝓝 0) := by
…

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

def OAI.FKCRT.TreeCoding.spineTail line 133
def OAI.FKCRT.TreeCoding.spineTrunc line 134
lemma OAI.FKCRT.TreeCoding.spineTail_nonneg line 136
lemma OAI.FKCRT.TreeCoding.spineTail_le line 139
lemma OAI.FKCRT.TreeCoding.spineTrunc_bound line 144
lemma OAI.FKCRT.TreeCoding.spineTrunc_tail_bound line 151
lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.spine_integrable_dom line 157
lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.spine_tail_integral_tendsto line 162
lemma OAI.FKCRT.TreeCoding.codeSpineSum_sub line 174
lemma OAI.FKCRT.TreeCoding.codeSpineSum_abs_le line 178
lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.spineTrunc_integral_error line 183
lemma OAI.FKCRT.TreeCoding.spineTail_eq line 195
lemma OAI.FKCRT.TreeCoding.spine_tail_control line 199

theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.uniform_integrable_spine_limit line 250

Source documentation

The full finite-variance all-vertex ancestral LLN for any deterministic slot label bounded in absolute value by the offspring count. No third moment or exponential upper tail.

theorem CriticalEvenOffspring.uniform_integrable_spine_limit (p : CriticalEvenOffspring)
    {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P)
    (b : ℕ×ℕ → ℝ) (hb : ∀ z,|b z| ≤ z.1) {ε : ℝ} (hε : 0 < ε) :
    Tendsto (fun n =>  (p.codeLaw n).real {d | ∃ v < 2*n+1,
      ε*Real.sqrt ((2*n+1:ℕ):ℝ) <  |codeSpineSum b d v-(∫ z,b z ∂p.spineLaw)*height d.val v|})
      atTop (𝓝 0) := by
…

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

abbrev OAI.FKCRT.TreeCoding.SpineRecords line 333
def OAI.FKCRT.TreeCoding.spineRecordType line 336
lemma OAI.FKCRT.TreeCoding.spineRecord_bounds line 339
def OAI.FKCRT.TreeCoding.spineRecordVertex line 344
lemma OAI.FKCRT.TreeCoding.spineRecordVertex_injective line 347
lemma OAI.FKCRT.TreeCoding.spineRecordType_fst line 357
lemma OAI.FKCRT.TreeCoding.spineRecords_card line 366
def OAI.FKCRT.TreeCoding.codeMarkLaw line 375
instance OAI.FKCRT.TreeCoding.codeMarkLaw_probability line 378
def OAI.FKCRT.TreeCoding.markedSpineSum line 382
lemma OAI.FKCRT.TreeCoding.markedSpineSum_deterministic line 387
lemma OAI.FKCRT.TreeCoding.measurable_markedSpineSum line 393
lemma OAI.FKCRT.TreeCoding.markedSpine_iIndep line 399
Source documentation
Conditional on the actual tree, distinct ancestors carry independent correctly sampled marks.
```
lemma markedSpine_iIndep {N : ℕ} (κ : ℕ → Measure A) [∀ k,IsProbabilityMeasure (κ k)]
    (d : Code N) {v : ℕ} (hv : v ≤ N) :
    iIndepFun (fun t : SpineRecords d v => fun a : Fin N → A => a (spineRecordVertex d hv t))
      (codeMarkLaw κ d) := by
…
```
Mentions: OAI.FKCRT.TreeCoding.Code, OAI.FKCRT.TreeCoding.SpineRecords, OAI.FKCRT.TreeCoding.spineRecordVertex, OAI.FKCRT.TreeCoding.codeMarkLaw
lemma OAI.FKCRT.TreeCoding.markedSpine_hasLaw line 406

lemma OAI.FKCRT.TreeCoding.markedSpine_deviation line 414

Source documentation

Bounded random marks concentrate round their conditional ancestral means.

lemma markedSpine_deviation {N : ℕ} (κ : ℕ → Measure A) [∀ k,IsProbabilityMeasure (κ k)]
    (b : (ℕ×ℕ) → A → ℝ) (hb : ∀ z,Measurable (b z)) {R : ℝ}
    (hbound : ∀ z a,|b z a| ≤ R) (d : Code N) {v : ℕ} (hv : v ≤ N)
    {r : ℝ} (hr : 0 ≤ r) :
    (codeMarkLaw κ d).real {a | r ≤ |markedSpineSum b d hv a-
      codeSpineSum (fun z => ∫ a,b z a ∂κ z.1) d v|} ≤
        2*Real.exp (-r^2/(2*(height d.val v)*R^2)) := by
…

Mentions: OAI.FKCRT.TreeCoding.Code, OAI.FKCRT.TreeCoding.codeMarkLaw, OAI.FKCRT.TreeCoding.markedSpineSum, OAI.FKCRT.TreeCoding.codeSpineSum, OAI.FKCRT.TreeCoding.height

def OAI.FKCRT.TreeCoding.codeMarkKernel line 472
instance OAI.FKCRT.TreeCoding.codeMarkKernel_markov line 475
def OAI.FKCRT.TreeCoding.CriticalEvenOffspring.markedCodeLaw line 478
instance OAI.FKCRT.TreeCoding.CriticalEvenOffspring.markedCodeLaw_probability line 481
lemma OAI.FKCRT.TreeCoding.compProd_real_bound line 485
lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.markedCodeLaw_fst line 498
lemma OAI.FKCRT.TreeCoding.measurable_marked_spine_joint line 506
lemma OAI.FKCRT.TreeCoding.markedSpineSum_zero_height line 512
lemma OAI.FKCRT.TreeCoding.marked_short_spine_bound line 519