SwitchingScalar.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Scalar estimates for finite leaf switching

The first estimates telescope the actual scaled ancestor recurrence. The second estimates bound a finite dyadic tolerance tail, including an empty tail. These lemmas involve only real scalars and finite sums; the switching construction supplies their hypotheses from its actual maps and weights.

theorem OAI.ReflexiveFixedPoints.scaled_path_step line 26
Source documentation
Multiplying the one-step displacement estimate by the parent weight produces the telescoping form, using the actual child-weight equation.
```
theorem scaled_path_step {w w' a a' α δ : ℝ}
    (hw : 0 ≤ w) (hchild : w' = w * α)
    (hstep : a ≤ α * a' + (1 - α) + δ) :
    w * a ≤ w' * a' + w - w' + w * δ := by
…
```

theorem OAI.ReflexiveFixedPoints.scaled_path_telescope line 37

Source documentation

The scaled finite path recurrence telescopes without division by weights. This identity needs no positive lower bound on any path weight.

theorem scaled_path_telescope (W A δ : ℕ → ℝ) (k : ℕ)
    (hstep : ∀ i < k,
      W i * A i ≤ W (i + 1) * A (i + 1) + W i - W (i + 1) + W i * δ i) :
    W 0 * A 0 ≤ W k * A k + W 0 - W k +
      ∑ i ∈ Finset.range k, W i * δ i := by
…

theorem OAI.ReflexiveFixedPoints.before_block_scalar_le line 57

Source documentation

The root displacement bound used before a whole descendant block switches. Both the terminal displacement and the unweighted ancestor error budget are at most e; path weights lie in the unit interval.

theorem before_block_scalar_le (W A δ : ℕ → ℝ) (k : ℕ) (e : ℝ)
    (hroot : W 0 = 1)
    (hW : ∀ i ≤ k, 0 ≤ W i ∧ W i ≤ 1)
    (he : 0 ≤ e) (hterminal : A k ≤ e)
    (hδ : ∀ i < k, 0 ≤ δ i)
    (hbudget : ∑ i ∈ Finset.range k, δ i ≤ e)
    (hstep : ∀ i < k,
      W i * A i ≤ W (i + 1) * A (i + 1) + W i - W (i + 1) + W i * δ i) :
    A 0 ≤ 1 - W k + 2 * e := by
…

theorem OAI.ReflexiveFixedPoints.dyadic_sum_range line 86
Source documentation
Exact finite geometric sum for the dyadic tolerance coefficients.
```
theorem dyadic_sum_range (N : ℕ) :
    (∑ d ∈ Finset.range N, (1 / 2 : ℝ) ^ (d + 1)) = 1 - (1 / 2 : ℝ) ^ N := by
…
```
theorem OAI.ReflexiveFixedPoints.dyadic_sum_Ico line 97
Source documentation
Exact finite dyadic tail, including the endpoint term that is discarded in the later upper bound.
```
theorem dyadic_sum_Ico (k N : ℕ) (hkN : k ≤ N) :
    (∑ d ∈ Finset.Ico k N, (1 / 2 : ℝ) ^ (d + 1)) =
      (1 / 2 : ℝ) ^ k - (1 / 2 : ℝ) ^ N := by
…
```

theorem OAI.ReflexiveFixedPoints.dyadic_weighted_tail_le line 105

Source documentation

A nonnegative decreasing budget schedule bounds every finite dyadic tolerance tail. No infinite series or limiting interchange is used.

theorem dyadic_weighted_tail_le (M : ℕ → ℝ)
    (hM_nonneg : ∀ d, 0 ≤ M d) (hM_anti : Antitone M)
    (k N : ℕ) (hkN : k ≤ N) :
    (∑ d ∈ Finset.Ico k N, (1 / 2 : ℝ) ^ (d + 1) * M d) ≤
      (1 / 2 : ℝ) ^ k * M k := by
…

theorem OAI.ReflexiveFixedPoints.dyadic_weighted_tail_le_initial line 124

Source documentation

The same finite tail is at most the budget at its initial level.

theorem dyadic_weighted_tail_le_initial (M : ℕ → ℝ)
    (hM_nonneg : ∀ d, 0 ≤ M d) (hM_anti : Antitone M)
    (k N : ℕ) (hkN : k ≤ N) :
    (∑ d ∈ Finset.Ico k N, (1 / 2 : ℝ) ^ (d + 1) * M d) ≤ M k := by
…

theorem OAI.ReflexiveFixedPoints.dyadic_weighted_tail_le_budget line 137

Source documentation

Uniform comparison with any particular node budget at the same level.

theorem dyadic_weighted_tail_le_budget (M : ℕ → ℝ)
    (hM_nonneg : ∀ d, 0 ≤ M d) (hM_anti : Antitone M)
    (k N : ℕ) (hkN : k ≤ N) {e : ℝ} (hbudget : M k ≤ e) :
    (∑ d ∈ Finset.Ico k N, (1 / 2 : ℝ) ^ (d + 1) * M d) ≤ e :=
…