Theorems · Theorem · measure theory

ContinuousMapZero.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] [inst_4 : Zero ↑s]
  (f : X → Y → E) (g : ContinuousMapZero (↑s) E),
  (∀ᵐ (x : X) ∂μ, ContinuousOn (f x) s) →
    (∀ᵐ (x : X) ∂μ, f x ↑0 = 0) →
      ∀ (bound : X → ℝ),
        MeasureTheory.HasFiniteIntegral bound μ →
          (∀ᵐ (x : X) ∂μ, ∀ y ∈ s, ‖f x y‖ ≤ bound x) →
            MeasureTheory.HasFiniteIntegral (fun x => ContinuousMapZero.mkD (s.domRestrict (f x)) g) μ

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

Defined in

Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero

Cited by

4 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceNormedAddCommGroupCompactSpaceZero