GroupedWeights.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Grouping finite nonnegative weights

An optional slot assignment records which columns were retained. Grouping by the assigned slot and by a tag preserves every weighted expression that only depends on those two values. No nonemptiness assumptions are needed.

def OAI.MetricEntropyDuality.groupedWeight line 26
Source documentation
Total weight of columns with the specified slot and tag.
```
def groupedWeight (assignment : Y → Option K) (tag : Y → T) (μ : Y → ℝ)
    (k : K) (t : T) : ℝ := by
…
```
theorem OAI.MetricEntropyDuality.groupedWeight_nonneg line 31
theorem OAI.MetricEntropyDuality.groupedWeight_le_totalMass line 42
theorem OAI.MetricEntropyDuality.groupedWeight_le_one line 53
theorem OAI.MetricEntropyDuality.groupedWeight_eq_zero_of_unused line 59

theorem OAI.MetricEntropyDuality.sum_groupedWeight_mul line 71

Source documentation

Grouping is exact for arbitrary real functions of the slot and tag.

theorem sum_groupedWeight_mul (assignment : Y → Option K) (tag : Y → T)
    (μ : Y → ℝ) (B : K → T → ℝ) :
    (∑ k, ∑ t, groupedWeight assignment tag μ k t * B k t) =
      ∑ y, μ y * (match assignment y with
        | none => 0
        | some k => B k (tag y)) := by
…

Mentions: OAI.MetricEntropyDuality.groupedWeight

theorem OAI.MetricEntropyDuality.sum_groupedWeight_eq line 87

Source documentation

The total grouped weight is exactly the mass of assigned columns.

theorem sum_groupedWeight_eq (assignment : Y → Option K) (tag : Y → T)
    (μ : Y → ℝ) :
    (∑ k, ∑ t, groupedWeight assignment tag μ k t) =
      ∑ y, (match assignment y with
        | none => 0
        | some _ => μ y) := by
…

Mentions: OAI.MetricEntropyDuality.groupedWeight

theorem OAI.MetricEntropyDuality.sum_groupedWeight_le_totalMass line 101
theorem OAI.MetricEntropyDuality.sum_groupedWeight_le_one line 111