α : Type u_1
E : Type u_2
F : Type ?u.2314890
G : Type ?u.2314893
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) = 0 ∧ 0 < 1 / q ∨ (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) = ⊤ ∧ 1 / q < 0
⊢ f =ᵐ[μ] 0
α : Type u_1
E : Type u_2
F : Type ?u.2314890
G : Type ?u.2314893
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : snorm' f q μ = 0
⊢ f =ᵐ[μ] 0
rw [snorm', ENNReal.rpow_eq_zero_iff] at h
no goals
α : Type u_1
E : Type u_2
F : Type ?u.2314890
G : Type ?u.2314893
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) = 0 ∧ 0 < 1 / q ∨ (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) = ⊤ ∧ 1 / q < 0
⊢ f =ᵐ[μ] 0
cases h with
| inl h =>
  rw [lintegral_eq_zero_iff' (hf.ennnorm.pow_const q)] at h
  refine' h.left.mono fun x hx => _
  rw [Pi.zero_apply, ENNReal.rpow_eq_zero_iff] at hx
  cases hx with
  | inl hx =>
    cases' hx with hx _
    rwa [← ENNReal.coe_zero, ENNReal.coe_eq_coe, nnnorm_eq_zero] at hx
  | inr hx =>
    exact absurd hx.left ENNReal.coe_ne_top
| inr h =>
  exfalso
  rw [one_div, inv_lt_zero] at h
  exact hq0.not_lt h.right
case inl
α : Type u_1
E : Type u_2
F : Type ?u.2314890
G : Type ?u.2314893
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (fun x => ↑‖f x‖₊ ^ q) =ᵐ[μ] 0 ∧ 0 < 1 / q
⊢ f =ᵐ[μ] 0
case inl
α : Type u_1
E : Type u_2
F : Type ?u.2314890
G : Type ?u.2314893
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) = 0 ∧ 0 < 1 / q
⊢ f =ᵐ[μ] 0
rw [lintegral_eq_zero_iff' (hf.ennnorm.pow_const q)] at h
case inl
α : Type u_1
E : Type u_2
F : Type ?u.2314890
G : Type ?u.2314893
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (fun x => ↑‖f x‖₊ ^ q) =ᵐ[μ] 0 ∧ 0 < 1 / q
x : α
hx : (fun x => ↑‖f x‖₊ ^ q) x = OfNat.ofNat 0 x
⊢ f x = OfNat.ofNat 0 x
case inl
α : Type u_1
E : Type u_2
F : Type ?u.2314890
G : Type ?u.2314893
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (fun x => ↑‖f x‖₊ ^ q) =ᵐ[μ] 0 ∧ 0 < 1 / q
⊢ f =ᵐ[μ] 0
refine' h.left.mono fun x hx => _
case inl
α : Type u_1
E : Type u_2
F : Type ?u.2314890
G : Type ?u.2314893
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (fun x => ↑‖f x‖₊ ^ q) =ᵐ[μ] 0 ∧ 0 < 1 / q
x : α
hx : ↑‖f x‖₊ = 0 ∧ 0 < q ∨ ↑‖f x‖₊ = ⊤ ∧ q < 0
⊢ f x = OfNat.ofNat 0 x
case inl
α : Type u_1
E : Type u_2
F : Type ?u.2314890
G : Type ?u.2314893
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (fun x => ↑‖f x‖₊ ^ q) =ᵐ[μ] 0 ∧ 0 < 1 / q
x : α
hx : (fun x => ↑‖f x‖₊ ^ q) x = OfNat.ofNat 0 x
⊢ f x = OfNat.ofNat 0 x
rw [Pi.zero_apply, ENNReal.rpow_eq_zero_iff] at hx
no goals
case inl
α : Type u_1
E : Type u_2
F : Type ?u.2314890
G : Type ?u.2314893
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (fun x => ↑‖f x‖₊ ^ q) =ᵐ[μ] 0 ∧ 0 < 1 / q
x : α
hx : ↑‖f x‖₊ = 0 ∧ 0 < q ∨ ↑‖f x‖₊ = ⊤ ∧ q < 0
⊢ f x = OfNat.ofNat 0 x
cases hx with
| inl hx =>
  cases' hx with hx _
  rwa [← ENNReal.coe_zero, ENNReal.coe_eq_coe, nnnorm_eq_zero] at hx
| inr hx =>
  exact absurd hx.left ENNReal.coe_ne_top
case inl.inl.intro
α : Type u_1
E : Type u_2
F : Type ?u.2314890
G : Type ?u.2314893
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (fun x => ↑‖f x‖₊ ^ q) =ᵐ[μ] 0 ∧ 0 < 1 / q
x : α
hx : ↑‖f x‖₊ = 0
right✝ : 0 < q
⊢ f x = OfNat.ofNat 0 x
case inl.inl
α : Type u_1
E : Type u_2
F : Type ?u.2314890
G : Type ?u.2314893
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (fun x => ↑‖f x‖₊ ^ q) =ᵐ[μ] 0 ∧ 0 < 1 / q
x : α
hx : ↑‖f x‖₊ = 0 ∧ 0 < q
⊢ f x = OfNat.ofNat 0 x
cases' hx with hx _
no goals
case inl.inl.intro
α : Type u_1
E : Type u_2
F : Type ?u.2314890
G : Type ?u.2314893
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (fun x => ↑‖f x‖₊ ^ q) =ᵐ[μ] 0 ∧ 0 < 1 / q
x : α
hx : ↑‖f x‖₊ = 0
right✝ : 0 < q
⊢ f x = OfNat.ofNat 0 x
rwa [← ENNReal.coe_zero, ENNReal.coe_eq_coe, nnnorm_eq_zero] at hx
no goals
case inl.inr
α : Type u_1
E : Type u_2
F : Type ?u.2314890
G : Type ?u.2314893
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (fun x => ↑‖f x‖₊ ^ q) =ᵐ[μ] 0 ∧ 0 < 1 / q
x : α
hx : ↑‖f x‖₊ = ⊤ ∧ q < 0
⊢ f x = OfNat.ofNat 0 x
exact absurd hx.left ENNReal.coe_ne_top
case inr.h
α : Type u_1
E : Type u_2
F : Type ?u.2314890
G : Type ?u.2314893
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) = ⊤ ∧ 1 / q < 0
⊢ False
case inr
α : Type u_1
E : Type u_2
F : Type ?u.2314890
G : Type ?u.2314893
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) = ⊤ ∧ 1 / q < 0
⊢ f =ᵐ[μ] 0
exfalso
case inr.h
α : Type u_1
E : Type u_2
F : Type ?u.2314890
G : Type ?u.2314893
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) = ⊤ ∧ q < 0
⊢ False
case inr.h
α : Type u_1
E : Type u_2
F : Type ?u.2314890
G : Type ?u.2314893
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) = ⊤ ∧ 1 / q < 0
⊢ False
rw [one_div, inv_lt_zero] at h
no goals
case inr.h
α : Type u_1
E : Type u_2
F : Type ?u.2314890
G : Type ?u.2314893
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → E
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) = ⊤ ∧ q < 0
⊢ False
exact hq0.not_lt h.right