OAI/NumberTheory/Ostmann/Arithmetic/BulkLogBudgetComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.bulkLogWeightedKernelPairBudget_le line 13

   Source documentation

   Two trees have at most twice their leaf count in logarithmic factors. Their additional derivative-root cuts cost at most one more copy of the existing root budget. Only a fixed, depth-dependent variation factor remains.

   theorem bulkLogWeightedKernelPairBudget_le
       (ψ : 𝓢(ℝ, ℂ)) (V lo hi : ℝ) (n d r e t rlog : ℕ) (B D Dlog : ℝ)
       (hDlog : 0 ≤ Dlog) (ht : t ≤ 2 * 2 ^ n) (hr : rlog ≤ r) :
       bulkLogWeightedKernelPairBudget ψ V lo hi n d r e t rlog B D Dlog ≤
         (2 * (2 + Dlog * (Real.exp 2 - 1)) ^ t) *
           bulkKernelPairComparisonBudget ψ V lo hi n d r e B D := by
   …

   Mentions: OAI.Ostmann.bulkLogWeightedKernelPairBudget, OAI.Ostmann.bulkKernelPairComparisonBudget