OAI/Analysis/TreePotential/SegmentCancellation.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BoundedTreePotentials.Segments.shortening_injective line 13
2. def OAI.BoundedTreePotentials.Segments.Atom.sees line 61
3. def OAI.BoundedTreePotentials.Segments.Atom.original line 63
4. def OAI.BoundedTreePotentials.Segments.Atom.exitCoeff line 66
5. lemma OAI.BoundedTreePotentials.Segments.Atom.original_spec line 69
6. lemma OAI.BoundedTreePotentials.Segments.Atom.original_eq line 74
7. lemma OAI.BoundedTreePotentials.Segments.Atom.exitCoeff_eq line 81
8. lemma OAI.BoundedTreePotentials.Segments.Atom.exitCoeff_ne_zero line 85
9. lemma OAI.BoundedTreePotentials.Segments.Atom.original_injective line 90
10. lemma OAI.BoundedTreePotentials.Segments.Atom.early_cancellation line 104

    Source documentation

    The shorter-start half of opposite-exit cancellation.

    lemma early_cancellation {C : Set Node} (hC : Initial C) {g : Node → ℝ}
        (hg : IsUnitTest g) (hsupp : ∀ v ∉ C, g v=0) (A B : Atom) (Q : Finset Node)
        (hQ : ∀ q ∈ Q, IsExit C q)
        (hop : ∀ q ∈ Q, A.exitCoeff g q*B.exitCoeff g q < 0)
        (hearly : ∀ q ∈ Q, Prefix (A.original q).start (B.original q).start ∧
          (A.original q).start ≠ (B.original q).start) :
        2*(∑ q ∈ Q, |A.exitCoeff g q*B.exitCoeff g q|) ≤
          1-(∑ S ∈ A.family, (S.eval g)^2) := by
    …

    Mentions: OAI.BoundedTreePotentials.Segments.Node, OAI.BoundedTreePotentials.Segments.Initial, OAI.BoundedTreePotentials.Segments.IsUnitTest, OAI.BoundedTreePotentials.Segments.Atom, OAI.BoundedTreePotentials.Segments.IsExit, OAI.BoundedTreePotentials.Segments.Prefix

11. lemma OAI.BoundedTreePotentials.Segments.Atom.opposite_starts line 146
12. theorem OAI.BoundedTreePotentials.Segments.Atom.cancellation line 168

    Source documentation

    Opposite coefficients at any finite set of actual exits consume exactly both unused squared-evaluation budgets, hence the two atom defects.

    theorem cancellation {C : Set Node} (hC : Initial C) {g : Node → ℝ}
        (hg : IsUnitTest g) (hsupp : ∀ v ∉ C, g v=0) (A B : Atom) (Q : Finset Node)
        (hQ : ∀ q ∈ Q, IsExit C q) :
        (∑ q ∈ Q, oppositeProduct (A.exitCoeff g q) (B.exitCoeff g q)) ≤
          (1-A.pairing g)+(1-B.pairing g) := by
    …

    Mentions: OAI.BoundedTreePotentials.Segments.Node, OAI.BoundedTreePotentials.Segments.Initial, OAI.BoundedTreePotentials.Segments.IsUnitTest, OAI.BoundedTreePotentials.Segments.Atom, OAI.BoundedTreePotentials.Segments.IsExit, OAI.BoundedTreePotentials.Segments.oppositeProduct

13. lemma OAI.BoundedTreePotentials.Segments.finitePairing_filter line 207
14. lemma OAI.BoundedTreePotentials.Segments.finitePairing_tail line 216
15. lemma OAI.BoundedTreePotentials.Segments.finitePairing_filter_finset line 225
16. lemma OAI.BoundedTreePotentials.Segments.finitePairing_tail_finset line 233
17. lemma OAI.BoundedTreePotentials.Segments.core_head_norm line 242
18. lemma OAI.BoundedTreePotentials.Segments.core_tail_norm line 254
19. lemma OAI.BoundedTreePotentials.Segments.functionalCoeffs_unit line 266
20. lemma OAI.BoundedTreePotentials.Segments.functionalCoeffs_eq line 274
21. lemma OAI.BoundedTreePotentials.Segments.core_test_head line 282
22. lemma OAI.BoundedTreePotentials.Segments.core_head_norming line 294