OAI/Analysis/LipschitzHilbert/Trees/SourceShortTreeGlobal.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The original short-tree sum on the full Whitney partition, with integrability and a uniform size-density-area bound.

  1. abbrev OAI.LipschitzHilbert.SourceLabeledLattice.WhitneyCell line 16
  2. def OAI.LipschitzHilbert.SourceLabeledLattice.shortLocalValue line 20
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.packet_univ_nonempty line 27
  4. def OAI.LipschitzHilbert.SourceLabeledLattice.shortTreeValue line 32
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.ordinaryPacketValue_measurable line 40
  6. theorem OAI.LipschitzHilbert.SourceLabeledLattice.finite_cutoff_integral line 52
  7. theorem OAI.LipschitzHilbert.SourceLabeledLattice.short_tree_integrable_bound line 77

    Source documentation

    The original short-tree sum is integrable on the full Whitney partition.

    theorem short_tree_integrable_bound (P : SourceLabeledLattice N κ Label Item)
    (hne : Nonempty P.PacketIndex) (B : ℕ) (hcard : ∀ j, (P.labels j).card≤B)
    (oldSlope : ℝ) (cell : ∀ j, P.labels j → ℤ) (grid : ℤ) (w tau : ℝ)
    (htime : P.topLength≤tau)
    (hslope : ∀ j l, oldSlope+P.rowSlope j l ∈
      scaledAngularCell (w/P.topLength) grid j.val (cell j l))
    (horder : 205≤2*P.order) (M sigma eta : ℝ)
    (hM : 0≤M) (hsigma : 0≤sigma) (heta : 0≤eta)
    (coefficient : P.PacketIndex → EuclideanSpace ℂ κ)
    (hcoefficient : ∀ q, ‖coefficient q‖≤sigma)
    (selector : ∀ j, P.labels j → κ → ℝ → ℂ)
    (hselector : ∀ j l a, Measurable (selector j l a))
…

    Mentions: OAI.LipschitzHilbert.SourceLabeledLattice, OAI.LipschitzHilbert.scaledAngularCell