Documentation

LeanPool.FullyDynamicMatching.FD1D.V5.Parameters

Parameters for manuscript bundle v5 #

This module records the exact choices

a = 2000 * ceil(log₂(m+1)) and n = 2^L = 2^floor(log₂(max(1, floor(m/a)))).

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

The v5 regularization parameter.

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

    The positive integer whose largest dyadic power determines the depth.

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

      The depth of the complete dyadic partition.

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

        The number of leaves in the complete dyadic partition.

        Equations
        Instances For
          source
          theorem FD1D.V5.parameterA_pos {m : ℕ} (hm : 1 ≤ m) :
          0 < parameterA m
          source
          theorem FD1D.V5.parameterA_cast_pos {m : ℕ} (hm : 1 ≤ m) :
          0 < ↑(parameterA m)
          source
          theorem FD1D.V5.depthTarget_pos (m : ℕ) :
          0 < depthTarget m
          source
          theorem FD1D.V5.depthTarget_le {m : ℕ} (hm : 1 ≤ m) :
          depthTarget m ≤ m
          source
          theorem FD1D.V5.treeDepth_le_clog {m : ℕ} (hm : 1 ≤ m) :
          treeDepth m ≤ Nat.clog 2 (m + 1)
          source
          theorem FD1D.V5.two_thousand_mul_treeDepth_le_parameterA {m : ℕ} (hm : 1 ≤ m) :
          2000 * treeDepth m ≤ parameterA m

          The exact depth budget a ≥ 2000 L.

          source
          theorem FD1D.V5.parameterA_cast_ge_treeDepth {m : ℕ} (hm : 1 ≤ m) :
          2000 * ↑(treeDepth m) ≤ ↑(parameterA m)
          source
          theorem FD1D.V5.leafCount_pos (m : ℕ) :
          0 < leafCount m
          source
          theorem FD1D.V5.leafCount_cast_pos (m : ℕ) :
          0 < ↑(leafCount m)
          source
          theorem FD1D.V5.leafCount_le_depthTarget (m : ℕ) :
          leafCount m ≤ depthTarget m
          source
          theorem FD1D.V5.depthTarget_lt_two_mul_leafCount (m : ℕ) :
          depthTarget m < 2 * leafCount m
          source
          theorem FD1D.V5.parameterQuotient_lt_two_mul_leafCount (m : ℕ) :
          m / parameterA m < 2 * leafCount m
          source
          theorem FD1D.V5.m_le_two_mul_parameterA_mul_leafCount {m : ℕ} (hm : 1 ≤ m) :
          m ≤ 2 * parameterA m * leafCount m
          source
          theorem FD1D.V5.one_div_leafCount_le_two_mul_parameterA_div {m : ℕ} (hm : 1 ≤ m) :
          1 / ↑(leafCount m) ≤ 2 * ↑(parameterA m) / ↑m

          The spatial discretization estimate 1/n ≤ 2a/m.

          source
          theorem FD1D.V5.log_one_add_two_mul_div_le_parameterA_div_two_thousand {m : ℕ} (hm : 1 ≤ m) :
          Real.log (1 + 2 * ↑m / ↑(parameterA m)) ≤ ↑(parameterA m) / 2000

          The potential budget used in the transient energy estimate.

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

          A convenient explicit base-two logarithmic upper bound.

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

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

          source
          theorem FD1D.V5.parameterA_cast_le_log_succ {m : ℕ} (hm : 2 ≤ m) :
          ↑(parameterA m) ≤ 8000 / Real.log 2 * Real.log ↑(m + 1)

          The same bound in the manuscript's displayed log(m+1) form.

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

          Asymptotic natural-log form of the parameter estimate.