α : Type u_1
β : Type ?u.1629871
ι : Type ?u.1629874
E : Type u_2
F : Type ?u.1629880
𝕜 : Type ?u.1629883
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : { x // x ∈ simpleFunc E p μ } → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤), P (indicatorConst p hs (_ : ↑↑μ s ≠ ⊤) c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p) (hg : Memℒp (↑g) p),
    Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
f : { x // x ∈ simpleFunc E p μ }
⊢ ∀ (f : α →ₛ E) (hf : Memℒp (↑f) p), P (toLp f hf)
α : Type u_1
β : Type ?u.1629871
ι : Type ?u.1629874
E : Type u_2
F : Type ?u.1629880
𝕜 : Type ?u.1629883
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : { x // x ∈ simpleFunc E p μ } → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤), P (indicatorConst p hs (_ : ↑↑μ s ≠ ⊤) c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p) (hg : Memℒp (↑g) p),
    Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
f : { x // x ∈ simpleFunc E p μ }
⊢ P f
suffices ∀ f : α →ₛ E, ∀ hf : Memℒp f p μ, P (toLp f hf) by
  rw [← toLp_toSimpleFunc f]
  apply this
α : Type u_1
β : Type ?u.1629871
ι : Type ?u.1629874
E : Type u_2
F : Type ?u.1629880
𝕜 : Type ?u.1629883
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : { x // x ∈ simpleFunc E p μ } → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤), P (indicatorConst p hs (_ : ↑↑μ s ≠ ⊤) c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p) (hg : Memℒp (↑g) p),
    Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
⊢ ∀ (f : α →ₛ E) (hf : Memℒp (↑f) p), P (toLp f hf)
α : Type u_1
β : Type ?u.1629871
ι : Type ?u.1629874
E : Type u_2
F : Type ?u.1629880
𝕜 : Type ?u.1629883
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : { x // x ∈ simpleFunc E p μ } → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤), P (indicatorConst p hs (_ : ↑↑μ s ≠ ⊤) c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p) (hg : Memℒp (↑g) p),
    Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
f : { x // x ∈ simpleFunc E p μ }
⊢ ∀ (f : α →ₛ E) (hf : Memℒp (↑f) p), P (toLp f hf)
clear f
case h_ind
α : Type u_1
β : Type ?u.1629871
ι : Type ?u.1629874
E : Type u_2
F : Type ?u.1629880
𝕜 : Type ?u.1629883
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : { x // x ∈ simpleFunc E p μ } → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤), P (indicatorConst p hs (_ : ↑↑μ s ≠ ⊤) c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p) (hg : Memℒp (↑g) p),
    Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
⊢ ∀ (c : E) {s : Set α} (hs : MeasurableSet s)
    (hf : Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p),
    P (toLp (SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) hf)

case h_add
α : Type u_1
β : Type ?u.1629871
ι : Type ?u.1629874
E : Type u_2
F : Type ?u.1629880
𝕜 : Type ?u.1629883
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : { x // x ∈ simpleFunc E p μ } → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤), P (indicatorConst p hs (_ : ↑↑μ s ≠ ⊤) c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p) (hg : Memℒp (↑g) p),
    Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
⊢ ∀ ⦃f g : α →ₛ E⦄,
    Disjoint (support ↑f) (support ↑g) →
      (∀ (hf : Memℒp (↑f) p), P (toLp f hf)) →
        (∀ (hf : Memℒp (↑g) p), P (toLp g hf)) → ∀ (hf : Memℒp (↑(f + g)) p), P (toLp (f + g) hf)
α : Type u_1
β : Type ?u.1629871
ι : Type ?u.1629874
E : Type u_2
F : Type ?u.1629880
𝕜 : Type ?u.1629883
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : { x // x ∈ simpleFunc E p μ } → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤), P (indicatorConst p hs (_ : ↑↑μ s ≠ ⊤) c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p) (hg : Memℒp (↑g) p),
    Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
⊢ ∀ (f : α →ₛ E) (hf : Memℒp (↑f) p), P (toLp f hf)
apply SimpleFunc.induction
α : Type u_1
β : Type ?u.1629871
ι : Type ?u.1629874
E : Type u_2
F : Type ?u.1629880
𝕜 : Type ?u.1629883
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : { x // x ∈ simpleFunc E p μ } → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤), P (indicatorConst p hs (_ : ↑↑μ s ≠ ⊤) c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p) (hg : Memℒp (↑g) p),
    Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
f : { x // x ∈ simpleFunc E p μ }
this : ∀ (f : α →ₛ E) (hf : Memℒp (↑f) p), P (toLp f hf)
⊢ P (toLp (toSimpleFunc f) (_ : Memℒp (↑(toSimpleFunc f)) p))
α : Type u_1
β : Type ?u.1629871
ι : Type ?u.1629874
E : Type u_2
F : Type ?u.1629880
𝕜 : Type ?u.1629883
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : { x // x ∈ simpleFunc E p μ } → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤), P (indicatorConst p hs (_ : ↑↑μ s ≠ ⊤) c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p) (hg : Memℒp (↑g) p),
    Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
f : { x // x ∈ simpleFunc E p μ }
this : ∀ (f : α →ₛ E) (hf : Memℒp (↑f) p), P (toLp f hf)
⊢ P f
rw [← toLp_toSimpleFunc f]
no goals
α : Type u_1
β : Type ?u.1629871
ι : Type ?u.1629874
E : Type u_2
F : Type ?u.1629880
𝕜 : Type ?u.1629883
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : { x // x ∈ simpleFunc E p μ } → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤), P (indicatorConst p hs (_ : ↑↑μ s ≠ ⊤) c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p) (hg : Memℒp (↑g) p),
    Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
f : { x // x ∈ simpleFunc E p μ }
this : ∀ (f : α →ₛ E) (hf : Memℒp (↑f) p), P (toLp f hf)
⊢ P (toLp (toSimpleFunc f) (_ : Memℒp (↑(toSimpleFunc f)) p))
apply this
case h_ind
α : Type u_1
β : Type ?u.1629871
ι : Type ?u.1629874
E : Type u_2
F : Type ?u.1629880
𝕜 : Type ?u.1629883
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : { x // x ∈ simpleFunc E p μ } → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤), P (indicatorConst p hs (_ : ↑↑μ s ≠ ⊤) c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p) (hg : Memℒp (↑g) p),
    Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
c : E
s : Set α
hs : MeasurableSet s
hf : Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p
⊢ P (toLp (SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) hf)
case h_ind
α : Type u_1
β : Type ?u.1629871
ι : Type ?u.1629874
E : Type u_2
F : Type ?u.1629880
𝕜 : Type ?u.1629883
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : { x // x ∈ simpleFunc E p μ } → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤), P (indicatorConst p hs (_ : ↑↑μ s ≠ ⊤) c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p) (hg : Memℒp (↑g) p),
    Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
⊢ ∀ (c : E) {s : Set α} (hs : MeasurableSet s)
    (hf : Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p),
    P (toLp (SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) hf)
intro c s hs hf
case pos
α : Type u_1
β : Type ?u.1629871
ι : Type ?u.1629874
E : Type u_2
F : Type ?u.1629880
𝕜 : Type ?u.1629883
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : { x // x ∈ simpleFunc E p μ } → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤), P (indicatorConst p hs (_ : ↑↑μ s ≠ ⊤) c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p) (hg : Memℒp (↑g) p),
    Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
c : E
s : Set α
hs : MeasurableSet s
hf : Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p
hc : c = 0
⊢ P (toLp (SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) hf)

case neg
α : Type u_1
β : Type ?u.1629871
ι : Type ?u.1629874
E : Type u_2
F : Type ?u.1629880
𝕜 : Type ?u.1629883
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : { x // x ∈ simpleFunc E p μ } → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤), P (indicatorConst p hs (_ : ↑↑μ s ≠ ⊤) c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p) (hg : Memℒp (↑g) p),
    Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
c : E
s : Set α
hs : MeasurableSet s
hf : Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p
hc : ¬c = 0
⊢ P (toLp (SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) hf)
case h_ind
α : Type u_1
β : Type ?u.1629871
ι : Type ?u.1629874
E : Type u_2
F : Type ?u.1629880
𝕜 : Type ?u.1629883
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : { x // x ∈ simpleFunc E p μ } → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤), P (indicatorConst p hs (_ : ↑↑μ s ≠ ⊤) c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p) (hg : Memℒp (↑g) p),
    Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
c : E
s : Set α
hs : MeasurableSet s
hf : Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p
⊢ P (toLp (SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) hf)
by_cases hc : c = 0
no goals
case neg
α : Type u_1
β : Type ?u.1629871
ι : Type ?u.1629874
E : Type u_2
F : Type ?u.1629880
𝕜 : Type ?u.1629883
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : { x // x ∈ simpleFunc E p μ } → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤), P (indicatorConst p hs (_ : ↑↑μ s ≠ ⊤) c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p) (hg : Memℒp (↑g) p),
    Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
c : E
s : Set α
hs : MeasurableSet s
hf : Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p
hc : ¬c = 0
⊢ P (toLp (SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) hf)
exact h_ind c hs (SimpleFunc.measure_lt_top_of_memℒp_indicator hp_pos hp_ne_top hc hs hf)
case h.e'_1
α : Type u_1
β : Type ?u.1629871
ι : Type ?u.1629874
E : Type u_2
F : Type ?u.1629880
𝕜 : Type ?u.1629883
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : { x // x ∈ simpleFunc E p μ } → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤), P (indicatorConst p hs (_ : ↑↑μ s ≠ ⊤) c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p) (hg : Memℒp (↑g) p),
    Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
c : E
s : Set α
hs : MeasurableSet s
hf : Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p
hc : c = 0
⊢ toLp (SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) hf =
    indicatorConst p (_ : MeasurableSet ∅) (_ : ↑↑μ ∅ ≠ ⊤) 0
case pos
α : Type u_1
β : Type ?u.1629871
ι : Type ?u.1629874
E : Type u_2
F : Type ?u.1629880
𝕜 : Type ?u.1629883
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : { x // x ∈ simpleFunc E p μ } → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤), P (indicatorConst p hs (_ : ↑↑μ s ≠ ⊤) c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p) (hg : Memℒp (↑g) p),
    Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
c : E
s : Set α
hs : MeasurableSet s
hf : Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p
hc : c = 0
⊢ P (toLp (SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) hf)
convert h_ind 0 MeasurableSet.empty (by simp) using 1
case h.e'_1.a
α : Type u_1
β : Type ?u.1629871
ι : Type ?u.1629874
E : Type u_2
F : Type ?u.1629880
𝕜 : Type ?u.1629883
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : { x // x ∈ simpleFunc E p μ } → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤), P (indicatorConst p hs (_ : ↑↑μ s ≠ ⊤) c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p) (hg : Memℒp (↑g) p),
    Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
c : E
s : Set α
hs : MeasurableSet s
hf : Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p
hc : c = 0
⊢ ↑(toLp (SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) hf) =
    ↑(indicatorConst p (_ : MeasurableSet ∅) (_ : ↑↑μ ∅ ≠ ⊤) 0)
case h.e'_1
α : Type u_1
β : Type ?u.1629871
ι : Type ?u.1629874
E : Type u_2
F : Type ?u.1629880
𝕜 : Type ?u.1629883
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : { x // x ∈ simpleFunc E p μ } → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤), P (indicatorConst p hs (_ : ↑↑μ s ≠ ⊤) c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p) (hg : Memℒp (↑g) p),
    Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
c : E
s : Set α
hs : MeasurableSet s
hf : Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p
hc : c = 0
⊢ toLp (SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) hf =
    indicatorConst p (_ : MeasurableSet ∅) (_ : ↑↑μ ∅ ≠ ⊤) 0
ext1
no goals
case h.e'_1.a
α : Type u_1
β : Type ?u.1629871
ι : Type ?u.1629874
E : Type u_2
F : Type ?u.1629880
𝕜 : Type ?u.1629883
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : { x // x ∈ simpleFunc E p μ } → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤), P (indicatorConst p hs (_ : ↑↑μ s ≠ ⊤) c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p) (hg : Memℒp (↑g) p),
    Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
c : E
s : Set α
hs : MeasurableSet s
hf : Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p
hc : c = 0
⊢ ↑(toLp (SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) hf) =
    ↑(indicatorConst p (_ : MeasurableSet ∅) (_ : ↑↑μ ∅ ≠ ⊤) 0)
simp [hc]
no goals
α : Type u_1
β : Type ?u.1629871
ι : Type ?u.1629874
E : Type u_2
F : Type ?u.1629880
𝕜 : Type ?u.1629883
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : { x // x ∈ simpleFunc E p μ } → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤), P (indicatorConst p hs (_ : ↑↑μ s ≠ ⊤) c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p) (hg : Memℒp (↑g) p),
    Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
c : E
s : Set α
hs : MeasurableSet s
hf : Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p
hc : c = 0
⊢ ↑↑μ ∅ < ⊤
simp
case h_add
α : Type u_1
β : Type ?u.1629871
ι : Type ?u.1629874
E : Type u_2
F : Type ?u.1629880
𝕜 : Type ?u.1629883
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : { x // x ∈ simpleFunc E p μ } → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤), P (indicatorConst p hs (_ : ↑↑μ s ≠ ⊤) c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p) (hg : Memℒp (↑g) p),
    Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
f g : α →ₛ E
hfg : Disjoint (support ↑f) (support ↑g)
hf : ∀ (hf : Memℒp (↑f) p), P (toLp f hf)
hg : ∀ (hf : Memℒp (↑g) p), P (toLp g hf)
hfg' : Memℒp (↑(f + g)) p
⊢ P (toLp (f + g) hfg')
case h_add
α : Type u_1
β : Type ?u.1629871
ι : Type ?u.1629874
E : Type u_2
F : Type ?u.1629880
𝕜 : Type ?u.1629883
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : { x // x ∈ simpleFunc E p μ } → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤), P (indicatorConst p hs (_ : ↑↑μ s ≠ ⊤) c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p) (hg : Memℒp (↑g) p),
    Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
⊢ ∀ ⦃f g : α →ₛ E⦄,
    Disjoint (support ↑f) (support ↑g) →
      (∀ (hf : Memℒp (↑f) p), P (toLp f hf)) →
        (∀ (hf : Memℒp (↑g) p), P (toLp g hf)) → ∀ (hf : Memℒp (↑(f + g)) p), P (toLp (f + g) hf)
intro f g hfg hf hg hfg'
case h_add.intro
α : Type u_1
β : Type ?u.1629871
ι : Type ?u.1629874
E : Type u_2
F : Type ?u.1629880
𝕜 : Type ?u.1629883
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : { x // x ∈ simpleFunc E p μ } → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤), P (indicatorConst p hs (_ : ↑↑μ s ≠ ⊤) c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p) (hg : Memℒp (↑g) p),
    Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
f g : α →ₛ E
hfg : Disjoint (support ↑f) (support ↑g)
hf : ∀ (hf : Memℒp (↑f) p), P (toLp f hf)
hg : ∀ (hf : Memℒp (↑g) p), P (toLp g hf)
hfg' : Memℒp (↑(f + g)) p
hf' : Memℒp (↑f) p
hg' : Memℒp (↑g) p
⊢ P (toLp (f + g) hfg')
case h_add
α : Type u_1
β : Type ?u.1629871
ι : Type ?u.1629874
E : Type u_2
F : Type ?u.1629880
𝕜 : Type ?u.1629883
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : { x // x ∈ simpleFunc E p μ } → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤), P (indicatorConst p hs (_ : ↑↑μ s ≠ ⊤) c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p) (hg : Memℒp (↑g) p),
    Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
f g : α →ₛ E
hfg : Disjoint (support ↑f) (support ↑g)
hf : ∀ (hf : Memℒp (↑f) p), P (toLp f hf)
hg : ∀ (hf : Memℒp (↑g) p), P (toLp g hf)
hfg' : Memℒp (↑(f + g)) p
⊢ P (toLp (f + g) hfg')
obtain ⟨hf', hg'⟩ : Memℒp f p μ ∧ Memℒp g p μ :=
  (memℒp_add_of_disjoint hfg f.stronglyMeasurable g.stronglyMeasurable).mp hfg'
no goals
case h_add.intro
α : Type u_1
β : Type ?u.1629871
ι : Type ?u.1629874
E : Type u_2
F : Type ?u.1629880
𝕜 : Type ?u.1629883
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
P : { x // x ∈ simpleFunc E p μ } → Prop
h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤), P (indicatorConst p hs (_ : ↑↑μ s ≠ ⊤) c)
h_add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p) (hg : Memℒp (↑g) p),
    Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)
f g : α →ₛ E
hfg : Disjoint (support ↑f) (support ↑g)
hf : ∀ (hf : Memℒp (↑f) p), P (toLp f hf)
hg : ∀ (hf : Memℒp (↑g) p), P (toLp g hf)
hfg' : Memℒp (↑(f + g)) p
hf' : Memℒp (↑f) p
hg' : Memℒp (↑g) p
⊢ P (toLp (f + g) hfg')
exact h_add hf' hg' hfg (hf hf') (hg hg')