HasCompactSupport.exists_simpleFunc_approx_of_prod
theorem HasCompactSupport.exists_simpleFunc_approx_of_prod :
∀ {X : Type u_7} {Y : Type u_8} {α : Type u_9} [inst : Zero α] [inst_1 : TopologicalSpace X]
[inst_2 : TopologicalSpace Y] [inst_3 : MeasurableSpace X] [inst_4 : MeasurableSpace Y]
[inst_5 : OpensMeasurableSpace X] [inst_6 : OpensMeasurableSpace Y] [inst_7 : PseudoMetricSpace α]
{f : X × Y → α},
Continuous f → HasCompactSupport f → ∀ {ε : ℝ}, 0 < ε → ∃ g, ∀ (x : X × Y), dist (f x) (↑g x) < ε
This theorem states that for any continuous function `f` with compact support on a product space (denoted as `X × Y`), it can be uniformly approximated by simple functions. This approximation can be done to any precision `ε` that is greater than zero. The function `f` maps from the product space `X × Y` to some pseudometric space `α`. The subtlety to note here is that the spaces `X` and `Y` are not assumed to be separable, which means the product of their Borel sigma algebras might not contain all open sets. Nevertheless, the theorem states that there are enough sets available to approximate `f` if it has the property of compact support.
More concisely: Given a continuous function `f` with compact support on a non-separable product space `X × Y`, there exists a sequence of simple functions that uniformly approximates `f` to any given precision `ε > 0`.
|
HasCompactSupport.measurable_of_prod
theorem HasCompactSupport.measurable_of_prod :
∀ {X : Type u_7} {Y : Type u_8} {α : Type u_9} [inst : Zero α] [inst_1 : TopologicalSpace X]
[inst_2 : TopologicalSpace Y] [inst_3 : MeasurableSpace X] [inst_4 : MeasurableSpace Y]
[inst_5 : OpensMeasurableSpace X] [inst_6 : OpensMeasurableSpace Y] [inst_7 : TopologicalSpace α]
[inst_8 : TopologicalSpace.PseudoMetrizableSpace α] [inst_9 : MeasurableSpace α] [inst_10 : BorelSpace α]
{f : X × Y → α}, Continuous f → HasCompactSupport f → Measurable f
The theorem states that for any continuous function `f` with compact support mapping from a product space `X × Y` into a space `α`, if `X` and `Y` are topological spaces, `α` is a pseudometrizable and topological space, also measurable with a Borel sigma-algebra, then `f` is measurable. Here, measurability refers to the property that the preimage of every measurable set in the codomain is measurable in the domain. Notably, the spaces `X` and `Y` are not assumed to be separable, meaning they might not contain all open sets; however, they still contain enough to approximate compactly supported continuous functions.
More concisely: A continuous function with compact support from a product of two topological spaces into a pseudometrizable and measurable space is measurable.
|