Compact Support Domination for Bounded Tests

This gives an integrable domination statement for a compactly supported bounded test.

Let $F,\eta:\mathbb R^n\to\mathbb R$, let $S\subseteq\mathbb R^n$ be compact, and let $C\in\mathbb R$. Assume $F$ is locally integrable, $\eta$ is almost-everywhere strongly measurable, $\operatorname{supp}(\eta)\subseteq S$, and $\|\eta(x)\|\le C$ for every $x$. Then

is integrable, and for every $x$,

Consequently $x\mapsto F(x)\eta(x)$ is integrable with respect to volume measure. The Lean declaration is compact_bounded_test_domination_readable; the hypotheses are pointwise except for the stated a.e. measurability condition.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem compact_bounded_test_domination {n : ℕ}
    {F η : EuclideanSpace ℝ (Fin n) → ℝ} {S : Set (EuclideanSpace ℝ (Fin n))}
    {C : ℝ} (hF : LocallyIntegrable F (volume : Measure (EuclideanSpace ℝ (Fin n))))
    (hS : IsCompact S)
    (hη : AEStronglyMeasurable η (volume : Measure (EuclideanSpace ℝ (Fin n))))
    (hsupp : Function.support η ⊆ S) (hbound : ∀ x, ‖η x‖ ≤ C) :
    Integrable (S.indicator fun x => C * ‖F x‖)
        (volume : Measure (EuclideanSpace ℝ (Fin n))) ∧
      (∀ x, ‖F x * η x‖ ≤ (S.indicator fun y => C * ‖F y‖) x) ∧
      Integrable (fun x => F x * η x)
        (volume : Measure (EuclideanSpace ℝ (Fin n)))

Module navigation

Module: Analysis/WeakDerivative/Calculus.

Previous: integral_weakDeriv_mul_eq_swap · Next: integral_flux_eq_neg_forcing_of_bounded_weak_test.

Source excerpt, lines 1089–1099 · Frozen source 408915f.