Documentation

TauCeti.Analysis.Convex.Sequence.FiniteSlopeMultiset

Finite slope multisets #

The finite slopes of a convex height sequence are the slopes of all of its unit edges, counted with multiplicity. This file packages that invariant on FiniteSlopeData, the canonical presentation of a nonempty convex height sequence with finite domain.

The multiset has cardinality equal to the horizontal length of the polygon. Its sum is the difference between the endpoint heights. The multiplicity of a real slope σ is the width of the finite face of slope σ, so a singleton face contributes multiplicity zero.

Main results #

References #

source
def TauCeti.FiniteSlopeData.slopeMultiset {Γ : Type u_1} [Preorder Γ] (d : FiniteSlopeData Γ) :
Multiset Γ

The multiset of the slopes of the unit edges of finite slope data.

Each i : Fin length contributes one copy of slope i, so repeated slopes retain their multiplicity. In particular, slope data of length zero has the empty slope multiset.

Instances For
    source
    theorem TauCeti.FiniteSlopeData.slopeMultiset_def {Γ : Type u_1} [Preorder Γ] (d : FiniteSlopeData Γ) :
    d.slopeMultiset = ↑(List.ofFn d.slope)

    The slope multiset lists the slopes of the unit edges from left to right.

    source
    theorem TauCeti.FiniteSlopeData.eq_of_slopeMultiset_eq {Γ : Type u_2} [PartialOrder Γ] {d e : FiniteSlopeData Γ} (hs : d.start = e.start) (hy : d.initialHeight = e.initialHeight) (hm : d.slopeMultiset = e.slopeMultiset) :
    d = e

    A nondecreasing unit-slope presentation is determined by its anchor and slope multiset. In particular, different subdivisions of equal slopes do not give different unit data.

    source
    @[simp]
    theorem TauCeti.FiniteSlopeData.mem_slopeMultiset {Γ : Type u_1} [Preorder Γ] {d : FiniteSlopeData Γ} {m : Γ} :
    m ∈ d.slopeMultiset ↔ ∃ (i : Fin d.length), d.slope i = m

    A value occurs in the slope multiset exactly when it is the slope of a unit edge.

    source
    @[simp]
    theorem TauCeti.FiniteSlopeData.slopeMultiset_eq_zero_iff {Γ : Type u_1} [Preorder Γ] {d : FiniteSlopeData Γ} :
    d.slopeMultiset = 0 ↔ d.length = 0

    The slope multiset is empty exactly when the represented polygon is a singleton.

    source
    @[simp]
    theorem TauCeti.FiniteSlopeData.card_slopeMultiset {Γ : Type u_1} [Preorder Γ] (d : FiniteSlopeData Γ) :
    d.slopeMultiset.card = d.length

    The number of finite unit slopes is the horizontal length of the polygon.

    source
    @[simp]
    theorem TauCeti.FiniteSlopeData.count_slopeMultiset {Γ : Type u_1} [Preorder Γ] [DecidableEq Γ] (d : FiniteSlopeData Γ) (m : Γ) :
    Multiset.count m d.slopeMultiset = {i : Fin d.length | d.slope i = m}.card

    The multiplicity of a value in the slope multiset is the number of unit edges with that slope.

    source
    @[simp]
    theorem TauCeti.FiniteSlopeData.slopeMultiset_map {Γ : Type u_1} [Preorder Γ] {Γ' : Type u_2} [Preorder Γ'] [AddCommMonoid Γ] [AddCommMonoid Γ'] (d : FiniteSlopeData Γ) (f : Γ →+o Γ') :
    (d.map f).slopeMultiset = Multiset.map (⇑f) d.slopeMultiset

    The slope multiset of transported slope data is the image of the slope multiset.

    source
    theorem TauCeti.FiniteSlopeData.sum_slopeMultiset_eq_sum {Γ : Type u_1} [Preorder Γ] [AddCommMonoid Γ] (d : FiniteSlopeData Γ) :
    d.slopeMultiset.sum = ∑ i : Fin d.length, d.slope i

    The sum of the finite slopes is the sum over the unit edges.

    source
    theorem TauCeti.FiniteSlopeData.sum_slopeMultiset {Γ : Type u_1} [Preorder Γ] [AddCommGroup Γ] (d : FiniteSlopeData Γ) :
    d.slopeMultiset.sum = (d.heights (d.start + d.length)).untop₀ - (d.heights d.start).untop₀

    The sum of the finite slopes is the difference between the endpoint heights.

    source
    theorem TauCeti.FiniteSlopeData.exists_isFiniteFace_heights (d : FiniteSlopeData ℝ) (σ : ℝ) :
    ∃ (l : ℕ) (u : ℕ), IsFiniteFace d.heights σ l u

    A polygon represented by real finite slope data has a finite face at every real slope.

    source
    theorem TauCeti.FiniteSlopeData.count_slopeMultiset_of_isFiniteFace (d : FiniteSlopeData ℝ) {σ : ℝ} {l u : ℕ} (hf : IsFiniteFace d.heights σ l u) :
    Multiset.count σ d.slopeMultiset = u - l

    The multiplicity of a real slope σ in the slope multiset is the width u - l of the finite face of slope σ. The endpoints l and u are absolute indices.