CommonIndex.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A common index for all compression levels

For nonnegative column weights of total mass at most one, an average bound on the number of indices omitted by each column gives one index whose omitted mass is at most the same bound. No level parameter enters the selection, so this index can be used at every approximation level.

theorem OAI.MetricEntropyDuality.sum_sub_sum_filter_eq line 23

Source documentation

The mass lost by retaining a filter is exactly the mass of its complement.

theorem sum_sub_sum_filter_eq {Y : Type uY} (s : Finset Y)
    (p : Y → Prop) [DecidablePred p] (μ : Y → ℝ) :
    (∑ y ∈ s, μ y) - (∑ y ∈ s.filter p, μ y) =
      ∑ y ∈ s.filter (fun y => ¬ p y), μ y := by
…

theorem OAI.MetricEntropyDuality.sum_omitted_mass line 31

Source documentation

Count weighted omissions by indices or by columns.

theorem sum_omitted_mass {Y : Type uY} [Fintype Y] {u : ℕ}
    (T : Y → Finset (Fin u)) (μ : Y → ℝ) :
    (∑ i : Fin u, ∑ y ∈ Finset.univ.filter (fun y => i ∉ T y), μ y) =
      ∑ y, μ y * ((Finset.univ \ T y).card : ℝ) := by
…

theorem OAI.MetricEntropyDuality.exists_common_index line 48

Source documentation

One index has omitted mass at most θ; it is chosen before all levels.

theorem exists_common_index {Y : Type uY} [Fintype Y] {u : ℕ}
    (hu : 0 < u) (T : Y → Finset (Fin u)) (μ : Y → ℝ)
    (hμ : ∀ y, 0 ≤ μ y) (hmass : ∑ y, μ y ≤ 1)
    {θ : ℝ} (hθ : 0 ≤ θ)
    (hcomp : ∀ y, ((Finset.univ \ T y).card : ℝ) ≤ θ * (u : ℝ)) :
    ∃ i : Fin u, (∑ y ∈ Finset.univ.filter (fun y => i ∉ T y), μ y) ≤ θ := by
…