Fibre and double counting

TheoremUnique witnesses transported by finite-sum equality#✓fully proved

If every integer-valued sum over T pulls back to the corresponding sum over s, then a property with a unique witness in T pulls back to a property with a unique witness in s.

theorem existsUnique_of_sum_comp {α β : Type*} (s : Finset α) (T : Finset β) (i : α → β)
    (hsum : ∀ F : β → ℤ, ∑ a ∈ s, F (i a) = ∑ b ∈ T, F b)
    (Q : β → Prop) (hQ : ∃! b, b ∈ T ∧ Q b) : ∃! a, a ∈ s ∧ Q (i a)

TheoremLabelings with equal fiber sizes differ by a permutation#✓fully proved

Two labelings of a finite type with equally sized fibers differ by a permutation.

theorem exists_perm_of_fiber {V C : Type*} [Fintype V] [DecidableEq C]
    (α β : V → C)
    (h : ∀ y, Fintype.card {x // α x = y} = Fintype.card {x // β x = y}) :
    ∃ p : Equiv.Perm V, ∀ x, β (p x) = α x

TheoremDensity bounds transfer through equal-fiber maps#✓fully proved

A density bound transfers through a map whose fibers over the target carrier all have the same cardinality.

theorem card_filter_le_of_fibers {Ω X : Type*} [DecidableEq X]
    (Ωs : Finset Ω) (f : Ω → X) (Xs : Finset X) (hf : Set.MapsTo f Ωs Xs)
    (hconst : ∀ x ∈ Xs, ∀ x' ∈ Xs,
      (Ωs.filter fun e => f e = x).card ≤ (Ωs.filter fun e => f e = x').card)
    (Q : X → Prop) [DecidablePred Q] (ε : ℝ)
    (hQ : ((Xs.filter Q).card : ℝ) ≤ ε * Xs.card) :
    ((Ωs.filter fun e => Q (f e)).card : ℝ) ≤ ε * Ωs.card

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.