OAI/Analysis/LipschitzHilbert/Trees/FiniteGoodPath.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.finite_good_path_domination line 14

   Source documentation

   The bad terminal tops carry at most half the original amount.

   theorem finite_good_path_domination (S bad : Finset τ) (hbadS : bad ⊆ S)
       (w e Q : τ → ℝ) (V C : ℝ) (hV : 0 < V)
       (htotal : ∑ t ∈ S, e t*Q t = V)
       (hprob : ∀ t ∈ bad, e t*Q t/V ≤ C*w t)
       (he : ∀ t ∈ S, e t ≤ C*w t) (hQ : ∀ t ∈ S, 0 ≤ Q t)
       (hbad : C*(∑ t ∈ bad, w t) ≤ 1/2) :
       V ≤ 2*C*∑ t ∈ S\bad, w t*Q t := by
   …