CarlesonSorting.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Ordering the moment tuples in the laminar counting lemma

Each tuple has a sorting permutation. Summing over all permutations and then reindexing the tuple sum gives the factorial overcount in §6, count:moment, including repeated occurrences and repeated intervals.

theorem OAI.LipschitzHilbert.tuple_comp_perm_bijective line 26

theorem OAI.LipschitzHilbert.sum_tuple_le_factorial_sum_sorted line 40

Source documentation

A nonnegative permutation-invariant tuple weight loses at most n! when the tuple sum is restricted to one monotone ordering.

theorem sum_tuple_le_factorial_sum_sorted (rank : ι → α) (n : ℕ)
    (w : (Fin n → ι) → ℝ) (hw : ∀ a, 0 ≤ w a)
    (hperm : ∀ (a : Fin n → ι) (σ : Equiv.Perm (Fin n)), w (a ∘ σ) = w a) :
    (∑ a : Fin n → ι, w a) ≤
      (n.factorial : ℝ) * ∑ a : Fin n → ι, if Monotone (rank ∘ a) then w a else 0 := by
…