ProfilePivots.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A common index and greedy pivots at every profile level

The retained index is chosen once from the column weights. At each level, the bounded greedy construction is applied to the actual retained graph balls. All assignments and residual bounds below are consequently proved for the actual partition graphs.

theorem OAI.MetricEntropyDuality.exists_profile_pivots line 26

Source documentation

One common retained index and an actual bounded pivot assignment at each of the finitely many profile levels.

theorem exists_profile_pivots {X : Type uX} {Y : Type uY}
    [Fintype X] [Nonempty X] [Fintype Y]
    {u : ℕ} {Label : Fin u → Type uLabel}
    (L : (i : Fin u) → X → Label i) (v : Y → X) (T : Y → Finset (Fin u))
    (μ : Y → ℝ) (hμ : ∀ y, 0 ≤ μ y) (hmass : ∑ y, μ y ≤ 1)
    (hu : 0 < u) (θ : ℝ) (hθ : 0 < θ) (s : ℕ) (hs : 1 ≤ (s : ℝ) * θ)
    (hcomp : ∀ y, ((Finset.univ \ T y).card : ℝ) ≤ θ * (u : ℝ)) (h : ℕ) :
    ∃ i : Fin u, ∃ centers : Fin h → Fin s → X,
      ∃ assigned : Fin h → Y → Option (Fin s),
        (∑ y ∈ Finset.univ.filter (fun y => i ∉ T y), μ y) ≤ θ ∧
        (∀ j y k, assigned j y = some k →
          i ∈ T y ∧ PartitionGraph.near L (T y) j.val (centers j k) (v y)) ∧
…

Mentions: OAI.MetricEntropyDuality.PartitionGraph.near