CoarseProbability.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

The actual finite coarse randomness

At each internal node, the child thresholds are independent uniform labels. Recursive subtrees are independent of these labels. This complete probability space also includes labels below pruned nodes.

instance OAI.EditApproximation.coarseDrawsFintype line 22
def OAI.EditApproximation.coarseCanonicalDraws line 29
instance OAI.EditApproximation.coarseDrawsInhabited line 33
instance OAI.EditApproximation.coarseDrawsMeasurableSingletonClass line 38
instance OAI.EditApproximation.coarseDrawMeasure_isProbabilityMeasure line 51
Source documentation
Literal recursive independent label law, with a deterministic leaf.
```
instance coarseDrawMeasure_isProbabilityMeasure (B D : ℕ) [NeZero B]
    [MeasurableSpace (Fin B)] [MeasurableSingletonClass (Fin B)] :
    IsProbabilityMeasure (coarseDrawMeasure B D) := by
…
```
Mentions: OAI.EditApproximation.coarseDrawMeasure
def OAI.EditApproximation.coarseInternalNodes line 66
Source documentation
Symbolic number of internal nodes in a complete coarse tree.
```
def coarseInternalNodes (B : ℕ) : ℕ → ℕ
  | 0 => 0
  | D + 1 => 1 + B * coarseInternalNodes B D
```
theorem OAI.EditApproximation.coarseInternalNodes_eq_sum line 70
def OAI.EditApproximation.coarseChildListStart line 80
Source documentation
Actual source starts of all children of a literal list traversal.
```
def coarseChildListStart {B D : ℕ} {α : Type u}
    (children : List (CoarseSourceTree B α D)) (start : ℕ) (i : Fin children.length) : ℕ :=
…
```
Mentions: OAI.EditApproximation.CoarseSourceTree

theorem OAI.EditApproximation.coarseChildrenCost_eq_sum line 85

Source documentation

The literal list recurrence equals its finite sum at the actual starts.

theorem coarseChildrenCost_eq_sum {B D : ℕ} {α : Type u}
    (k : ℕ) (value : CoarseSourceTree B α D → ℕ → Fin (2 * k + 1) → ℕ)
    (children : List (CoarseSourceTree B α D)) (start : ℕ) (shift : Fin (2 * k + 1)) :
    coarseChildrenCost k value children start shift =
      ∑ i : Fin children.length, univ.inf' univ_nonempty
        (fun next => value children[i.val] (coarseChildListStart children start i) next +
          2 * Nat.dist shift.val next.val) := by
…

Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.coarseChildrenCost, OAI.EditApproximation.coarseChildListStart

theorem OAI.EditApproximation.coarse_product_section_bound line 109

Source documentation

Integrating a uniform conditional failure bound over the ancestor labels does not add a union over the possible allowance values.

theorem coarse_product_section_bound {X Y : Type*}
    [MeasurableSpace X] [MeasurableSpace Y]
    (μ : Measure X) (ν : Measure Y) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
    (bad : Set (X × Y)) (hbad : MeasurableSet bad) (failure : ℝ) (hfailure : 0 ≤ failure)
    (hsection : ∀ x, ν.real {y | (x, y) ∈ bad} ≤ failure) :
    (μ.prod ν).real bad ≤ failure := by
…

theorem OAI.EditApproximation.coarse_child_projection_probability line 125

Source documentation

The recursive child coordinates have precisely their own subtree law.

theorem coarse_child_projection_probability (B D : ℕ) [NeZero B]
    [MeasurableSpace (Fin B)] [MeasurableSingletonClass (Fin B)]
    (i : Fin B) (bad : Set (CoarseThresholdDraws B D)) :
    (Measure.pi fun _ : Fin B => coarseDrawMeasure B D).real {below | below i ∈ bad} =
      (coarseDrawMeasure B D).real bad := by
…

Mentions: OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.coarseDrawMeasure

