BulkHalfLogBudgetComparison.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Cost of retaining the original terminal logarithmic factors

theorem OAI.Ostmann.bulkHalfLogWeightedKernelPairBudget_le line 11

Source documentation

Two half-bulk factors per leaf in each tree fit the existing derivative-root budget.

theorem bulkHalfLogWeightedKernelPairBudget_le
    (ψ : 𝓢(ℝ, ℂ)) (V lo hi : ℝ) (n d r e t rlog : ℕ) (B D Dlog : ℝ)
    (hDlog : 0 ≤ Dlog) (ht : t ≤ 4 * 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