α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
this✝ : ∀ (f : α →ₛ E), Memℒp (↑f) p → P ↑f
this : ∀ (f : { x // x ∈ Lp.simpleFunc E p μ }), P ↑↑↑f
⊢ ∀ ⦃f : α → E⦄, Memℒp f p → P f
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
this : ∀ (f : α →ₛ E), Memℒp (↑f) p → P ↑f
⊢ ∀ ⦃f : α → E⦄, Memℒp f p → P f
have : ∀ f : Lp.simpleFunc E p μ, P f := by
  intro f
  exact
    h_ae (Lp.simpleFunc.toSimpleFunc_eq_toFun f) (Lp.simpleFunc.memℒp f)
      (this (Lp.simpleFunc.toSimpleFunc f) (Lp.simpleFunc.memℒp f))
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
this✝¹ : ∀ (f : α →ₛ E), Memℒp (↑f) p → P ↑f
this✝ : ∀ (f : { x // x ∈ Lp.simpleFunc E p μ }), P ↑↑↑f
this : ∀ (f : { x // x ∈ Lp E p }), P ↑↑f
⊢ ∀ ⦃f : α → E⦄, Memℒp f p → P f
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
this✝ : ∀ (f : α →ₛ E), Memℒp (↑f) p → P ↑f
this : ∀ (f : { x // x ∈ Lp.simpleFunc E p μ }), P ↑↑↑f
⊢ ∀ ⦃f : α → E⦄, Memℒp f p → P f
have : ∀ f : Lp E p μ, P f := fun f =>
  (Lp.simpleFunc.denseRange hp_ne_top).induction_on f h_closed this
no goals
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
this✝¹ : ∀ (f : α →ₛ E), Memℒp (↑f) p → P ↑f
this✝ : ∀ (f : { x // x ∈ Lp.simpleFunc E p μ }), P ↑↑↑f
this : ∀ (f : { x // x ∈ Lp E p }), P ↑↑f
⊢ ∀ ⦃f : α → E⦄, Memℒp f p → P f
exact fun f hf => h_ae hf.coeFn_toLp (Lp.memℒp _) (this (hf.toLp f))
case h_ind
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
⊢ ∀ (c : E) {s : Set α} (hs : MeasurableSet s),
    Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p →
      P ↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))

case h_add
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
⊢ ∀ ⦃f g : α →ₛ E⦄,
    Disjoint (support ↑f) (support ↑g) → (Memℒp (↑f) p → P ↑f) → (Memℒp (↑g) p → P ↑g) → Memℒp (↑(f + g)) p → P ↑(f + g)
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
⊢ ∀ (f : α →ₛ E), Memℒp (↑f) p → P ↑f
apply SimpleFunc.induction
case h_ind
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
c : E
s : Set α
hs : MeasurableSet s
h : Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p
⊢ P ↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
case h_ind
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
⊢ ∀ (c : E) {s : Set α} (hs : MeasurableSet s),
    Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p →
      P ↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
intro c s hs h
case pos
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
c : E
s : Set α
hs : MeasurableSet s
h : Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p
hc : c = 0
⊢ P ↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))

case neg
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
c : E
s : Set α
hs : MeasurableSet s
h : Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p
hc : ¬c = 0
⊢ P ↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
case h_ind
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
c : E
s : Set α
hs : MeasurableSet s
h : Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p
⊢ P ↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
by_cases hc : c = 0
case neg
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
c : E
s : Set α
hs : MeasurableSet s
h : Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p
hc : ¬c = 0
hp_pos : p ≠ 0
⊢ P ↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
case neg
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
c : E
s : Set α
hs : MeasurableSet s
h : Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p
hc : ¬c = 0
⊢ P ↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
have hp_pos : p ≠ 0 := (lt_of_lt_of_le zero_lt_one _i.elim).ne'
no goals
case neg
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
c : E
s : Set α
hs : MeasurableSet s
h : Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p
hc : ¬c = 0
hp_pos : p ≠ 0
⊢ P ↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
exact h_ind c hs (SimpleFunc.measure_lt_top_of_memℒp_indicator hp_pos hp_ne_top hc hs h)
case pos
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
s : Set α
hs : MeasurableSet s
h : Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0))) p
⊢ P ↑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0))
case pos
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
c : E
s : Set α
hs : MeasurableSet s
h : Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p
hc : c = 0
⊢ P ↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
subst hc
case h.e'_1
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
s : Set α
hs : MeasurableSet s
h : Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0))) p
⊢ ↑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) = Set.indicator ∅ fun x => 0
case pos
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
s : Set α
hs : MeasurableSet s
h : Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0))) p
⊢ P ↑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0))
convert h_ind 0 MeasurableSet.empty (by simp) using 1
case h.e'_1.h
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
s : Set α
hs : MeasurableSet s
h : Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0))) p
x✝ : α
⊢ ↑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) x✝ = Set.indicator ∅ (fun x => 0) x✝
case h.e'_1
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
s : Set α
hs : MeasurableSet s
h : Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0))) p
⊢ ↑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) = Set.indicator ∅ fun x => 0
ext
no goals
case h.e'_1.h
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
s : Set α
hs : MeasurableSet s
h : Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0))) p
x✝ : α
⊢ ↑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) x✝ = Set.indicator ∅ (fun x => 0) x✝
simp [const]
no goals
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
s : Set α
hs : MeasurableSet s
h : Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0))) p
⊢ ↑↑μ ∅ < ⊤
simp
case h_add
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
f g : α →ₛ E
hfg : Disjoint (support ↑f) (support ↑g)
hf : Memℒp (↑f) p → P ↑f
hg : Memℒp (↑g) p → P ↑g
int_fg : Memℒp (↑(f + g)) p
⊢ P ↑(f + g)
case h_add
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
⊢ ∀ ⦃f g : α →ₛ E⦄,
    Disjoint (support ↑f) (support ↑g) → (Memℒp (↑f) p → P ↑f) → (Memℒp (↑g) p → P ↑g) → Memℒp (↑(f + g)) p → P ↑(f + g)