def OAI.EditApproximation.coarseDataListStart line 138
Source documentation
Source starts attached to the full child metadata list.
```
def coarseDataListStart {B D : ℕ} {α : Type u}
    (children : List (CoarseSourceTree B α D × Fin B × CoarseThresholdDraws B D))
    (start : ℕ) (i : Fin children.length) : ℕ :=
…
```
Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.CoarseThresholdDraws
theorem OAI.EditApproximation.coarseDescendantEvents_iff line 143
theorem OAI.EditApproximation.coarseTrueThresholdSum_eq_sum line 164
def OAI.EditApproximation.coarseNodeChildStart line 192
def OAI.EditApproximation.coarseNodeChildCost line 196
theorem OAI.EditApproximation.coarseChildrenCost_ofFn line 203
theorem OAI.EditApproximation.coarseDataListStart_ofFn line 214
theorem OAI.EditApproximation.coarseTrueThresholdSum_ofFn line 224
theorem OAI.EditApproximation.coarseChildThreshold_cast line 242
theorem OAI.EditApproximation.coarseTrueThresholdSum_sample line 251

theorem OAI.EditApproximation.coarse_finite_threshold_simultaneous line 269

Source documentation

A finite family of fixed child-cost lists shares the same independent threshold labels. A union bound needs no independence between the lists.

theorem coarse_finite_threshold_simultaneous {B : ℕ} [NeZero B]
    [MeasurableSpace (Fin B)] [MeasurableSingletonClass (Fin B)]
    {I : Type*} [Fintype I]
    (value : I → Fin B → ℝ) (scale allowance Q lam : ℝ)
    (hvalue : ∀ i j, 0 ≤ value i j) (hu : 0 < scale) (ha : 0 < allowance)
    (hQ : Q * scale = allowance) (hscale : scale ≤ allowance / 2)
    (hlam : 0 ≤ lam) (hlamone : lam ≤ 1)
    (bernstein : FiniteBernsteinInput (Measure.pi fun _ : Fin B =>
      (PMF.uniformOfFintype (Fin B)).toMeasure)) :
    (Measure.pi fun _ : Fin B => (PMF.uniformOfFintype (Fin B)).toMeasure).real
      {draws | ¬ ∀ i, |(∑ j, coarseThresholdSample scale (value i j) (draws j)) -
          ∑ j, value i j| ≤ lam * (∑ j, value i j) + allowance} ≤
…

Mentions: OAI.EditApproximation.FiniteBernsteinInput, OAI.EditApproximation.coarseThresholdSample

def OAI.EditApproximation.coarseNodeSamplingValue line 304

Source documentation

The two deterministic cost lists used at a node, simultaneously for all shifts. The Boolean coordinate selects the lower or upper list.

noncomputable def coarseNodeSamplingValue {B D : ℕ} {α : Type u}
    (k : ℕ) (lam : ℚ) (f : ℝ)
    (value : CoarseSourceTree B α D → ℕ → Fin (2 * k + 1) → ℕ)
    (children : Fin B → CoarseSourceTree B α D) (start : ℕ)
    (index : Fin (2 * k + 1) × Bool) (i : Fin B) : ℝ :=
…

Mentions: OAI.EditApproximation.CoarseSourceTree

def OAI.EditApproximation.CoarseNodeDeviationEvent line 313

theorem OAI.EditApproximation.coarseNodeDeviationEvent_probability line 325

Source documentation

One complete node event costs four scalar Bernstein tails per shift.

theorem coarseNodeDeviationEvent_probability {B D : ℕ} [NeZero B] {α : Type u}
    [MeasurableSpace (Fin B)] [MeasurableSingletonClass (Fin B)]
    (k : ℕ) (Q lam allowance : ℚ) (f : ℝ)
    (value : CoarseSourceTree B α D → ℕ → Fin (2 * k + 1) → ℕ)
    (children : Fin B → CoarseSourceTree B α D) (start : ℕ)
    (hQ : 2 ≤ Q) (hlam : 0 ≤ lam) (hlamone : lam < 1)
    (ha : 0 < allowance) (hf : 0 < f)
    (bernstein : FiniteBernsteinInput (Measure.pi fun _ : Fin B =>
      (PMF.uniformOfFintype (Fin B)).toMeasure)) :
    (Measure.pi fun _ : Fin B => (PMF.uniformOfFintype (Fin B)).toMeasure).real
      {draws | ¬ CoarseNodeDeviationEvent k Q lam allowance f value children start draws} ≤
      4 * (2 * k + 1 : ℕ) * Real.exp (-(lam : ℝ) * Q / 12) := by
