OAI/Probability/DilutedSpin/ShiftedFrameGeometry.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.PrescribedTree.branchingCount_stem line 14
2. def OAI.DilutedSpinGlass.PrescribedTree.shiftedPrefixDepths line 24

   Source documentation

   Charged depths after retaining the genuine shared prefix above d.

   noncomputable def shiftedPrefixDepths (S : PrescribedTree n) (d : ℕ) : Finset ℕ :=
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree

3. lemma OAI.DilutedSpinGlass.PrescribedTree.mem_shiftedPrefixDepths line 27
4. theorem OAI.DilutedSpinGlass.PrescribedTree.shifted_prefix_old_count line 34

   Source documentation

   No old branch can pay a charged target factor, even below a retained shared prefix. Equal-depth occurrences in the twins remain separate.

   theorem shifted_prefix_old_count (S : PrescribedTree n) (d : ℕ)
       (hS : NoAdjacentBranchDepths S) :
       branchingCount (stem (doubled (bottomUnary S)) d) (· ∈ shiftedPrefixDepths S d)=0 := by
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.NoAdjacentBranchDepths, OAI.DilutedSpinGlass.PrescribedTree.branchingCount, OAI.DilutedSpinGlass.PrescribedTree.stem, OAI.DilutedSpinGlass.PrescribedTree.doubled, OAI.DilutedSpinGlass.PrescribedTree.bottomUnary, OAI.DilutedSpinGlass.PrescribedTree.shiftedPrefixDepths

5. theorem OAI.DilutedSpinGlass.PrescribedTree.shifted_prefix_target_count line 40
6. theorem OAI.DilutedSpinGlass.PrescribedTree.shifted_prefix_total_count line 46
7. lemma OAI.DilutedSpinGlass.PrescribedTree.branchRegular_unary line 52
8. lemma OAI.DilutedSpinGlass.PrescribedTree.branchRegular_grid_stem line 57
9. lemma OAI.DilutedSpinGlass.PrescribedTree.branchRegular_grid_of_lower line 73

   Source documentation

   All higher-degree factors below a regularly interior evaluation depth are uniformly positive; no regularity of a union of shapes is needed.

   lemma branchRegular_grid_of_lower (S : PrescribedTree n) (d L : ℕ) (η : ℝ)
       (h : η≤(d:ℝ)/(L:ℝ)) : BranchRegular S (grid n d L) η := by
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.BranchRegular, OAI.DilutedSpinGlass.PrescribedTree.grid

10. lemma OAI.DilutedSpinGlass.PrescribedTree.branchRegular_shifted_frame line 91
11. theorem OAI.DilutedSpinGlass.PrescribedTree.shifted_prefix_relative_charge line 112

    Source documentation

    Exact cancellation of all powers of the grid mesh in the absolute extension cost, with arbitrary shared prefixes and aligned twin depths.

    theorem shifted_prefix_relative_charge (S : PrescribedTree n) (d k : ℕ)
        (a b : (stem (doubled (unary S)) d).Leaf) (hab : a≠b)
        (η : ℝ) (hη : 0<η)
        (hr : BranchRegular (stem (doubled (unary S)) d) (grid (n+1+1+d) 0 (n+1+1+d)) η) :
        shiftedCharge (shiftedPrefixDepths S d) (stem (doubled (unary S)) d)
            (stem (doubled (bottomUnary S)) d) k /
          |partialKappa (stem (doubled (unary S)) d) (grid (n+1+1+d) 0 (n+1+1+d)) Finset.univ /
            partialKappa (stem (doubled (unary S)) d) (grid (n+1+1+d) 0 (n+1+1+d)) {b,a}| ≤
          chargeBound (2*(leaves (stem (doubled (bottomUnary S)) d)+k:ℕ))
            (((shiftedPrefixDepths S d).card:ℝ)*(leaves (stem (doubled (bottomUnary S)) d)+k:ℕ)) k
            (2*branchingCount S (fun _ => True)) /
              η^(branchExcess (stem (doubled (unary S)) d)) := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.stem, OAI.DilutedSpinGlass.PrescribedTree.doubled, OAI.DilutedSpinGlass.PrescribedTree.unary, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.BranchRegular, OAI.DilutedSpinGlass.PrescribedTree.grid, OAI.DilutedSpinGlass.PrescribedTree.shiftedCharge, OAI.DilutedSpinGlass.PrescribedTree.shiftedPrefixDepths, OAI.DilutedSpinGlass.PrescribedTree.bottomUnary, OAI.DilutedSpinGlass.PrescribedTree.partialKappa, OAI.DilutedSpinGlass.PrescribedTree.chargeBound, OAI.DilutedSpinGlass.PrescribedTree.leaves, OAI.DilutedSpinGlass.PrescribedTree.branchingCount, OAI.DilutedSpinGlass.PrescribedTree.branchExcess