English
Homogeneity of IndL1: condExpIndL1 hm μ s (c • x) = c • condExpIndL1 hm μ s x.
Русский
Гомогенность IndL1 по скаляру: condExpIndL1 hm μ s (c • x) = c • condExpIndL1 hm μ s x.
LaTeX
$$$condExpIndL1 hm μ s (c \cdot x) = c \cdot condExpIndL1 hm μ s x$$$
Lean4
theorem norm_condExpIndL1Fin_le (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : G) :
‖condExpIndL1Fin hm hs hμs x‖ ≤ μ.real s * ‖x‖ :=
by
rw [L1.norm_eq_integral_norm, ← ENNReal.toReal_ofReal (norm_nonneg x), measureReal_def, ← ENNReal.toReal_mul, ←
ENNReal.ofReal_le_iff_le_toReal (ENNReal.mul_ne_top hμs ENNReal.ofReal_ne_top),
ofReal_integral_norm_eq_lintegral_enorm]
swap; · rw [← memLp_one_iff_integrable]; exact Lp.memLp _
have h_eq : ∫⁻ a, ‖condExpIndL1Fin hm hs hμs x a‖ₑ ∂μ = ∫⁻ a, ‖condExpIndSMul hm hs hμs x a‖ₑ ∂μ :=
by
refine lintegral_congr_ae ?_
filter_upwards [condExpIndL1Fin_ae_eq_condExpIndSMul hm hs hμs x] with z hz
rw [hz]
rw [h_eq, ofReal_norm_eq_enorm]
exact lintegral_nnnorm_condExpIndSMul_le hm hs hμs x
