FiniteSeparationArithmetic.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Deficit charges in the finite-tree separation induction

The exact deficit charges are those of prop:finite-separation.

theorem OAI.TreeEdit.BinaryLower.FiniteTree.row_deficit_charge line 14

Source documentation

At least half the children each charge q unmatched symbols.

theorem row_deficit_charge {m : ℕ} (bad : Finset (Fin m))
    (δ : Fin m → ℝ) (q : ℝ) (hq : 0 ≤ q)
    (hnonneg : ∀ i, 0 ≤ δ i) (hbad : ∀ i ∈ bad, q ≤ δ i)
    (hhalf : m ≤ 2 * bad.card) :
    (m : ℝ) * q / 2 ≤ ∑ i, δ i := by
…

theorem OAI.TreeEdit.BinaryLower.FiniteTree.finite_charge_le_gap line 32

Source documentation

The chosen row charge is no larger than the tagged transition gap.

theorem finite_charge_le_gap (m h : ℕ) (hm : 2 ≤ m) (B : ℝ) (hB : 0 ≤ B) :
    (m : ℝ) * (B / (4 : ℝ) ^ h) / 2 ≤ ((m : ℝ) - 1) * B := by
…

theorem OAI.TreeEdit.BinaryLower.FiniteTree.finite_charge_identity line 44

Source documentation

Half the total row charge is exactly the next 4⁻ʰ separation scale.

theorem finite_charge_identity (m T h : ℕ) (B : ℝ) :
    (T : ℝ) * ((m : ℝ) * (B / (4 : ℝ) ^ h) / 2) / 2 =
      ((m : ℝ) * T * B) / (4 : ℝ) ^ (h + 1) := by
…