OAI/NumberTheory/Ostmann/Tree/RationalQuartetCut.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Cutting an actual rational tree at its bottom quartets

The option-valued state records ancestor validity. On a valid cut each state contains the original depth-two tree and its propagated current entries. No quartet replacement or independence hypothesis is used.

  1. def OAI.Ostmann.treeLeafMap line 17
  2. def OAI.Ostmann.treeLeafZipProduct line 22
  3. theorem OAI.Ostmann.treeLeafProduct_quartetBlocks line 27
  4. def OAI.Ostmann.RationalTreeData.cutTwo line 38
  5. theorem OAI.Ostmann.RationalTreeData.frequency_cutTwo line 44
  6. structure OAI.Ostmann.RationalQuartetState line 51
  7. def OAI.Ostmann.rationalQuartetStates line 58
  8. def OAI.Ostmann.quartetCutValue line 72
  9. theorem OAI.Ostmann.quartetCutValue_pair line 78
  10. def OAI.Ostmann.rationalQuartetStateAmplitude line 84
  11. theorem OAI.Ostmann.rationalTreeAmplitude_cut line 90

    Source documentation

    Holding all bottom-quartet products fixes the entire upper recursion.

    theorem rationalTreeAmplitude_cut {p : ℕ} [Fact p.Prime]
    (g : ZMod p → ℂ) (D : (ZMod p)ˣ) (n : ℕ) {C : (ZMod p)ˣ}
    (T : RationalTreeData (ZMod p)ˣ (n + 2) C) (XL XR : (ZMod p)ˣ)
    (c : TreeLeafTuple Bool (n + 2)) (m : TreeLeafTuple (ZMod p)ˣ (n + 2)) :
    rationalTreeAmplitude g D T XL XR c m =
      quartetCutValue (rationalQuartetStateAmplitude g D) n
        (rationalQuartetStates n T XL XR c
          (treeLeafMap (treeLeafProduct 2) n (quartetBlockTupleEquiv (ZMod p)ˣ n m)))
        (quartetBlockTupleEquiv (ZMod p)ˣ n m) := by
…

    Mentions: OAI.Ostmann.RationalTreeData, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.rationalTreeAmplitude, OAI.Ostmann.quartetCutValue, OAI.Ostmann.rationalQuartetStateAmplitude, OAI.Ostmann.rationalQuartetStates, OAI.Ostmann.treeLeafMap, OAI.Ostmann.treeLeafProduct, OAI.Ostmann.quartetBlockTupleEquiv

  12. def OAI.Ostmann.treeLeafZip line 117
  13. def OAI.Ostmann.rationalQuartetStateArgument line 122
  14. theorem OAI.Ostmann.rationalQuartetStates_profile line 128

    Source documentation

    The weighted arguments exposed at the cut are exactly the leaves of the truncated rational tree, with the same invalid-ancestor zeros.

    theorem rationalQuartetStates_profile {p : ℕ} [Fact p.Prime]
    (D : (ZMod p)ˣ) (n : ℕ) {C : (ZMod p)ˣ}
    (T : RationalTreeData (ZMod p)ˣ (n + 2) C) (XL XR : (ZMod p)ˣ)
    (c : TreeLeafTuple Bool (n + 2)) (P : TreeLeafTuple (ZMod p)ˣ n)
    (w : TreeLeafTuple (ZMod p → ℝ) n) :
    quartetCutValue (fun S (wp : (ZMod p → ℝ) × (ZMod p)ˣ) =>
        wp.1 (rationalQuartetStateArgument D S wp.2)) n
      (rationalQuartetStates n T XL XR c P) (treeLeafZip n w P) =
      rationalProfileLeafValue D (T.cutTwo n) w XL XR P := by
…

    Mentions: OAI.Ostmann.RationalTreeData, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.quartetCutValue, OAI.Ostmann.rationalQuartetStateArgument, OAI.Ostmann.rationalQuartetStates, OAI.Ostmann.treeLeafZip, OAI.Ostmann.rationalProfileLeafValue

  15. theorem OAI.Ostmann.rationalQuartetStates_profile_mean_le line 151

    Source documentation

    Horizontal density domination applies directly to the genuine cut states, even though their current entries depend on the product vector.

    theorem rationalQuartetStates_profile_mean_le {p : ℕ} [Fact p.Prime]
    (D : (ZMod p)ˣ) (n : ℕ) {C : (ZMod p)ˣ}
    (T : RationalTreeData (ZMod p)ˣ (n + 2) C) (XL XR : (ZMod p)ˣ)
    (c : TreeLeafTuple Bool (n + 2))
    (w : TreeLeafTuple (ZMod p → ℝ) n) (hw : treeWeightsNonneg n w) :
    (∑ P : TreeLeafTuple (ZMod p)ˣ n,
      quartetCutValue (fun S (wp : (ZMod p → ℝ) × (ZMod p)ˣ) =>
        wp.1 (rationalQuartetStateArgument D S wp.2)) n
        (rationalQuartetStates n T XL XR c P) (treeLeafZip n w P)) /
      (Fintype.card (TreeLeafTuple (ZMod p)ˣ n) : ℝ) ≤
        (2 : ℝ) ^ (2 ^ n - 1) * treeProfileMean n w := by
…

    Mentions: OAI.Ostmann.RationalTreeData, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.treeWeightsNonneg, OAI.Ostmann.quartetCutValue, OAI.Ostmann.rationalQuartetStateArgument, OAI.Ostmann.rationalQuartetStates, OAI.Ostmann.treeLeafZip, OAI.Ostmann.treeProfileMean