Curvature.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Cost-weighted curvature

Finite weighted variance and the local energy telescope from Section 6 of the edit-distance manuscript. Zero child masses are allowed, with the length-gap invariant forcing their length gaps to vanish.

theorem OAI.EditApproximation.weighted_variance_identity line 17
theorem OAI.EditApproximation.curvature_nonneg line 42

theorem OAI.EditApproximation.curvature_l1_squared_le line 54

Source documentation

Weighted Cauchy--Schwarz controls the total absolute deviation by the curvature times the total warmup mass.

theorem curvature_l1_squared_le {ι : Type*} (children : Finset ι)
    (mass gap : ι → ℝ)
    (hmass : ∀ i ∈ children, 0 ≤ mass i)
    (hzero : ∀ i ∈ children, mass i = 0 → gap i = 0)
    (hW : 0 < ∑ i ∈ children, mass i) :
    (∑ i ∈ children,
      |gap i - ((∑ j ∈ children, gap j) / (∑ j ∈ children, mass j)) * mass i|) ^ 2 ≤
      (∑ i ∈ children, mass i) *
        ((∑ i ∈ children, gap i ^ 2 / mass i) -
          (∑ i ∈ children, gap i) ^ 2 / (∑ i ∈ children, mass i)) := by
…

theorem OAI.EditApproximation.curvature_l1_le_sqrt line 77

theorem OAI.EditApproximation.local_energy_discrepancy line 93

Source documentation

The parent/rounded-parent energy discrepancy is controlled by endpoint movement and the negative part of the parent-minus-child mass discrepancy.

theorem local_energy_discrepancy {parentMass childMass parentGap roundedGap movement : ℝ}
    (hp : 0 < parentMass) (hc : 0 < childMass)
    (hparent : |parentGap| ≤ parentMass)
    (hchild : |roundedGap| ≤ childMass)
    (hmove : |parentGap - roundedGap| ≤ movement)
    (hsmall : movement ≤ parentMass) :
    parentGap ^ 2 / parentMass - roundedGap ^ 2 / childMass ≤
      3 * movement + 2 * max (childMass - parentMass) 0 := by
…