…

Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.FiniteBernsteinInput, OAI.EditApproximation.CoarseNodeDeviationEvent

theorem OAI.EditApproximation.coarseNodeDeviationEvent_bounds line 360

Source documentation

The deviation event is expressed using only the root labels, yet it implies the literal true-cost inequalities for every subtree realization.

theorem coarseNodeDeviationEvent_bounds {B D : ℕ} [NeZero B] {α : Type u}
    (k : ℕ) (Q lam allowance : ℚ) (f : ℝ) (hQ : Q ≠ 0)
    (value : CoarseSourceTree B α D → ℕ → Fin (2 * k + 1) → ℕ)
    (children : Fin B → CoarseSourceTree B α D)
    (draws : Fin B → Fin B) (below : Fin B → CoarseThresholdDraws B D) (start : ℕ)
    (hevent : CoarseNodeDeviationEvent k Q lam allowance f value children start draws) :
    ∀ shift,
      (1 - (lam : ℝ)) *
          ((coarseChildrenCost k value (List.ofFn children) start shift : ℝ) /
            (f * (1 + (lam : ℝ)))) - allowance ≤
        coarseTrueThresholdSum k Q value allowance
          (fun cost => cost / (f * (1 + (lam : ℝ))))
…

Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.CoarseNodeDeviationEvent, OAI.EditApproximation.coarseChildrenCost, OAI.EditApproximation.coarseTrueThresholdSum

theorem OAI.EditApproximation.coarseAccuracyEvent_of_node line 401

Source documentation

Root and actual descendant events suffice for the complete-tree accuracy event; no approximate child value occurs in the root event.

theorem coarseAccuracyEvent_of_node {B D : ℕ} [NeZero B] {α : Type u} [DecidableEq α]
    (k : ℕ) (Q lam allowance : ℚ) (frame : List (Option α))
    (children : Fin B → CoarseSourceTree B α D)
    (draws : Fin B → Fin B) (below : Fin B → CoarseThresholdDraws B D)
    (start : ℕ) (hQ : Q ≠ 0)
    (hchild : ∀ i, CoarseAccuracyEvent k Q lam frame (children i) (below i)
      (lam * coarseChildThreshold B Q allowance (draws i)) (coarseNodeChildStart children start i))
    (hnode : CoarseNodeDeviationEvent k Q lam allowance (coarseStructuralFactor lam D)
      (fun child => coarseShiftCost k frame child) children start draws) :
    CoarseAccuracyEvent k Q lam frame (.branch children) (draws, below) allowance start := by
…

Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.CoarseAccuracyEvent, OAI.EditApproximation.coarseChildThreshold, OAI.EditApproximation.coarseNodeChildStart, OAI.EditApproximation.CoarseNodeDeviationEvent, OAI.EditApproximation.coarseStructuralFactor, OAI.EditApproximation.coarseShiftCost

theorem OAI.EditApproximation.coarseAccuracyEvent_failure line 424

Source documentation

Simultaneous accuracy for the literal finite recursive estimator. Every descendant is integrated conditional on its ancestor labels, with a bound uniform in its resulting positive allowance.

theorem coarseAccuracyEvent_failure {B D : ℕ} [NeZero B] {α : Type u} [DecidableEq α]
    [MeasurableSpace (Fin B)] [MeasurableSingletonClass (Fin B)]
    (k : ℕ) (Q lam : ℚ) (frame : List (Option α))
    (tree : CoarseSourceTree B α D) (allowance : ℚ) (start : ℕ)
    (hQ : 2 ≤ Q) (hlam : 0 < lam) (hlamone : lam < 1) (ha : 0 < allowance)
    (bernstein : FiniteBernsteinInput (Measure.pi fun _ : Fin B =>
      (PMF.uniformOfFintype (Fin B)).toMeasure)) :
    (coarseDrawMeasure B D).real
      {draws | ¬ CoarseAccuracyEvent k Q lam frame tree draws allowance start} ≤
      (coarseInternalNodes B D : ℝ) *
        (4 * (2 * k + 1 : ℕ) * Real.exp (-(lam : ℝ) * Q / 12)) := by
…

Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.FiniteBernsteinInput, OAI.EditApproximation.coarseDrawMeasure, OAI.EditApproximation.CoarseAccuracyEvent, OAI.EditApproximation.coarseInternalNodes