English
Basic lemma about membership in intersections and products of sets: x belongs to a ∩ b exactly when x ∈ a and x ∈ b.
Русский
Базовое лемматическое свойство принадлежности: x ∈ a ∩ b тогда и только тогда, когда x ∈ a и x ∈ b.
LaTeX
$$$$x\\in a\\cap b \\iff x\\in a \\land x\\in b.$$$$
Lean4
/-- To prove something for an arbitrary `MemLp` function in a second countable
Borel normed group, it suffices to show that
* the property holds for (multiples of) characteristic functions;
* is closed under addition;
* the set of functions in the `Lᵖ` space for which the property holds is closed.
* the property is closed under the almost-everywhere equal relation.
It is possible to make the hypotheses in the induction steps a bit stronger, and such conditions
can be added once we need them (for example in `h_add` it is only necessary to consider the sum of
a simple function with a multiple of a characteristic function and that the intersection
of their images is a subset of `{0}`).
-/
@[elab_as_elim]
theorem induction [_i : Fact (1 ≤ p)] (hp_ne_top : p ≠ ∞) (motive : (α → E) → Prop)
(indicator : ∀ (c : E) ⦃s⦄, MeasurableSet s → μ s < ∞ → motive (s.indicator fun _ => c))
(add :
∀ ⦃f g : α → E⦄,
Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g))
(closed : IsClosed {f : Lp E p μ | motive f}) (ae : ∀ ⦃f g⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g) :
∀ ⦃f : α → E⦄, MemLp f p μ → motive f :=
by
have : ∀ f : SimpleFunc α E, MemLp f p μ → motive f :=
by
apply SimpleFunc.induction
· intro c s hs h
by_cases hc : c = 0
· subst hc; convert indicator 0 MeasurableSet.empty (by simp) using 1; ext; simp
have hp_pos : p ≠ 0 := (lt_of_lt_of_le zero_lt_one _i.elim).ne'
exact indicator c hs (SimpleFunc.measure_lt_top_of_memLp_indicator hp_pos hp_ne_top hc hs h)
· intro f g hfg hf hg int_fg
rw [SimpleFunc.coe_add, memLp_add_of_disjoint hfg f.stronglyMeasurable g.stronglyMeasurable] at int_fg
exact add hfg int_fg.1 int_fg.2 (hf int_fg.1) (hg int_fg.2)
have : ∀ f : Lp.simpleFunc E p μ, motive f := by
intro f
exact
ae (Lp.simpleFunc.toSimpleFunc_eq_toFun f) (Lp.simpleFunc.memLp f)
(this (Lp.simpleFunc.toSimpleFunc f) (Lp.simpleFunc.memLp f))
have : ∀ f : Lp E p μ, motive f := fun f => (Lp.simpleFunc.denseRange hp_ne_top).induction_on f closed this
exact fun f hf => ae hf.coeFn_toLp (Lp.memLp _) (this (hf.toLp f))
