OAI/Analysis/LipschitzHilbert/Trees/UnaryPartitionSum.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact summation over the constructed unary segments.

  1. theorem OAI.LipschitzHilbert.UnarySegmentPartition.indices_disjoint line 18
  2. theorem OAI.LipschitzHilbert.UnarySegmentPartition.indices_union line 27
  3. theorem OAI.LipschitzHilbert.UnarySegmentPartition.sum_blocks line 40
  4. theorem OAI.LipschitzHilbert.sum_Ico_mass_drop line 48
  5. theorem OAI.LipschitzHilbert.unary_partition_weighted_drop_le line 58

    Source documentation

    The discarded errors are charged to actual mass drops. Summation over segments introduces no factor counting the number of tiny drops.

    theorem unary_partition_weighted_drop_le (n : ℕ → ℝ) (hn : Antitone n)
    (start finish : ℕ) (P : UnarySegmentPartition n start finish) {μ Q : ℝ}
    (hμ : μ ≤ 1) (hnpos : ∀ j, start ≤ j → j ≤ finish → 0 < n j)
    (hQ : ∀ j ∈ Finset.Ico start finish, n j ^ μ ≤ Q) :
    (∑ b ∈ P.blocks, n b.1 ^ (μ - 1) * (n b.1 - n b.2)) ≤
      Q * ∑ j ∈ Finset.Ico start finish, pathDrop n j := by
…

    Mentions: OAI.LipschitzHilbert.UnarySegmentPartition, OAI.LipschitzHilbert.pathDrop