Real.measurable_log
theorem Real.measurable_log : Measurable Real.log
The theorem `Real.measurable_log` states that the real logarithm function is measurable. In other words, for every measurable set in the codomain, the preimage of that set under the real logarithm function is also a measurable set. This means if we have a set of real numbers which are suitably 'nice' (measurable), then the set of all numbers which map to that set under the logarithm function is also 'nice' (measurable).
More concisely: The real logarithm function maps measurable sets to measurable sets.
|
Real.aemeasurable_of_aemeasurable_exp
theorem Real.aemeasurable_of_aemeasurable_exp :
∀ {α : Type u_1} {x : MeasurableSpace α} {f : α → ℝ} {μ : MeasureTheory.Measure α},
AEMeasurable (fun x => (f x).exp) μ → AEMeasurable f μ
This theorem states that for any type `α`, any measurable space `x` on `α`, any function `f` from `α` to the real numbers `ℝ`, and any measure `μ` on `α`, if the function obtained by applying the real exponential function to the output of `f` is almost everywhere measurable with respect to the measure `μ`, then the original function `f` is also almost everywhere measurable with respect to the measure `μ`. In other words, the measurability of the composed function, with respect to almost everywhere, implies the measurability of the original function.
More concisely: If a function composited with the real exponential function is almost everywhere measurable, then the original function is almost everywhere measurable.
|
Real.measurable_exp
theorem Real.measurable_exp : Measurable Real.exp
The theorem `Real.measurable_exp` states that the real exponential function (`Real.exp`), which is defined as the real part of the complex exponential, is a measurable function. In the context of measurable spaces, a function is considered measurable if the preimage of every measurable set is also measurable. In this case, for any measurable set in the codomain of the real exponential function, its preimage under the function is also a measurable set in the domain.
More concisely: The real exponential function `Real.exp` is a measurable function from the real numbers to the real numbers.
|
Measurable.exp
theorem Measurable.exp :
∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → ℝ}, Measurable f → Measurable fun x => (f x).exp
This theorem states that for any measurable space `α` and any real-valued function `f` on that space, if `f` is a measurable function, then the function that sends each point `x` in the space to the real exponential of `f(x)` is also measurable. Here, a function is called measurable if the preimage of every measurable set under the function is also measurable. The real exponential function is defined as the real part of the complex exponential function.
More concisely: If `f` is a real-valued, measurable function on a measurable space `α`, then the function `x ↦ exp(f(x))` is measurable.
|