English
In a second-countable target space, the first coordinate is ae-strongly measurable whenever the pair is identDistrib.
Русский
Во втором счетном целевом пространстве первая координата ae-сложно измерима тогда, когда пара identDistrib.
LaTeX
$$[TopologicalSpace γ] [PseudoMetrizableSpace γ] [OpensMeasurableSpace γ] [SecondCountableTopology γ] (h : IdentDistrib f g μ ν) : AEStronglyMeasurable f μ$$
Lean4
theorem eLpNorm_eq [NormedAddCommGroup γ] [OpensMeasurableSpace γ] (h : IdentDistrib f g μ ν) (p : ℝ≥0∞) :
eLpNorm f p μ = eLpNorm g p ν := by
by_cases h0 : p = 0
· simp [h0]
by_cases h_top : p = ∞
· simp only [h_top, eLpNorm, eLpNormEssSup, ENNReal.top_ne_zero, if_true, if_false]
apply essSup_eq
exact h.comp (measurable_coe_nnreal_ennreal.comp measurable_nnnorm)
simp only [eLpNorm_eq_eLpNorm' h0 h_top, eLpNorm', one_div]
congr 1
apply lintegral_eq
exact h.comp (Measurable.pow_const (measurable_coe_nnreal_ennreal.comp measurable_nnnorm) p.toReal)
