Documentation

LeanPool.FullyDynamicMatching.FD1D.Parameters

Parameter choices #

This file makes the parameter choices in the hierarchical matching argument computationally exact. Natural-number division is the floor in the definition of the tree depth.

source
def FD1D.parameterA (m : ℕ) :
ℕ

The regularization parameter a = 200 * ceil(log₂(m+1)).

Equations
Instances For
    source
    def FD1D.depthTarget (m : ℕ) :
    ℕ

    The positive integer whose largest dyadic power determines the tree.

    Equations
    Instances For
      source
      def FD1D.treeDepth (m : ℕ) :
      ℕ

      The depth of the complete dyadic tree.

      Equations
      Instances For
        source
        def FD1D.leafCount (m : ℕ) :
        ℕ

        The number n = 2^L of leaves in the complete dyadic tree.

        Equations
        Instances For
          source
          @[simp]
          theorem FD1D.policyA_eq_parameterA (m : ℕ) :
          policyA m = parameterA m
          source
          theorem FD1D.parameterA_eq_policyA (m : ℕ) :
          parameterA m = policyA m
          source
          theorem FD1D.parameterA_pos {m : ℕ} (hm : 1 ≤ m) :
          0 < parameterA m
          source
          theorem FD1D.parameterA_ne_zero {m : ℕ} (hm : 1 ≤ m) :
          parameterA m ≠ 0
          source
          theorem FD1D.parameterA_cast_pos {m : ℕ} (hm : 1 ≤ m) :
          0 < ↑(parameterA m)
          source
          theorem FD1D.parameterA_cast_ne_zero {m : ℕ} (hm : 1 ≤ m) :
          ↑(parameterA m) ≠ 0
          source
          @[simp]
          theorem FD1D.natFloor_parameterRatio (m : ℕ) :
          ⌊↑m / ↑(parameterA m)⌋₊ = m / parameterA m
          source
          theorem FD1D.depthTarget_pos (m : ℕ) :
          0 < depthTarget m
          source
          theorem FD1D.depthTarget_ne_zero (m : ℕ) :
          depthTarget m ≠ 0
          source
          theorem FD1D.depthTarget_le {m : ℕ} (hm : 1 ≤ m) :
          depthTarget m ≤ m
          source
          theorem FD1D.treeDepth_le_clog {m : ℕ} (hm : 1 ≤ m) :
          treeDepth m ≤ Nat.clog 2 (m + 1)
          source
          theorem FD1D.two_hundred_mul_treeDepth_le_parameterA {m : ℕ} (hm : 1 ≤ m) :
          200 * treeDepth m ≤ parameterA m
          source
          theorem FD1D.parameterA_ge_treeDepth {m : ℕ} (hm : 1 ≤ m) :
          parameterA m ≥ 200 * treeDepth m
          source
          theorem FD1D.parameterA_cast_ge_treeDepth {m : ℕ} (hm : 1 ≤ m) :
          200 * ↑(treeDepth m) ≤ ↑(parameterA m)
          source
          @[simp]
          theorem FD1D.leafCount_eq_pow (m : ℕ) :
          leafCount m = 2 ^ treeDepth m
          source
          theorem FD1D.leafCount_pos (m : ℕ) :
          0 < leafCount m
          source
          theorem FD1D.one_le_leafCount (m : ℕ) :
          1 ≤ leafCount m
          source
          theorem FD1D.leafCount_ne_zero (m : ℕ) :
          leafCount m ≠ 0
          source
          theorem FD1D.leafCount_cast_pos (m : ℕ) :
          0 < ↑(leafCount m)
          source
          theorem FD1D.leafCount_cast_ne_zero (m : ℕ) :
          ↑(leafCount m) ≠ 0
          source
          theorem FD1D.leafCount_le_depthTarget (m : ℕ) :
          leafCount m ≤ depthTarget m

          n is a power of two not exceeding max(1, floor(m/a)).

          source
          theorem FD1D.pow_le_depthTarget_iff {m k : ℕ} :
          2 ^ k ≤ depthTarget m ↔ k ≤ treeDepth m

          Exponent form of the fact that n is the largest admissible power of two.

          source
          theorem FD1D.pow_le_leafCount_of_pow_le_depthTarget {m k : ℕ} (hk : 2 ^ k ≤ depthTarget m) :
          2 ^ k ≤ leafCount m

          Every power of two below the target is at most n.

          source
          theorem FD1D.depthTarget_lt_two_mul_leafCount (m : ℕ) :
          depthTarget m < 2 * leafCount m

          The target is strictly less than twice its largest dyadic power.

          source
          theorem FD1D.parameterQuotient_lt_two_mul_leafCount (m : ℕ) :
          m / parameterA m < 2 * leafCount m
          source
          theorem FD1D.m_le_two_mul_parameterA_mul_leafCount {m : ℕ} (hm : 1 ≤ m) :
          m ≤ 2 * parameterA m * leafCount m

          Natural-number form of the reciprocal leaf-size estimate.

          source
          theorem FD1D.one_div_leafCount_le_two_mul_parameterA_div {m : ℕ} (hm : 1 ≤ m) :
          1 / ↑(leafCount m) ≤ 2 * ↑(parameterA m) / ↑m

          The paper's estimate 1/n ≤ 2a/m, over the reals.

          source
          theorem FD1D.parameterA_cast_le_logb {m : ℕ} (hm : 2 ≤ m) :
          ↑(parameterA m) ≤ 800 * Real.logb 2 ↑m

          A convenient explicit logarithmic bound, still written in base two.

          source
          theorem FD1D.parameterA_cast_le_log {m : ℕ} (hm : 2 ≤ m) :
          ↑(parameterA m) ≤ 800 / Real.log 2 * Real.log ↑m

          Explicit natural-log form of a = O(log m), valid for m ≥ 2.

          source
          theorem FD1D.parameterA_isBigO_log :
          (fun (m : ℕ) => ↑(parameterA m)) =O[Filter.atTop] fun (m : ℕ) => Real.log ↑m

          Asymptotic form of the explicit logarithmic estimate.