SpineMoments.lean`

42 declarations, 0 contain sorry, 0 declared as axioms

instance OAI.FKCRT.Inventory.CoreLabel.(instance at line 12) line 12
instance OAI.FKCRT.Inventory.CoreLabel.(instance at line 13) line 13
lemma OAI.FKCRT.Inventory.CoreLabel.rootMass_pos line 15
lemma OAI.FKCRT.Inventory.CoreLabel.rootLaw_pos line 23
lemma OAI.FKCRT.Inventory.CoreLabel.root_fiber line 26
def OAI.FKCRT.Inventory.CoreLabel.markLaw line 33
Source documentation
Actual conditional root-core marks. The arbitrary probability at an unattainable arity is never used by the offspring distribution.
```
def markLaw (P : Parameters) (k : ℕ) : PMF CoreLabel :=
…
```
Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.CoreLabel
lemma OAI.FKCRT.Inventory.CoreLabel.markLaw_apply line 40
lemma OAI.FKCRT.Inventory.CoreLabel.offspring_zero_unattainable line 45
lemma OAI.FKCRT.Inventory.CoreLabel.offspring_pos_attainable line 51
theorem OAI.FKCRT.Inventory.CoreLabel.offspring_mul_mark line 59
Source documentation
Exact disintegration identity. The marks are independent draws from this kernel after the actual offspring array is fixed.
```
theorem offspring_mul_mark (P : Parameters) (k : ℕ) (c : CoreLabel) :
    (actualOffspring P).law k*markLaw P k c=if c.arity=k then rootLaw P c else 0 := by
…
```
Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.CoreLabel, OAI.FKCRT.Inventory.actualOffspring, OAI.FKCRT.Inventory.law, OAI.FKCRT.Inventory.CoreLabel.markLaw, OAI.FKCRT.Inventory.CoreLabel.rootLaw
theorem OAI.FKCRT.Inventory.CoreLabel.product_disintegration line 73
Source documentation
The finite product form used in the source's conditional marked law.
```
theorem product_disintegration (P : Parameters) {I : Type*} [Fintype I]
    (d : I→ℕ) (a : I → CoreLabel) :
    (∏ i,(actualOffspring P).law (d i))*(∏ i,markLaw P (d i) (a i))=
      if ∀ i,(a i).arity=d i then ∏ i,rootLaw P (a i) else 0 := by
…
```
Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.CoreLabel, OAI.FKCRT.Inventory.actualOffspring, OAI.FKCRT.Inventory.law, OAI.FKCRT.Inventory.CoreLabel.markLaw, OAI.FKCRT.Inventory.CoreLabel.arity, OAI.FKCRT.Inventory.CoreLabel.rootLaw
def OAI.FKCRT.TreeCoding.ladderType line 96
Source documentation
Offspring and right-child index seen at a genuine weak ascending record.
```
def ladderType (x : ℕ → ℕ) : ℕ × ℕ := (x (ladderIndex x),ladderOvershoot x)
```
Mentions: OAI.FKCRT.TreeCoding.ladderIndex, OAI.FKCRT.TreeCoding.ladderOvershoot
lemma OAI.FKCRT.TreeCoding.measurable_ladderType line 98
lemma OAI.FKCRT.TreeCoding.weakLadderHit_terminal_lt line 106
lemma OAI.FKCRT.TreeCoding.ladderType_of_hit line 116
lemma OAI.FKCRT.TreeCoding.measurableSet_ladderTypeHit line 120
lemma OAI.FKCRT.TreeCoding.ladderTypeHit_truncate line 125
lemma OAI.FKCRT.TreeCoding.ladderTypeHit_endpoint line 135
lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.ladderTypeHit_mass line 148
lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.ladderType_slice line 164
Source documentation
The exact spine pair has probability p(k) for each of its k possible child slots, and is independent of the infinite future.
```
lemma CriticalEvenOffspring.ladderType_slice (p : CriticalEvenOffspring)
    (k l : ℕ) (F : Set (ℕ → ℕ)) (hF : MeasurableSet F) :
    p.streamLaw ({x | ladderType x=(k,l)} ∩ ladderTail ⁻¹' F)=
      (if l<k then p.law k else 0)*p.streamLaw F := by
…
```
Mentions: OAI.FKCRT.TreeCoding.CriticalEvenOffspring, OAI.FKCRT.TreeCoding.ladderType, OAI.FKCRT.TreeCoding.ladderTail
def OAI.FKCRT.TreeCoding.CriticalEvenOffspring.spineLaw line 196
instance OAI.FKCRT.TreeCoding.(instance at line 199) line 199
lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.spineLaw_singleton line 202
lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.ladderType_rectangle line 209
lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.ladderType_indep_tail line 234
lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.ladderTypes_iid line 242
lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.spine_lintegral_fst line 256
lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.spine_integrable_fst line 276
lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.spine_integral_fst line 284
lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.spine_integrable_label line 294
lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.ladderType_hasLaw line 299
lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.ladderTypes_hasLaw line 303

lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.spine_label_deviation line 309

Source documentation

A genuinely sampled spine's bounded labels satisfy a two-sided Hoeffding bound. The label mean is the exact p(k)-per-child-slot spine expectation.

lemma CriticalEvenOffspring.spine_label_deviation (p : CriticalEvenOffspring)
    (b : ℕ×ℕ → ℝ) (a d : ℝ) (hb : ∀ z,b z∈Set.Icc a d)
    (h : ℕ) (r : ℝ) (hr : 0≤r) :
    p.streamLaw.real {x | r≤|∑ i ∈ Finset.range h,
      (b (ladderType (ladderTail^[i] x)) - ∫ z,b z ∂p.spineLaw)|} ≤
      2*Real.exp (-r^2/(2*h*((d-a)/2)^2)) := by
…

Mentions: OAI.FKCRT.TreeCoding.CriticalEvenOffspring, OAI.FKCRT.TreeCoding.ladderType, OAI.FKCRT.TreeCoding.ladderTail

lemma OAI.FKCRT.TreeCoding.prefixMaximum_eq_ladder line 355
lemma OAI.FKCRT.TreeCoding.renewalCount_before line 362
def OAI.FKCRT.TreeCoding.recordTypeAt line 374
Source documentation
A record's terminal offspring and its increase over the previous running maximum. This definition uses only the first t offspring, even for streams which have no later records.
```
def recordTypeAt (x : ℕ → ℕ) (t : ℕ) : ℕ×ℕ :=
…
```
lemma OAI.FKCRT.TreeCoding.recordTypeAt_ladder line 377
def OAI.FKCRT.TreeCoding.recordSpineSum line 393
lemma OAI.FKCRT.TreeCoding.recordSpineSum_eq line 396
lemma OAI.FKCRT.TreeCoding.integerSum_congr_prefix line 418
lemma OAI.FKCRT.TreeCoding.recordSpineSum_congr_prefix line 426
lemma OAI.FKCRT.TreeCoding.measurable_recordSpineSum line 440