English
For an integrable function f: α → E, either f equals its average almost everywhere, or there exists a measurable t with 0 < μ(t) and μ(tᶜ) > 0 such that the average of f over t and over its complement tᶜ are different.
Русский
Для интегрируемой функции f:α→E либо f равна своему среднему значению почти всюду, либо существует измеримое множество t с 0 < μ(t) и μ(∖t) > 0, для которого средние значения f по t и по комплементу t различны.
LaTeX
$$$$ f =^a f_{avg} \;\text{или}\; \langle f \rangle_t \neq \langle f \rangle_{t^c}.$$$$
Lean4
/-- If `f : α → E` is an integrable function, then either it is a.e. equal to the constant
`⨍ x, f x ∂μ` or there exists a measurable set such that `μ t ≠ 0`, `μ tᶜ ≠ 0`, and the average
values of `f` over `t` and `tᶜ` are different. -/
theorem ae_eq_const_or_exists_average_ne_compl [IsFiniteMeasure μ] (hfi : Integrable f μ) :
f =ᵐ[μ] const α (⨍ x, f x ∂μ) ∨
∃ t, MeasurableSet t ∧ μ t ≠ 0 ∧ μ tᶜ ≠ 0 ∧ (⨍ x in t, f x ∂μ) ≠ ⨍ x in tᶜ, f x ∂μ :=
by
refine or_iff_not_imp_right.mpr fun H => ?_; push_neg at H
refine hfi.ae_eq_of_forall_setIntegral_eq _ _ (integrable_const _) fun t ht ht' => ?_; clear ht'
simp only [const_apply, setIntegral_const]
by_cases h₀ : μ t = 0
· rw [restrict_eq_zero.2 h₀, integral_zero_measure, measureReal_def, h₀, ENNReal.toReal_zero, zero_smul]
by_cases h₀' : μ tᶜ = 0
· rw [← ae_eq_univ] at h₀'
rw [restrict_congr_set h₀', restrict_univ, measureReal_congr h₀', measure_smul_average]
have := average_mem_openSegment_compl_self ht.nullMeasurableSet h₀ h₀' hfi
rw [← H t ht h₀ h₀', openSegment_same, mem_singleton_iff] at this
rw [this, measure_smul_setAverage _ (measure_ne_top μ _)]
