OAI/Combinatorics/EditApproximation/Geometry/TreeAccounting.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.tree_layer_sum line 25

   Source documentation

   Labeled nodes of a complete M-ary tree at one physical depth.

   theorem tree_layer_sum {M d : ℕ} (weight : TreeLayer M (d + 1) → ℝ) :
       (∑ node : TreeLayer M d, ∑ child : Fin M, weight (node, child)) =
         ∑ node : TreeLayer M (d + 1), weight node := by
   …

   Mentions: OAI.EditApproximation.TreeLayer

2. theorem OAI.EditApproximation.tree_frontier_telescope line 31

   Source documentation

   Mass/energy differences cancel exactly between successive frontiers.

   theorem tree_frontier_telescope (M J : ℕ)
       (weight : (d : ℕ) → TreeLayer M d → ℝ) :
       (∑ d ∈ range J, ∑ node : TreeLayer M d,
         (weight d node - ∑ child : Fin M, weight (d + 1) (node, child))) =
           weight 0 PUnit.unit - ∑ node : TreeLayer M J, weight J node := by
   …

   Mentions: OAI.EditApproximation.TreeLayer

3. theorem OAI.EditApproximation.small_growth_pow line 52

   Source documentation

   The explicit small-growth bound used for the comparison frontiers.

   theorem small_growth_pow {x : ℝ} (n : ℕ) (hx : 0 ≤ x)
       (hsmall : (n : ℝ) * x ≤ 1 / 2) :
       (1 + x) ^ n ≤ 1 + 2 * n * x := by
   …

4. theorem OAI.EditApproximation.curvature_total_from_telescope line 73

   Source documentation

   The final scalar summation of the local curvature/energy estimates. The conservation identities are supplied by tree_frontier_telescope for the comparison masses and energies.

   theorem curvature_total_from_telescope {ι : Type*} (nodes : Finset ι)
       (curvature discrepancy massDifference movement slack energyDifference : ι → ℝ)
       (D rootMass terminalMass : ℝ)
       (hroot : 0 ≤ rootMass) (hterminal : terminalMass ≤ 2 * D)
       (hconservation : (∑ v ∈ nodes, massDifference v) = rootMass - terminalMass)
       (henergy : (∑ v ∈ nodes, energyDifference v) ≤ 2 * D)
       (hdiscrepancy : ∀ v ∈ nodes, 0 ≤ discrepancy v)
       (hslackNonneg : ∀ v ∈ nodes, 0 ≤ slack v)
       (hslack : ∀ v ∈ nodes, massDifference v + discrepancy v ≤ slack v)
       (hcurvature : ∀ v ∈ nodes, curvature v ≤ energyDifference v + 3 * movement v +
         2 * max (-massDifference v) 0) :
       (∑ v ∈ nodes, (curvature v + discrepancy v)) ≤
   …

5. theorem OAI.EditApproximation.curvature_total_parameter_bound line 125

   Source documentation

   Substituting the endpoint and warmup slack totals gives the manuscript's stated curvature constant. Here u=J/P and v=J/T.

   theorem curvature_total_parameter_bound {total movement slack D F u v : ℝ}
       (hD : 0 ≤ D) (hF : 1 ≤ F) (hu : 0 ≤ u) (hv : 0 ≤ v)
       (htotal : total ≤ 8 * D + 3 * movement + 4 * slack)
       (hmove : movement ≤ 4 * u * D)
       (hslack : slack ≤ 512 * F * u * D + 4 * F * v * D) :
       total ≤ 5000 * F * (1 + u + v) * D := by
   …

6. theorem OAI.EditApproximation.bad_node_cost_from_curvature line 144

   Source documentation

   Exceptional-node cost uses the total curvature/discrepancy charge; no count of nodes or independence assumption is needed.

   theorem bad_node_cost_from_curvature {ι : Type*} (nodes : Finset ι)
       (cost scale curvature discrepancy : ι → ℝ) (ratio totalBound : ℝ)
       (hratio : 0 ≤ ratio)
       (hcost : ∀ i ∈ nodes, cost i ≤ 2 * scale i)
       (hcurvature : ∀ i ∈ nodes, 0 ≤ curvature i)
       (hdiscrepancy : ∀ i ∈ nodes, 0 ≤ discrepancy i)
       (htotal : (∑ i ∈ nodes, (curvature i + discrepancy i)) ≤ totalBound) :
       (∑ i ∈ nodes with scale i < ratio * curvature i ∨ scale i < ratio * discrepancy i,
         cost i) ≤ 2 * ratio * totalBound := by
   …