OAI/Analysis/DiamondDistortion/DirectEnergy.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DiamondDistortion.DirectLayers.signed line 20
2. lemma OAI.DiamondDistortion.DirectLayers.signed_average line 21
3. lemma OAI.DiamondDistortion.DirectLayers.signed_error line 24
4. lemma OAI.DiamondDistortion.DirectLayers.signed_slope line 33
5. lemma OAI.DiamondDistortion.DirectLayers.deviation_bound line 38
6. lemma OAI.DiamondDistortion.DirectLayers.Regular.signed_supported line 48
7. lemma OAI.DiamondDistortion.DirectLayers.Regular.signed_layer line 52
8. lemma OAI.DiamondDistortion.DirectLayers.Regular.projected_layer_lower line 61
9. lemma OAI.DiamondDistortion.DirectLayers.Regular.supported_selection line 72
10. lemma OAI.DiamondDistortion.DirectLayers.approximate_bound line 134
11. theorem OAI.DiamondDistortion.DirectLayers.predictable_graph line 146
12. theorem OAI.DiamondDistortion.DirectLayers.variation_graph line 167
13. lemma OAI.DiamondDistortion.DirectLayers.gap_telescope line 200

    Source documentation

    The fresh-gap inequality telescopes for every supported predictable dyadic process, even when each increment contains a nonzero old-head part.

    lemma gap_telescope (hin : GapInput A.projection) {k : ℕ} (T : Protocol X I k)
        (hM : T.Martingale) (hN : T.Nested) (hAn : T.Anchored) (hS : T.Supported A.projection) :
        T.freshSum A.projection ≤ 400*(T.terminalEnergy-T.initialEnergy) := by
    …

    Mentions: OAI.DiamondDistortion.DirectLayers.GapInput

14. theorem OAI.DiamondDistortion.DirectLayers.gap_graph line 245
15. lemma OAI.DiamondDistortion.DirectLayers.norm_right_signed line 275
16. lemma OAI.DiamondDistortion.DirectLayers.signed_tail line 284
17. lemma OAI.DiamondDistortion.DirectLayers.Regular.true_selection line 296

    Source documentation

    Exact slopes, with a single common finite ancestral head on each level. Choosing the parent head slightly finer also ensures both child outcomes carry a fresh layer; this is valid for both adaptive and leakage inputs.

    lemma true_selection (k : ℕ) (f : Vertex k → X) {s L η r q : ℝ}
        (hl : ∀ u v,s*distance k u v ≤ ‖f u-f v‖)
        (hu : ∀ u v,‖f u-f v‖ ≤ L*distance k u v)
        (hη : 0 < η) (hr : r < s) (hq : 0 ≤ q) (hqr : q ≤ r-2*η) :
        ∃ (T : Protocol X I k) (e : History k → Edge k),
          T.Martingale ∧ T.Nested ∧ T.Anchored ∧ T.CommonHeads ∧
          (∀ u,T.last u=slope f (e u)) ∧
          (∀ u,‖T.last u-A.projection (T.lastHead u) (T.last u)‖ < η) ∧
          (k:ℝ)*q^2 ≤ T.freshSum A.projection ∧ T.leakageSum A.projection ≤ (k:ℝ)*η^2 := by
    …

18. lemma OAI.DiamondDistortion.DirectLayers.sign_constant_nonneg line 366
19. lemma OAI.DiamondDistortion.DirectLayers.dyadic_budget line 375
20. theorem OAI.DiamondDistortion.DirectLayers.adaptive_graph line 393
21. def OAI.DiamondDistortion.DirectLayers.leakageTolerance line 419
22. lemma OAI.DiamondDistortion.DirectLayers.leakage_tolerance_properties line 421
23. theorem OAI.DiamondDistortion.DirectLayers.leakage_graph line 433