WeightedDeficit.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Finite weighted deficits used after the actual leaf-switching estimates.

The scalar argument allows zero leaf weights and returns a positive-weight leaf. The application constructs its vectors using the strictly positive path weights, then supplies the row estimates through block_deficit_of_detection.

def OAI.ReflexiveFixedPoints.pathDeficit line 24

Source documentation

Sum of the nonnegative deficits on the path incident to a leaf.

def pathDeficit {V S : Type*} [Fintype V]
    (R : V → S → Prop) [DecidableRel R]
    (a : V → S → ℝ) (s : S) : ℝ :=
…

def OAI.ReflexiveFixedPoints.IsBadLeaf line 30
Source documentation
Equality at the threshold is bad, so a good leaf has a strict inequality.
```
def IsBadLeaf {V S : Type*}
    (R : V → S → Prop) (a : V → S → ℝ) (s : S) : Prop :=
…
```
def OAI.ReflexiveFixedPoints.badLeafMass line 35
Source documentation
The total weight of leaves with at least one failing incident detector.
```
def badLeafMass {V S : Type*} [Fintype S]
    (R : V → S → Prop) (w : S → ℝ) (a : V → S → ℝ) : ℝ := by
…
```

theorem OAI.ReflexiveFixedPoints.finite_weighted_deficit line 45

Source documentation

Finite double counting gives a common leaf without a lower bound on weights.

The first two conclusions retain the quantitative estimates. The selected leaf has positive weight and satisfies every incident detector strictly.

theorem finite_weighted_deficit
    {V S : Type*} [Fintype V] [Fintype S]
    (R : V → S → Prop) [DecidableRel R]
    (w : S → ℝ) (e : V → ℝ) (a : V → S → ℝ)
    (hw : ∀ s, 0 ≤ w s)
    (hw_sum : (∑ s, w s) = 1)
    (ha : ∀ v s, R v s → a v s ≤ 1)
    (hrow : ∀ v,
      (∑ s, if R v s then w s * (1 - a v s) else 0) ≤ 5 * e v)
    (he_sum : (∑ v, e v) ≤ (1 : ℝ) / 128) :
    (∑ s, w s * pathDeficit R a s) ≤ (5 : ℝ) / 128 ∧
      badLeafMass R w a ≤ (5 : ℝ) / 64 ∧
…

Mentions: OAI.ReflexiveFixedPoints.pathDeficit, OAI.ReflexiveFixedPoints.badLeafMass

theorem OAI.ReflexiveFixedPoints.block_deficit_of_detection line 135

Source documentation

A block's actual telescoping identity turns detection into weighted deficit.

Only the detector is linear. The block outputs may come from nonlinear maps; their actual finite telescoping identity is the input htelescope.

theorem block_deficit_of_detection
    {X S : Type*} [AddCommGroup X] [Module ℝ X]
    (block : Finset S) (w : S → ℝ) (d : S → X)
    (f : X →ₗ[ℝ] ℝ) (U V : X) (W e : ℝ)
    (hmass : (∑ s ∈ block, w s) = W)
    (htelescope : (∑ s ∈ block, w s • d s) = U - V)
    (hdetect : W - 5 * e ≤ f (U - V)) :
    (∑ s ∈ block, w s * (1 - f (d s))) ≤ 5 * e := by
…