α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
⊢ ↑↑μ (↑f ⁻¹' {y}) < ⊤
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
⊢ ↑↑μ (↑f ⁻¹' {y}) < ⊤
have hp_pos_real : 0 < p.toReal := ENNReal.toReal_pos hp_pos hp_ne_top
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hf_snorm : snorm (↑f) p μ < ⊤
⊢ ↑↑μ (↑f ⁻¹' {y}) < ⊤
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
⊢ ↑↑μ (↑f ⁻¹' {y}) < ⊤
have hf_snorm := Memℒp.snorm_lt_top hf
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hf_snorm : ∀ (a : E), a ∈ SimpleFunc.range f → ↑‖a‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {a}) < ⊤
⊢ ↑↑μ (↑f ⁻¹' {y}) < ⊤
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hf_snorm : snorm (↑f) p μ < ⊤
⊢ ↑↑μ (↑f ⁻¹' {y}) < ⊤
rw [snorm_eq_snorm' hp_pos hp_ne_top, f.snorm'_eq, ←
  @ENNReal.lt_rpow_one_div_iff _ _ (1 / p.toReal) (by simp [hp_pos_real]),
  @ENNReal.top_rpow_of_pos (1 / (1 / p.toReal)) (by simp [hp_pos_real]),
  ENNReal.sum_lt_top_iff] at hf_snorm
case pos
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hf_snorm : ∀ (a : E), a ∈ SimpleFunc.range f → ↑‖a‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {a}) < ⊤
hyf : y ∈ SimpleFunc.range f
⊢ ↑↑μ (↑f ⁻¹' {y}) < ⊤

case neg
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hf_snorm : ∀ (a : E), a ∈ SimpleFunc.range f → ↑‖a‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {a}) < ⊤
hyf : ¬y ∈ SimpleFunc.range f
⊢ ↑↑μ (↑f ⁻¹' {y}) < ⊤
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hf_snorm : ∀ (a : E), a ∈ SimpleFunc.range f → ↑‖a‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {a}) < ⊤
⊢ ↑↑μ (↑f ⁻¹' {y}) < ⊤
by_cases hyf : y ∈ f.range
case neg
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hf_snorm : ∀ (a : E), a ∈ SimpleFunc.range f → ↑‖a‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {a}) < ⊤
hyf : ¬y ∈ SimpleFunc.range f
⊢ ↑↑μ (↑f ⁻¹' {y}) < ⊤

case pos
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hf_snorm : ∀ (a : E), a ∈ SimpleFunc.range f → ↑‖a‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {a}) < ⊤
hyf : y ∈ SimpleFunc.range f
⊢ ↑↑μ (↑f ⁻¹' {y}) < ⊤
case pos
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hf_snorm : ∀ (a : E), a ∈ SimpleFunc.range f → ↑‖a‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {a}) < ⊤
hyf : y ∈ SimpleFunc.range f
⊢ ↑↑μ (↑f ⁻¹' {y}) < ⊤

case neg
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hf_snorm : ∀ (a : E), a ∈ SimpleFunc.range f → ↑‖a‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {a}) < ⊤
hyf : ¬y ∈ SimpleFunc.range f
⊢ ↑↑μ (↑f ⁻¹' {y}) < ⊤
swap
case pos
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hyf : y ∈ SimpleFunc.range f
hf_snorm : ↑‖y‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {y}) < ⊤
⊢ ↑↑μ (↑f ⁻¹' {y}) < ⊤
case pos
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hf_snorm : ∀ (a : E), a ∈ SimpleFunc.range f → ↑‖a‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {a}) < ⊤
hyf : y ∈ SimpleFunc.range f
⊢ ↑↑μ (↑f ⁻¹' {y}) < ⊤
specialize hf_snorm y hyf
case pos
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hyf : y ∈ SimpleFunc.range f
hf_snorm : ↑‖y‖₊ ^ ENNReal.toReal p < ⊤ ∧ ↑↑μ (↑f ⁻¹' {y}) < ⊤ ∨ ↑‖y‖₊ ^ ENNReal.toReal p = 0 ∨ ↑↑μ (↑f ⁻¹' {y}) = 0
⊢ ↑↑μ (↑f ⁻¹' {y}) < ⊤
case pos
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hyf : y ∈ SimpleFunc.range f
hf_snorm : ↑‖y‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {y}) < ⊤
⊢ ↑↑μ (↑f ⁻¹' {y}) < ⊤
rw [ENNReal.mul_lt_top_iff] at hf_snorm
no goals
case pos
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hyf : y ∈ SimpleFunc.range f
hf_snorm : ↑‖y‖₊ ^ ENNReal.toReal p < ⊤ ∧ ↑↑μ (↑f ⁻¹' {y}) < ⊤ ∨ ↑‖y‖₊ ^ ENNReal.toReal p = 0 ∨ ↑↑μ (↑f ⁻¹' {y}) = 0
⊢ ↑↑μ (↑f ⁻¹' {y}) < ⊤
cases hf_snorm with
| inl hf_snorm => exact hf_snorm.2
| inr hf_snorm =>
  cases hf_snorm with
  | inl hf_snorm =>
    refine' absurd _ hy_ne
    simpa [hp_pos_real] using hf_snorm
  | inr hf_snorm => simp [hf_snorm]
no goals
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hf_snorm : (∑ y in SimpleFunc.range f, ↑‖y‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {y})) ^ (1 / ENNReal.toReal p) < ⊤
⊢ 0 < 1 / ENNReal.toReal p
simp [hp_pos_real]
no goals
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hf_snorm : ∑ y in SimpleFunc.range f, ↑‖y‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {y}) < ⊤ ^ (1 / (1 / ENNReal.toReal p))
⊢ 0 < 1 / (1 / ENNReal.toReal p)
simp [hp_pos_real]
case neg
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hf_snorm : ∀ (a : E), a ∈ SimpleFunc.range f → ↑‖a‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {a}) < ⊤
hyf : ¬y ∈ SimpleFunc.range f
h_empty : ↑f ⁻¹' {y} = ∅
⊢ ↑↑μ (↑f ⁻¹' {y}) < ⊤

case h_empty
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hf_snorm : ∀ (a : E), a ∈ SimpleFunc.range f → ↑‖a‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {a}) < ⊤
hyf : ¬y ∈ SimpleFunc.range f
⊢ ↑f ⁻¹' {y} = ∅
case neg
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hf_snorm : ∀ (a : E), a ∈ SimpleFunc.range f → ↑‖a‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {a}) < ⊤
hyf : ¬y ∈ SimpleFunc.range f
⊢ ↑↑μ (↑f ⁻¹' {y}) < ⊤
suffices h_empty : f ⁻¹' {y} = ∅
case h_empty.h
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hf_snorm : ∀ (a : E), a ∈ SimpleFunc.range f → ↑‖a‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {a}) < ⊤
hyf : ¬y ∈ SimpleFunc.range f
x : α
⊢ x ∈ ↑f ⁻¹' {y} ↔ x ∈ ∅
case h_empty
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hf_snorm : ∀ (a : E), a ∈ SimpleFunc.range f → ↑‖a‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {a}) < ⊤
hyf : ¬y ∈ SimpleFunc.range f
⊢ ↑f ⁻¹' {y} = ∅
ext1 x
case h_empty.h
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hf_snorm : ∀ (a : E), a ∈ SimpleFunc.range f → ↑‖a‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {a}) < ⊤
hyf : ¬y ∈ SimpleFunc.range f
x : α
⊢ ¬↑f x = y
case h_empty.h
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hf_snorm : ∀ (a : E), a ∈ SimpleFunc.range f → ↑‖a‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {a}) < ⊤
hyf : ¬y ∈ SimpleFunc.range f
x : α
⊢ x ∈ ↑f ⁻¹' {y} ↔ x ∈ ∅
rw [Set.mem_preimage, Set.mem_singleton_iff, mem_empty_iff_false, iff_false_iff]
case h_empty.h
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hf_snorm : ∀ (a : E), a ∈ SimpleFunc.range f → ↑‖a‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {a}) < ⊤
hyf : ¬y ∈ SimpleFunc.range f
x : α
hxy : ↑f x = y
⊢ y ∈ SimpleFunc.range f
case h_empty.h
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hf_snorm : ∀ (a : E), a ∈ SimpleFunc.range f → ↑‖a‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {a}) < ⊤
hyf : ¬y ∈ SimpleFunc.range f
x : α
⊢ ¬↑f x = y
refine' fun hxy => hyf _
case h_empty.h
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hf_snorm : ∀ (a : E), a ∈ SimpleFunc.range f → ↑‖a‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {a}) < ⊤
hyf : ¬y ∈ SimpleFunc.range f
x : α
hxy : ↑f x = y
⊢ ∃ y_1, ↑f y_1 = y
case h_empty.h
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hf_snorm : ∀ (a : E), a ∈ SimpleFunc.range f → ↑‖a‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {a}) < ⊤
hyf : ¬y ∈ SimpleFunc.range f
x : α
hxy : ↑f x = y
⊢ y ∈ SimpleFunc.range f
rw [mem_range, Set.mem_range]
no goals
case h_empty.h
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hf_snorm : ∀ (a : E), a ∈ SimpleFunc.range f → ↑‖a‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {a}) < ⊤
hyf : ¬y ∈ SimpleFunc.range f
x : α
hxy : ↑f x = y
⊢ ∃ y_1, ↑f y_1 = y
exact ⟨x, hxy⟩
case neg
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hf_snorm : ∀ (a : E), a ∈ SimpleFunc.range f → ↑‖a‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {a}) < ⊤
hyf : ¬y ∈ SimpleFunc.range f
h_empty : ↑f ⁻¹' {y} = ∅
⊢ 0 < ⊤
case neg
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hf_snorm : ∀ (a : E), a ∈ SimpleFunc.range f → ↑‖a‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {a}) < ⊤
hyf : ¬y ∈ SimpleFunc.range f
h_empty : ↑f ⁻¹' {y} = ∅
⊢ ↑↑μ (↑f ⁻¹' {y}) < ⊤
rw [h_empty, measure_empty]
no goals
case neg
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hf_snorm : ∀ (a : E), a ∈ SimpleFunc.range f → ↑‖a‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {a}) < ⊤
hyf : ¬y ∈ SimpleFunc.range f
h_empty : ↑f ⁻¹' {y} = ∅
⊢ 0 < ⊤
exact ENNReal.coe_lt_top
no goals
case pos.inl
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hyf : y ∈ SimpleFunc.range f
hf_snorm : ↑‖y‖₊ ^ ENNReal.toReal p < ⊤ ∧ ↑↑μ (↑f ⁻¹' {y}) < ⊤
⊢ ↑↑μ (↑f ⁻¹' {y}) < ⊤
exact hf_snorm.2
no goals
case pos.inr
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hyf : y ∈ SimpleFunc.range f
hf_snorm : ↑‖y‖₊ ^ ENNReal.toReal p = 0 ∨ ↑↑μ (↑f ⁻¹' {y}) = 0
⊢ ↑↑μ (↑f ⁻¹' {y}) < ⊤
cases hf_snorm with
| inl hf_snorm =>
  refine' absurd _ hy_ne
  simpa [hp_pos_real] using hf_snorm
| inr hf_snorm => simp [hf_snorm]
case pos.inr.inl
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hyf : y ∈ SimpleFunc.range f
hf_snorm : ↑‖y‖₊ ^ ENNReal.toReal p = 0
⊢ y = 0
case pos.inr.inl
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hyf : y ∈ SimpleFunc.range f
hf_snorm : ↑‖y‖₊ ^ ENNReal.toReal p = 0
⊢ ↑↑μ (↑f ⁻¹' {y}) < ⊤
refine' absurd _ hy_ne
no goals
case pos.inr.inl
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hyf : y ∈ SimpleFunc.range f
hf_snorm : ↑‖y‖₊ ^ ENNReal.toReal p = 0
⊢ y = 0
simpa [hp_pos_real] using hf_snorm
no goals
case pos.inr.inr
α : Type u_1
β : Type ?u.1417450
ι : Type ?u.1417453
E : Type u_2
F : Type ?u.1417459
𝕜 : Type ?u.1417462
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : Memℒp (↑f) p
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < ENNReal.toReal p
hyf : y ∈ SimpleFunc.range f
hf_snorm : ↑↑μ (↑f ⁻¹' {y}) = 0
⊢ ↑↑μ (↑f ⁻¹' {y}) < ⊤
simp [hf_snorm]