OAI/Analysis/LipschitzHilbert/Trees/SourceSharedGoodPath.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Original per-top plane bounds descend to one common good set and one terminal count. The latter is the supremum of the actual first ineligible shifted endpoints, without an additional stopping premise.

  1. theorem OAI.LipschitzHilbert.nonnegative_integral_shared_good line 18

    Source documentation

    Shrinking a good set preserves an integral bound for a nonnegative integrand, even when integrability was proved only after restriction.

    theorem nonnegative_integral_shared_good {X : Type*} [MeasurableSpace X]
    (μ : Measure X) (f : X → ℝ) (localGood good : Set X) (B : ℝ)
    (hgood : MeasurableSet good) (hsub : good ⊆ localGood)
    (hf : ∀ x, 0 ≤ f x)
    (hbound : Integrable (localGood.indicator f) μ ∧
      (∫ x, localGood.indicator f x ∂μ) ≤ B) :
    Integrable (good.indicator f) μ ∧ (∫ x, good.indicator f x ∂μ) ≤ B := by
…
  2. def OAI.LipschitzHilbert.AngularGrid.sourceTopTerminalCount line 44
  3. theorem OAI.LipschitzHilbert.AngularGrid.source_top_shared_good_common_integral line 49