OAI/Analysis/TreePotential/UniformAverages.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoundedTreePotentials.CostHeads.linear_head_tail_clipping_optimized line 14

   Source documentation

   The optimized square-root clipping bound.

   theorem linear_head_tail_clipping_optimized (A : FiniteOuterHead) (x y : LinearOuter)
       (hx : linearOuterHead A.nodes A.initial x=x)
       (hy : linearOuterHead A.nodes A.initial y=0) :
       Real.sqrt (‖x‖^2+‖y‖^2/16) ≤ max ‖x+y‖ ‖x-y‖ := by
   …

   Mentions: OAI.BoundedTreePotentials.FiniteOuterHead, OAI.BoundedTreePotentials.LinearOuter, OAI.BoundedTreePotentials.CostHeads.linearOuterHead

2. lemma OAI.BoundedTreePotentials.Dyadic.histories_length line 32
3. def OAI.BoundedTreePotentials.Dyadic.uniformVectorAverage line 39
4. lemma OAI.BoundedTreePotentials.Dyadic.uniformVectorAverage_succ line 42
5. theorem OAI.BoundedTreePotentials.Dyadic.conditionalMean_eq_uniform line 59

   Source documentation

   An explicit average with exactly 2^k equally weighted future branches.

   theorem conditionalMean_eq_uniform (W : List Bool → E) (k : ℕ) (w : List Bool) :
       conditionalMean W k w=
         ((2:ℝ)^k)⁻¹ • (((histories k).map (fun v => W (v++w))).sum) := by
   …

   Mentions: OAI.BoundedTreePotentials.Dyadic.conditionalMean, OAI.BoundedTreePotentials.Dyadic.histories

6. lemma OAI.BoundedTreePotentials.Dyadic.histories_nodup line 71