intro f g hfg hf hg int_fg
case h_add
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
f g : α →ₛ E
hfg : Disjoint (support ↑f) (support ↑g)
hf : Memℒp (↑f) p → P ↑f
hg : Memℒp (↑g) p → P ↑g
int_fg : Memℒp (↑f) p ∧ Memℒp (↑g) p
⊢ P ↑(f + g)
case h_add
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
f g : α →ₛ E
hfg : Disjoint (support ↑f) (support ↑g)
hf : Memℒp (↑f) p → P ↑f
hg : Memℒp (↑g) p → P ↑g
int_fg : Memℒp (↑(f + g)) p
⊢ P ↑(f + g)
rw [SimpleFunc.coe_add,
  memℒp_add_of_disjoint hfg f.stronglyMeasurable g.stronglyMeasurable] at int_fg
no goals
case h_add
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
f g : α →ₛ E
hfg : Disjoint (support ↑f) (support ↑g)
hf : Memℒp (↑f) p → P ↑f
hg : Memℒp (↑g) p → P ↑g
int_fg : Memℒp (↑f) p ∧ Memℒp (↑g) p
⊢ P ↑(f + g)
refine' h_add hfg int_fg.1 int_fg.2 (hf int_fg.1) (hg int_fg.2)
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
this : ∀ (f : α →ₛ E), Memℒp (↑f) p → P ↑f
f : { x // x ∈ Lp.simpleFunc E p μ }
⊢ P ↑↑↑f
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
this : ∀ (f : α →ₛ E), Memℒp (↑f) p → P ↑f
⊢ ∀ (f : { x // x ∈ Lp.simpleFunc E p μ }), P ↑↑↑f
intro f
no goals
α : Type u_1
β : Type ?u.3297285
ι : Type ?u.3297288
E : Type u_2
F : Type ?u.3297294
𝕜 : Type ?u.3297297
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ : α → E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p → Memℒp g p → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Memℒp f p → P f → P g
this : ∀ (f : α →ₛ E), Memℒp (↑f) p → P ↑f
f : { x // x ∈ Lp.simpleFunc E p μ }
⊢ P ↑↑↑f
exact
  h_ae (Lp.simpleFunc.toSimpleFunc_eq_toFun f) (Lp.simpleFunc.memℒp f)
    (this (Lp.simpleFunc.toSimpleFunc f) (Lp.simpleFunc.memℒp f))