WeightedTree.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Positive edge weights and the actual path mass

Path mass is defined recursively from the parent maps and edge weights. Its normalization and its mass on every descendant block are consequences of the normalization at each parent.

theorem OAI.ReflexiveFixedPoints.sum_fiber_partition line 21

Source documentation

Partition a finite sum by the fibers of a function.

theorem sum_fiber_partition {A B M : Type*} [Fintype A] [Fintype B]
    [DecidableEq B] [AddCommMonoid M] (f : A → B) (g : A → M) :
    (∑ b, ∑ a ∈ Finset.univ.filter (fun a => f a = b), g a) = ∑ a, g a := by
…

theorem OAI.ReflexiveFixedPoints.sum_fiber_mul line 28

Source documentation

Regroup a weighted finite sum by the fibers of a function.

theorem sum_fiber_mul {A B R : Type*} [Fintype A] [Fintype B]
    [DecidableEq B] [NonUnitalNonAssocSemiring R]
    (f : A → B) (r : B → R) (g : A → R) :
    (∑ b, r b * (∑ a ∈ Finset.univ.filter (fun a => f a = b), g a)) =
      ∑ a, r (f a) * g a := by
…

structure OAI.ReflexiveFixedPoints.WeightedTree line 45
Source documentation
Positive edge weights, normalized separately over each parent's children.
```
structure WeightedTree (T : OrderedTree) where
…
```
Mentions: OAI.ReflexiveFixedPoints.OrderedTree
theorem OAI.ReflexiveFixedPoints.WeightedTree.weight_nonneg line 55
theorem OAI.ReflexiveFixedPoints.WeightedTree.weight_le_one line 58
def OAI.ReflexiveFixedPoints.WeightedTree.pathWeight line 67
Source documentation
The product of the actual edge weights on the path from the root.
```
def pathWeight : (k : ℕ) → T.Node k → ℝ
  | 0, _ => 1
  | k + 1, c => pathWeight k (T.parent k c) * W.weight k c
```
theorem OAI.ReflexiveFixedPoints.WeightedTree.pathWeight_zero line 71
theorem OAI.ReflexiveFixedPoints.WeightedTree.pathWeight_succ line 73
theorem OAI.ReflexiveFixedPoints.WeightedTree.pathWeight_pos line 76
theorem OAI.ReflexiveFixedPoints.WeightedTree.pathWeight_nonneg line 81
theorem OAI.ReflexiveFixedPoints.WeightedTree.pathWeight_le_one line 84

theorem OAI.ReflexiveFixedPoints.WeightedTree.sum_pathWeight_parent line 97

Source documentation

The parent map pushes the child path masses to the parent path masses.

theorem sum_pathWeight_parent (k : ℕ) (f : T.Node k → ℝ) :
    (∑ c, W.pathWeight (k + 1) c * f (T.parent k c)) =
      ∑ p, W.pathWeight k p * f p := by
…

theorem OAI.ReflexiveFixedPoints.WeightedTree.sum_pathWeight line 112

theorem OAI.ReflexiveFixedPoints.WeightedTree.sum_pathWeight_ancestor line 122

Source documentation

Every ancestor map pushes later-level path masses to earlier-level masses.

theorem sum_pathWeight_ancestor {i j : ℕ} (h : i ≤ j) (f : T.Node i → ℝ) :
    (∑ v, W.pathWeight j v * f (T.ancestorLE h v)) =
      ∑ p, W.pathWeight i p * f p := by
…

theorem OAI.ReflexiveFixedPoints.WeightedTree.descendant_sum_pathWeight line 136
Source documentation
The total mass below a node is exactly that node's path mass.
```
theorem descendant_sum_pathWeight {i j : ℕ} (h : i ≤ j) (p : T.Node i) :
    (∑ v ∈ T.descendants h p, W.pathWeight j v) = W.pathWeight i p := by
…
```
theorem OAI.ReflexiveFixedPoints.WeightedTree.pathWeight_le_ancestor line 142
theorem OAI.ReflexiveFixedPoints.WeightedTree.pathWeight_ratio_pos line 150
theorem OAI.ReflexiveFixedPoints.WeightedTree.pathWeight_ratio_le_one line 154