OAI/Analysis/SignedDisk/ActualMarkTrees1.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SignedDisk.ActualMarkTrees.direction_at_prefix line 33
2. def OAI.SignedDisk.ActualMarkTrees.pathEnergy line 50
3. def OAI.SignedDisk.ActualMarkTrees.pathSwitches line 53
4. lemma OAI.SignedDisk.ActualMarkTrees.mark_nonneg line 57
5. theorem OAI.SignedDisk.ActualMarkTrees.path_switch_bound line 65

   Source documentation

   The switch bound on every genuinely occupied path, using its complete intrinsic history, even before the particle's birth.

   theorem path_switch_bound {N : ℕ} {r R : ℝ} (hr : 0 < r) (hR : 0 ≤ R)
       (hN : R/r+1 ≤ (N:ℝ)) {h : ℂ → ℂ} (hh : Integrable h)
       (hsupp : ∀ y, h y ≠ 0 → ‖y‖ ≤ R) (k : ℕ) (q : Grid N)
       {p : List (Grid N)} (hp : activePath (tree (fun q => vectorMass h r q) k 1 q) p)
       {b : ℕ} (hb : b ≤ p.length) {x : ℂ} (hx : hat r (lastVertex q p) x ≠ 0) :
       pathSwitches h r k x p b ≤ 2+
         2*pathCharge (rootMarkIndicator (1:ℂ) (1/800) (tree (fun q => vectorMass h r q) k 1 q)) p b+
         2000000*pathCharge (pathEnergy h r k q) p b := by
   …

   Mentions: OAI.SignedDisk.ActualMarkTrees.tree, OAI.SignedDisk.ActualMarkTrees.lastVertex, OAI.SignedDisk.ActualMarkTrees.pathSwitches, OAI.SignedDisk.ActualMarkTrees.pathEnergy

6. def OAI.SignedDisk.CommonPrices.sign line 156
7. lemma OAI.SignedDisk.CommonPrices.sign_cases line 157
8. lemma OAI.SignedDisk.CommonPrices.sign_sq line 158
9. def OAI.SignedDisk.CommonPrices.cellPrice line 160
10. def OAI.SignedDisk.CommonPrices.rootWeight line 163
11. lemma OAI.SignedDisk.CommonPrices.rootWeight_nonneg line 165
12. abbrev OAI.SignedDisk.CommonPrices.ErrorIndex line 168
13. def OAI.SignedDisk.CommonPrices.smallPiece line 170
14. lemma OAI.SignedDisk.CommonPrices.smallPiece_mass line 175
15. lemma OAI.SignedDisk.CommonPrices.discounted_smallPiece_mass line 189
16. lemma OAI.SignedDisk.CommonPrices.weighted_defect_sum line 205
17. lemma OAI.SignedDisk.CommonPrices.smallPiece_price line 218
18. lemma OAI.SignedDisk.CommonPrices.smallPiece_common_price line 232
19. def OAI.SignedDisk.CommonPrices.goodRoots line 249
20. def OAI.SignedDisk.CommonPrices.badRoots line 251
21. def OAI.SignedDisk.CommonPrices.rootSum line 254
22. lemma OAI.SignedDisk.CommonPrices.rootSum_integrable line 257
23. lemma OAI.SignedDisk.CommonPrices.rootSum_partition line 261
24. lemma OAI.SignedDisk.CommonPrices.rootSum_mass line 266
25. def OAI.SignedDisk.CommonPrices.goodCone line 281

    Source documentation

    The actual normalized positive-cone part on one cell.

    def goodCone {N : ℕ} {r R : ℝ} (hr : 0 < r) (hR : 0 ≤ R)
        (hN : R/r+1 ≤ (N:ℝ)) {h : ℂ → ℂ} (hh : Integrable h)
        (hsupp : ∀ y, h y ≠ 0 → ‖y‖ ≤ R) (k : ℕ) (p : ℂ) (S : Finset (Grid N))
        {n : ℂ} (hn : ‖n‖ = 1) {s : ℝ} (hs : s = 1 ∨ s = -1) : ConeDensity (axis n s) (1/2) where
    …

26. def OAI.SignedDisk.CommonPrices.badPrice line 301
27. def OAI.SignedDisk.CommonPrices.badPiece line 305

    Source documentation

    Bad cone roots are exactly the unrestricted size-one part.

    def badPiece {N : ℕ} {r : ℝ} (hr : 0 < r) {h : ℂ → ℂ} (hh : Integrable h)
        (k : ℕ) (p : ℂ) (S : Finset (Grid N)) (n : ℂ) : ErrorPiece 2 :=
    …

28. lemma OAI.SignedDisk.CommonPrices.badPiece_mass line 310
29. def OAI.SignedDisk.CommonPrices.cellErrors line 320
30. lemma OAI.SignedDisk.CommonPrices.cellErrors_price line 325
31. lemma OAI.SignedDisk.CommonPrices.smallPiece_pair_sum line 340
32. lemma OAI.SignedDisk.CommonPrices.smallPiece_sum line 348
33. theorem OAI.SignedDisk.CommonPrices.cell_decomposition line 367

    Source documentation

    Exact cell decomposition before imposing the local partition-of-unity region. Both its scalar coordinates and all error densities are the actual finite dyadic construction.

    theorem cell_decomposition {N : ℕ} {r R : ℝ} (hr : 0 < r) (hR : 0 ≤ R)
        (hN : R/r+1 ≤ (N:ℝ)) {h : ℂ → ℂ} (hh : Integrable h)
        (hsupp : ∀ y, h y ≠ 0 → ‖y‖ ≤ R) (k : ℕ) (p : ℂ) (S : Finset (Grid N))
        {n : ℂ} (hn : ‖n‖ = 1) {s : ℝ} (hs : s = 1 ∨ s = -1) (X : ℂ) :
        (goodCone hr hR hN hh hsupp k p S hn hs).density X+
          (∑ i, (cellErrors hr hh k p S n i).density X) =
          rescale p (scale r k) (fun y => (∑ q ∈ S, hat (scale r k) q y) • h y) X := by
    …

    Mentions: OAI.SignedDisk.CommonPrices.goodCone, OAI.SignedDisk.CommonPrices.cellErrors

34. lemma OAI.SignedDisk.DirectionNeighbors.mem_window_comm line 389
35. lemma OAI.SignedDisk.DirectionNeighbors.card_window line 392