Theorems · Theorem · measure theory

ContinuousMap.hasFiniteIntegral_mkD_restrict_of_bound

∀ {X : Type u_1} {Y : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : TopologicalSpace Y]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] {s : Set Y} [inst_3 : CompactSpace ↑s] (f : X → Y → E) (g : C(↑s, E)),
  (∀ᵐ (x : X) ∂μ, ContinuousOn (f x) s) →
    ∀ (bound : X → ℝ),
      MeasureTheory.HasFiniteIntegral bound μ →
        (∀ᵐ (x : X) ∂μ, ∀ y ∈ s, ‖f x y‖ ≤ bound x) →
          MeasureTheory.HasFiniteIntegral (fun x => ContinuousMap.mkD (s.domRestrict (f x)) g) μ

A variant of ContinuousMap.hasFiniteIntegral_mkD_of_bound for a family of functions which are continuous on a compact set.

Defined in

Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap

Cited by

4 results in Mathlib

Foundations

Depth 201 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceTopologicalSpaceNormedAddCommGroupCompactSpace