OAI/Analysis/TreePotential/Dyadic.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoundedTreePotentials.Dyadic.histories line 14
2. def OAI.BoundedTreePotentials.Dyadic.average line 18
3. lemma OAI.BoundedTreePotentials.Dyadic.mem_histories line 21
4. lemma OAI.BoundedTreePotentials.Dyadic.average_zero line 29
5. lemma OAI.BoundedTreePotentials.Dyadic.average_succ line 31
6. lemma OAI.BoundedTreePotentials.Dyadic.average_const line 45
7. lemma OAI.BoundedTreePotentials.Dyadic.average_mono line 50
8. lemma OAI.BoundedTreePotentials.Dyadic.average_congr line 55
9. lemma OAI.BoundedTreePotentials.Dyadic.average_add line 59
10. lemma OAI.BoundedTreePotentials.Dyadic.average_mul line 65
11. lemma OAI.BoundedTreePotentials.Dyadic.average_sub line 71
12. lemma OAI.BoundedTreePotentials.Dyadic.average_nonneg line 77
13. def OAI.BoundedTreePotentials.Dyadic.IsMartingale line 82

    Source documentation

    The one-step arithmetic martingale identity on fair dyadic histories.

    def IsMartingale {E : Type*} [AddCommGroup E] [Module ℝ E]
        (m : ℕ) (W : List Bool → E) : Prop :=
    …

14. lemma OAI.BoundedTreePotentials.Dyadic.endpoints line 86
15. lemma OAI.BoundedTreePotentials.Dyadic.telescope line 95

    Source documentation

    Telescoping a predictable fair-child estimate, with the exact uniform averages and finite horizon, rather than an assumed energy conclusion.

    lemma telescope {m : ℕ} {v e : List Bool → ℝ} (hv : ∀ w, 0 ≤ v w)
        (he : ∀ w, w.length < m → (e (false::w)+e (true::w))/2 ≤
          16*((v (false::w)+v (true::w))/2-v w)) :
        (∑ i ∈ Finset.range m, average (i+1) e) ≤ 16*average m v := by
    …

    Mentions: OAI.BoundedTreePotentials.Dyadic.average

16. structure OAI.BoundedTreePotentials.CostHeads.PredictableLinearHeads line 126

    Source documentation

    Exact predictable timing: P_i has the same value for the two children of a history of length i-1. The support and nesting clauses are retained.

    structure PredictableLinearHeads (m : ℕ) (W : List Bool → LinearOuter)
        (P : List Bool → FiniteOuterHead) : Prop where
    …

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

17. def OAI.BoundedTreePotentials.CostHeads.linearLayer line 133

    Source documentation

    Measurable-window restriction to P_i \ P_{i-1}.

    def linearLayer (P : List Bool → FiniteOuterHead) (W : List Bool → LinearOuter)
        (w : List Bool) : LinearOuter :=
    …

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

18. lemma OAI.BoundedTreePotentials.CostHeads.linear_predictable_step line 138
19. theorem OAI.BoundedTreePotentials.CostHeads.linear_predictable_energy_sixteen line 167

    Source documentation

    A stronger constant is proved first. No predictability or support premise is moved to the wrong side of the newly revealed sign.

    theorem linear_predictable_energy_sixteen {m : ℕ} {W : List Bool → LinearOuter}
        {P : List Bool → FiniteOuterHead} (hW : IsMartingale m W)
        (hP : PredictableLinearHeads m W P) :
        (∑ i ∈ Finset.range m, average (i+1) (fun w => ‖linearLayer P W w‖^2)) ≤
          16*average m (fun w => ‖W w‖^2) :=
    …

    Mentions: OAI.BoundedTreePotentials.LinearOuter, OAI.BoundedTreePotentials.FiniteOuterHead, OAI.BoundedTreePotentials.CostHeads.PredictableLinearHeads, OAI.BoundedTreePotentials.CostHeads.linearLayer

20. theorem OAI.BoundedTreePotentials.CostHeads.linear_predictable_energy_495 line 174
21. theorem OAI.BoundedTreePotentials.CostHeads.linear_variation_energy_252 line 188