UniformProtocols.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.BoundedTreePotentials.BlockCalculus.linear_block_trimming_242 line 17
Source documentation
Component trimming with constant 242. Empty heads and roots use the same literal coordinate projection as in the outer sum.
```
theorem linear_block_trimming_242 {n : ℕ} {D : Set Node} (hD : Initial D) (x y : TreeHilbert n)
    (hx : head D x=x) (hy : head D y=0) :
    (linearBlockCost n y)^2≤242*((linearBlockCost n (x+y))^2+
      (linearBlockCost n (x-y))^2-2*(linearBlockCost n x)^2) := by
…
```
Mentions: OAI.BoundedTreePotentials.TreeHilbert, OAI.BoundedTreePotentials.BlockCalculus.head, OAI.BoundedTreePotentials.linearBlockCost
theorem OAI.BoundedTreePotentials.CostHeads.linear_variation_energy_1008 line 32
Source documentation
The variation-energy estimate for terminal bound 2.
```
theorem linear_variation_energy_1008 {m : ℕ} {W : List Bool → LinearOuter}
    {P : List Bool → FiniteOuterHead} (hW : IsMartingale m W)
    (hP : PredictableLinearHeads m W P)
    (hC : ∀ w,w.length=m → ‖W w‖≤2) :
    (∑ i ∈ Finset.range m,average (i+1) (fun w => ‖linearLayer P W w‖^2))≤1008 := by
…
```
Mentions: OAI.BoundedTreePotentials.LinearOuter, OAI.BoundedTreePotentials.FiniteOuterHead, OAI.BoundedTreePotentials.CostHeads.PredictableLinearHeads, OAI.BoundedTreePotentials.CostHeads.linearLayer
def OAI.BoundedTreePotentials.Dyadic.conditionalMean line 49
Source documentation
Exact finite conditional expectation over k future fair bits. Histories are chronological from the right, as in the energy theorems.
```
def conditionalMean (W : List Bool → E) : ℕ → List Bool → E
  | 0,w => W w
  | k+1,w => (1/2 : ℝ) • (conditionalMean W k (false::w)+conditionalMean W k (true::w))
```
lemma OAI.BoundedTreePotentials.Dyadic.conditionalMean_succ_front line 53
lemma OAI.BoundedTreePotentials.Dyadic.martingale_conditionalMean line 63
Source documentation
The local dyadic martingale identity is exactly the assertion that each value is its finite conditional terminal average.
```
lemma martingale_conditionalMean {m : ℕ} {W : List Bool → E} (hW : IsMartingale m W)
    (k : ℕ) (w : List Bool) (hw : w.length+k≤ m) : conditionalMean W k w=W w := by
…
```
Mentions: OAI.BoundedTreePotentials.Dyadic.IsMartingale, OAI.BoundedTreePotentials.Dyadic.conditionalMean
lemma OAI.BoundedTreePotentials.Dyadic.isMartingale_iff_terminal_averages line 72
lemma OAI.BoundedTreePotentials.Dyadic.conditionalMean_eq_average line 87