OAI/Analysis/TreePotential/Leakage.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BoundedTreePotentials.BlockCalculus.inward_pair_identity_leak line 17
2. lemma OAI.BoundedTreePotentials.BlockCalculus.InwardPiece.linear_le_two line 35
3. lemma OAI.BoundedTreePotentials.BlockCalculus.InwardPiece.error_bound line 44
4. theorem OAI.BoundedTreePotentials.BlockCalculus.linear_paired_leak line 54
5. lemma OAI.BoundedTreePotentials.leakage_energy_scalar line 79
6. theorem OAI.BoundedTreePotentials.BlockCalculus.linear_leakage_step line 108

   Source documentation

   One-step energy with actual leakage, valid with no head support assumption.

   theorem linear_leakage_step {n : ℕ} {D : Set Node} (hD : Initial D)
       (x y : TreeHilbert n) :
       ((linearBlockCost n ((x+y)-head D (x+y)))^2+
         (linearBlockCost n ((x-y)-head D (x-y)))^2)/2 ≤
         50*(linearBlockCost n (x-head D x))^2+
         32*(((linearBlockCost n (x+y))^2+(linearBlockCost n (x-y))^2)/2-
           (linearBlockCost n (head D x))^2) := by
   …

   Mentions: OAI.BoundedTreePotentials.TreeHilbert, OAI.BoundedTreePotentials.linearBlockCost, OAI.BoundedTreePotentials.BlockCalculus.head

7. lemma OAI.BoundedTreePotentials.BlockCalculus.head_nested line 138
8. lemma OAI.BoundedTreePotentials.CostHeads.linearOuterHead_nested line 151
9. lemma OAI.BoundedTreePotentials.CostHeads.linearOuterHead_norm_mono line 159
10. theorem OAI.BoundedTreePotentials.CostHeads.linearOuter_leakage_step line 165
11. structure OAI.BoundedTreePotentials.CostHeads.AdaptiveLinearWindows line 184

    Source documentation

    Both window endpoints are chosen from the past history. Within a history A_t is contained in D_t, and D_t is contained in either next A_{t+1}. There is deliberately no support assertion.

    structure AdaptiveLinearWindows (m : ℕ) (A D : List Bool → FiniteOuterHead) : Prop where
    …

    Mentions: OAI.BoundedTreePotentials.FiniteOuterHead

12. def OAI.BoundedTreePotentials.CostHeads.adaptiveLinearLayer line 188
13. def OAI.BoundedTreePotentials.CostHeads.adaptiveLinearLeak line 193
14. def OAI.BoundedTreePotentials.CostHeads.adaptiveLinearState line 198
15. lemma OAI.BoundedTreePotentials.CostHeads.adaptiveLinearState_contract line 203
16. lemma OAI.BoundedTreePotentials.CostHeads.adaptiveLinearState_le_head line 209
17. lemma OAI.BoundedTreePotentials.CostHeads.linear_adaptive_step line 219
18. lemma OAI.BoundedTreePotentials.Dyadic.telescope_leak line 253
19. theorem OAI.BoundedTreePotentials.CostHeads.linear_adaptive_energy_fifty line 286

    Source documentation

    Adaptive-window energy with an explicit absolute constant. The leakage is the actual parent window contribution. No parent support condition is present.

    theorem linear_adaptive_energy_fifty {m : ℕ} {W : List Bool → LinearOuter}
        {A D : List Bool → FiniteOuterHead} (hW : IsMartingale m W)
        (hAD : AdaptiveLinearWindows m A D) :
        (∑ i ∈ Finset.range m, average (i+1) (fun w => ‖adaptiveLinearLayer A D W w‖^2)) ≤
          50*(average m (fun w => ‖W w‖^2)+
            ∑ i ∈ Finset.range m, average i (fun w => ‖adaptiveLinearLeak A D W w‖^2)) := by
    …

    Mentions: OAI.BoundedTreePotentials.LinearOuter, OAI.BoundedTreePotentials.FiniteOuterHead, OAI.BoundedTreePotentials.CostHeads.AdaptiveLinearWindows, OAI.BoundedTreePotentials.CostHeads.adaptiveLinearLayer, OAI.BoundedTreePotentials.CostHeads.adaptiveLinearLeak

20. theorem OAI.BoundedTreePotentials.CostHeads.linear_adaptive_energy line 307

    Source documentation

    The adaptive estimate is uniform in the horizon, martingale, and measurable nested windows.

    theorem linear_adaptive_energy : ∃ K : ℝ, 0 < K ∧
        ∀ (m : ℕ) (W : List Bool → LinearOuter) (A D : List Bool → FiniteOuterHead),
          IsMartingale m W → AdaptiveLinearWindows m A D →
          (∑ i ∈ Finset.range m, average (i+1) (fun w => ‖adaptiveLinearLayer A D W w‖^2)) ≤
          K*(average m (fun w => ‖W w‖^2)+
            ∑ i ∈ Finset.range m, average i (fun w => ‖adaptiveLinearLeak A D W w‖^2)) := by
    …

    Mentions: OAI.BoundedTreePotentials.LinearOuter, OAI.BoundedTreePotentials.FiniteOuterHead, OAI.BoundedTreePotentials.CostHeads.AdaptiveLinearWindows, OAI.BoundedTreePotentials.CostHeads.adaptiveLinearLayer, OAI.BoundedTreePotentials.CostHeads.adaptiveLinearLeak

21. theorem OAI.BoundedTreePotentials.CostHeads.linear_fixed_leakage_1024 line 317

    Source documentation

    Fixed finite heads without support assumptions: the stronger adaptive estimate implies the leakage constant 1024.

    theorem linear_fixed_leakage_1024 {m : ℕ} {W : List Bool → LinearOuter}
        (P : ℕ → FiniteOuterHead) (hW : IsMartingale m W)
        (hP : ∀ i < m, ∀ n, (P i).nodes n ⊆ (P (i+1)).nodes n) :
        (∑ i ∈ Finset.range m, average (i+1) (fun w =>
          ‖linearOuterHead (P (i+1)).nodes (P (i+1)).initial (W w)-
            linearOuterHead (P i).nodes (P i).initial (W w)‖^2)) ≤
        1024*(average m (fun w => ‖W w‖^2)+
          ∑ i ∈ Finset.range m, average i (fun w =>
            ‖linearOuterHead (P (i+1)).nodes (P (i+1)).initial (W w)-
              linearOuterHead (P i).nodes (P i).initial (W w)‖^2)) := by
    …

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