mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x✝ : MeasurableSpace α
inst✝ : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s : Finset ι
hf : ∀ i ∈ ∅, MemLp (f i) (p i) μ
hμ : μ = 0
⊢ MemLp (∏ i ∈ ∅, f i) (∑ i ∈ ∅, (p i)⁻¹)⁻¹ μ

pp: case neg
ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x✝ : MeasurableSpace α
inst✝ : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s : Finset ι
hf : ∀ i ∈ ∅, MemLp (f i) (p i) μ
hμ : ¬μ = 0
⊢ MemLp (∏ i ∈ ∅, f i) (∑ i ∈ ∅, (p i)⁻¹)⁻¹ μ

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x✝ : MeasurableSpace α
inst✝ : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s : Finset ι
hf : ∀ i ∈ ∅, MemLp (f i) (p i) μ
hμ : μ = 0
⊢ MemLp (∏ i ∈ ∅, f i) (∑ i ∈ ∅, (p i)⁻¹)⁻¹ μ

case neg
ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x✝ : MeasurableSpace α
inst✝ : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s : Finset ι
hf : ∀ i ∈ ∅, MemLp (f i) (p i) μ
hμ : ¬μ = 0
⊢ MemLp (∏ i ∈ ∅, f i) (∑ i ∈ ∅, (p i)⁻¹)⁻¹ μ
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)

Tactic:
have hp_pos : 0 < p := lt_of_lt_of_le zero_lt_one hp1
  obtain hf_top | hf_top := eq_top_or_lt_top (∫⁻ a, f a ^ p ∂μ)
  · simp [hf_top, hp_pos]
  obtain hg_top | hg_top := eq_top_or_lt_top (∫⁻ a, g a ^ p ∂μ)
  · simp [hg_top, hp_pos]
  by_cases h1 : p = 1
  · refine le_of_eq ?_
    simp_rw [h1, one_div_one, ENNReal.rpow_one]
    exact lintegral_add_left' hf _
  have hp1_lt : 1 < p := by
    refine lt_of_le_of_ne hp1 ?_
    symm
    exact h1
  have hpq := Real.HolderConjugate.conjExponent hp1_lt
  by_cases h0 : (∫⁻ a, (f + g) a ^ p ∂μ) = 0
  · rw [h0, @ENNReal.zero_rpow_of_pos (1 / p) (by simp [lt_of_lt_of_le zero_lt_one hp1])]
    exact zero_le
  exact lintegral_Lp_add_le_aux hpq hf hg h0
    (lintegral_rpow_add_lt_top_of_lintegral_rpow_lt_top hf hf_top hg_top hp1).ne

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case refine_1
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
this : (∑ i ∈ s, (|f i| + |g i|) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) + (∑ i ∈ s, |g i| ^ p) ^ (1 / p)
⊢ 0 ≤ ∑ i ∈ s, |f i + g i| ^ p

pp: case refine_2
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
this : (∑ i ∈ s, (|f i| + |g i|) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) + (∑ i ∈ s, |g i| ^ p) ^ (1 / p)
i : ι
x✝ : i ∈ s
⊢ |f i + g i| ^ p ≤ (|f i| + |g i|) ^ p

pp: case refine_3
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
this : (∑ i ∈ s, (|f i| + |g i|) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) + (∑ i ∈ s, |g i| ^ p) ^ (1 / p)
⊢ 0 ≤ 1 / p

Tactic:
<;>

Goal state after:
case refine_1
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
this : (∑ i ∈ s, (|f i| + |g i|) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) + (∑ i ∈ s, |g i| ^ p) ^ (1 / p)
⊢ 0 ≤ ∑ i ∈ s, |f i + g i| ^ p

case refine_2
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
this : (∑ i ∈ s, (|f i| + |g i|) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) + (∑ i ∈ s, |g i| ^ p) ^ (1 / p)
i : ι
x✝ : i ∈ s
⊢ |f i + g i| ^ p ≤ (|f i| + |g i|) ^ p

case refine_3
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
this : (∑ i ∈ s, (|f i| + |g i|) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) + (∑ i ∈ s, |g i| ^ p) ^ (1 / p)
⊢ 0 ≤ 1 / p
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_5
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∑ i ∈ s, f i ^ p = ∑ i ∈ s, |f i| ^ p

pp: case e'_6
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∑ i ∈ s, g i ^ q = ∑ i ∈ s, |g i| ^ q

Tactic:
<;>

Goal state after:
case e'_5
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∑ i ∈ s, f i ^ p = ∑ i ∈ s, |f i| ^ p

case e'_6
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∑ i ∈ s, g i ^ q = ∑ i ∈ s, |g i| ^ q
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_5
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∀ x ∈ s, f x ^ p = |f x| ^ p

pp: case e'_6
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∀ x ∈ s, g x ^ q = |g x| ^ q

Tactic:
<;>

Goal state after:
case e'_5
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∀ x ∈ s, f x ^ p = |f x| ^ p

case e'_6
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∀ x ∈ s, g x ^ q = |g x| ^ q
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_5
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
i : ι
hi : i ∈ s
⊢ f i ^ p = |f i| ^ p

pp: case e'_6
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
i : ι
hi : i ∈ s
⊢ g i ^ q = |g i| ^ q

Tactic:
<;>

Goal state after:
case e'_5
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
i : ι
hi : i ∈ s
⊢ f i ^ p = |f i| ^ p

case e'_6
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
i : ι
hi : i ∈ s
⊢ g i ^ q = |g i| ^ q
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: case pos
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
l : Filter ι
F : Type u_5
inst✝¹ : PseudoEMetricSpace F
inst✝ : Zero F
f : ι → α → F
g : α → F
hg : TendstoInMeasure μ f l g
s : Set α
ε : ℝ≥0∞
hε : 0 < ε
n : ι
x : α
hx : x ∈ {x | ε ≤ edist ((fun i ↦ s.indicator (f i)) n x) (s.indicator g x)}
h✝ : x ∈ s
⊢ x ∈ {x | ε ≤ edist (f n x) (g x)}

pp: case neg
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
l : Filter ι
F : Type u_5
inst✝¹ : PseudoEMetricSpace F
inst✝ : Zero F
f : ι → α → F
g : α → F
hg : TendstoInMeasure μ f l g
s : Set α
ε : ℝ≥0∞
hε : 0 < ε
n : ι
x : α
hx : x ∈ {x | ε ≤ edist ((fun i ↦ s.indicator (f i)) n x) (s.indicator g x)}
h✝ : x ∉ s
⊢ x ∈ {x | ε ≤ edist (f n x) (g x)}

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
l : Filter ι
F : Type u_5
inst✝¹ : PseudoEMetricSpace F
inst✝ : Zero F
f : ι → α → F
g : α → F
hg : TendstoInMeasure μ f l g
s : Set α
ε : ℝ≥0∞
hε : 0 < ε
n : ι
x : α
hx : x ∈ {x | ε ≤ edist ((fun i ↦ s.indicator (f i)) n x) (s.indicator g x)}
h✝ : x ∈ s
⊢ x ∈ {x | ε ≤ edist (f n x) (g x)}

case neg
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
l : Filter ι
F : Type u_5
inst✝¹ : PseudoEMetricSpace F
inst✝ : Zero F
f : ι → α → F
g : α → F
hg : TendstoInMeasure μ f l g
s : Set α
ε : ℝ≥0∞
hε : 0 < ε
n : ι
x : α
hx : x ∈ {x | ε ≤ edist ((fun i ↦ s.indicator (f i)) n x) (s.indicator g x)}
h✝ : x ∉ s
⊢ x ∈ {x | ε ≤ edist (f n x) (g x)}
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_3
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ∑ i ∈ s, f i = ∑ i ∈ s, |f i|

pp: case e'_4
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ∑ i ∈ s, f i ^ p = ∑ i ∈ s, |f i| ^ p

Tactic:
<;>

Goal state after:
case e'_3
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ∑ i ∈ s, f i = ∑ i ∈ s, |f i|

case e'_4
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ∑ i ∈ s, f i ^ p = ∑ i ∈ s, |f i| ^ p
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_3
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ∀ x ∈ s, f x = |f x|

pp: case e'_4
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ∀ x ∈ s, f x ^ p = |f x| ^ p

Tactic:
<;>

Goal state after:
case e'_3
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ∀ x ∈ s, f x = |f x|

case e'_4
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ∀ x ∈ s, f x ^ p = |f x| ^ p
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_3
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
i : ι
hi : i ∈ s
⊢ f i = |f i|

pp: case e'_4
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
i : ι
hi : i ∈ s
⊢ f i ^ p = |f i| ^ p

Tactic:
<;>

Goal state after:
case e'_3
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
i : ι
hi : i ∈ s
⊢ f i = |f i|

case e'_4
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
i : ι
hi : i ∈ s
⊢ f i ^ p = |f i| ^ p
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_3
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∑ i ∈ s, (f i + g i) ^ p = ∑ i ∈ s, |f i + g i| ^ p

pp: case e'_4.e'_5.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∑ i ∈ s, f i ^ p = ∑ i ∈ s, |f i| ^ p

pp: case e'_4.e'_6.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∑ i ∈ s, g i ^ p = ∑ i ∈ s, |g i| ^ p

Tactic:
<;>

Goal state after:
case e'_3
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∑ i ∈ s, (f i + g i) ^ p = ∑ i ∈ s, |f i + g i| ^ p

case e'_4.e'_5.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∑ i ∈ s, f i ^ p = ∑ i ∈ s, |f i| ^ p

case e'_4.e'_6.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∑ i ∈ s, g i ^ p = ∑ i ∈ s, |g i| ^ p
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_3
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∀ x ∈ s, (f x + g x) ^ p = |f x + g x| ^ p

pp: case e'_4.e'_5.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∀ x ∈ s, f x ^ p = |f x| ^ p

pp: case e'_4.e'_6.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∀ x ∈ s, g x ^ p = |g x| ^ p

Tactic:
<;>

Goal state after:
case e'_3
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∀ x ∈ s, (f x + g x) ^ p = |f x + g x| ^ p

case e'_4.e'_5.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∀ x ∈ s, f x ^ p = |f x| ^ p

case e'_4.e'_6.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∀ x ∈ s, g x ^ p = |g x| ^ p
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_3
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
i : ι
hi : i ∈ s
⊢ (f i + g i) ^ p = |f i + g i| ^ p

pp: case e'_4.e'_5.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
i : ι
hi : i ∈ s
⊢ f i ^ p = |f i| ^ p

pp: case e'_4.e'_6.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
i : ι
hi : i ∈ s
⊢ g i ^ p = |g i| ^ p

Tactic:
<;>

Goal state after:
case e'_3
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
i : ι
hi : i ∈ s
⊢ (f i + g i) ^ p = |f i + g i| ^ p

case e'_4.e'_5.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
i : ι
hi : i ∈ s
⊢ f i ^ p = |f i| ^ p

case e'_4.e'_6.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
i : ι
hi : i ∈ s
⊢ g i ^ p = |g i| ^ p
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inl
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
i : ι
hi : i ∈ s
H : ∀ i ∈ s, f i = 0
⊢ f i * g i = 0

pp: case inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
i : ι
hi : i ∈ s
H : ∀ i ∈ s, g i = 0
⊢ f i * g i = 0

Tactic:
<;>

Goal state after:
case inl
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
i : ι
hi : i ∈ s
H : ∀ i ∈ s, f i = 0
⊢ f i * g i = 0

case inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
i : ι
hi : i ∈ s
H : ∀ i ∈ s, g i = 0
⊢ f i * g i = 0
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case pos.inl
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∑ i ∈ s, f i ^ p) ^ (1 / p) = ∞
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

pp: case pos.inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∑ i ∈ s, g i ^ q) ^ (1 / q) = ∞
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

Tactic:
<;>

Goal state after:
case pos.inl
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∑ i ∈ s, f i ^ p) ^ (1 / p) = ∞
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

case pos.inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∑ i ∈ s, g i ^ q) ^ (1 / q) = ∞
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: case succ
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
k n✝ : ℕ
hn : seqTendstoAeSeq hfg (n✝ + 1) ≤ k
⊢ μ {x | 2⁻¹ ^ (n✝ + 1) ≤ edist (f k x) (g x)} ≤ 2⁻¹ ^ (n✝ + 1)

Tactic:
exact Classical.choose_spec
      (exists_nat_measure_lt_two_inv hfg _) _ (le_trans (le_max_left _ _) hn)

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ i ∈ s, ↑(f i).toNNReal * ↑(g i).toNNReal ≤
    (∑ x ∈ s, ↑(f x).toNNReal ^ p) ^ p⁻¹ * (∑ x ∈ s, ↑(g x).toNNReal ^ q) ^ q⁻¹
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

Tactic:
convert! this using 1 <;> [skip; congr 2]

Goal state after:
case e'_3
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ i ∈ s, ↑(f i).toNNReal * ↑(g i).toNNReal ≤
    (∑ x ∈ s, ↑(f x).toNNReal ^ p) ^ p⁻¹ * (∑ x ∈ s, ↑(g x).toNNReal ^ q) ^ q⁻¹
⊢ ∑ i ∈ s, f i * g i = ∑ i ∈ s, ↑(f i).toNNReal * ↑(g i).toNNReal

case e'_4.e_a.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ i ∈ s, ↑(f i).toNNReal * ↑(g i).toNNReal ≤
    (∑ x ∈ s, ↑(f x).toNNReal ^ p) ^ p⁻¹ * (∑ x ∈ s, ↑(g x).toNNReal ^ q) ^ q⁻¹
⊢ ∑ i ∈ s, f i ^ p = ∑ x ∈ s, ↑(f x).toNNReal ^ p

case e'_4.e_a.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ i ∈ s, ↑(f i).toNNReal * ↑(g i).toNNReal ≤
    (∑ x ∈ s, ↑(f x).toNNReal ^ p) ^ p⁻¹ * (∑ x ∈ s, ↑(g x).toNNReal ^ q) ^ q⁻¹
⊢ 1 / p = p⁻¹

case e'_4.e_a.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ i ∈ s, ↑(f i).toNNReal * ↑(g i).toNNReal ≤
    (∑ x ∈ s, ↑(f x).toNNReal ^ p) ^ p⁻¹ * (∑ x ∈ s, ↑(g x).toNNReal ^ q) ^ q⁻¹
⊢ ∑ i ∈ s, g i ^ q = ∑ x ∈ s, ↑(g x).toNNReal ^ q

case e'_4.e_a.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ i ∈ s, ↑(f i).toNNReal * ↑(g i).toNNReal ≤
    (∑ x ∈ s, ↑(f x).toNNReal ^ p) ^ p⁻¹ * (∑ x ∈ s, ↑(g x).toNNReal ^ q) ^ q⁻¹
⊢ 1 / q = q⁻¹
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_3
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ i ∈ s, ↑(f i).toNNReal * ↑(g i).toNNReal ≤
    (∑ x ∈ s, ↑(f x).toNNReal ^ p) ^ p⁻¹ * (∑ x ∈ s, ↑(g x).toNNReal ^ q) ^ q⁻¹
⊢ ∑ i ∈ s, f i * g i = ∑ i ∈ s, ↑(f i).toNNReal * ↑(g i).toNNReal

pp: case e'_4.e_a.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ i ∈ s, ↑(f i).toNNReal * ↑(g i).toNNReal ≤
    (∑ x ∈ s, ↑(f x).toNNReal ^ p) ^ p⁻¹ * (∑ x ∈ s, ↑(g x).toNNReal ^ q) ^ q⁻¹
⊢ ∑ i ∈ s, f i ^ p = ∑ x ∈ s, ↑(f x).toNNReal ^ p

pp: case e'_4.e_a.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ i ∈ s, ↑(f i).toNNReal * ↑(g i).toNNReal ≤
    (∑ x ∈ s, ↑(f x).toNNReal ^ p) ^ p⁻¹ * (∑ x ∈ s, ↑(g x).toNNReal ^ q) ^ q⁻¹
⊢ ∑ i ∈ s, g i ^ q = ∑ x ∈ s, ↑(g x).toNNReal ^ q

Tactic:
<;>

Goal state after:
case e'_3
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ i ∈ s, ↑(f i).toNNReal * ↑(g i).toNNReal ≤
    (∑ x ∈ s, ↑(f x).toNNReal ^ p) ^ p⁻¹ * (∑ x ∈ s, ↑(g x).toNNReal ^ q) ^ q⁻¹
⊢ ∑ i ∈ s, f i * g i = ∑ i ∈ s, ↑(f i).toNNReal * ↑(g i).toNNReal

case e'_4.e_a.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ i ∈ s, ↑(f i).toNNReal * ↑(g i).toNNReal ≤
    (∑ x ∈ s, ↑(f x).toNNReal ^ p) ^ p⁻¹ * (∑ x ∈ s, ↑(g x).toNNReal ^ q) ^ q⁻¹
⊢ ∑ i ∈ s, f i ^ p = ∑ x ∈ s, ↑(f x).toNNReal ^ p

case e'_4.e_a.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ i ∈ s, ↑(f i).toNNReal * ↑(g i).toNNReal ≤
    (∑ x ∈ s, ↑(f x).toNNReal ^ p) ^ p⁻¹ * (∑ x ∈ s, ↑(g x).toNNReal ^ q) ^ q⁻¹
⊢ ∑ i ∈ s, g i ^ q = ∑ x ∈ s, ↑(g x).toNNReal ^ q
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
⊢ MemLp (fun x ↦ ‖f x‖ ^ q.toReal) (p / q) μ ↔ MemLp f p μ

Tactic:
refine ⟨fun h => ?_, fun h => h.norm_rpow_div q⟩

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (fun x ↦ ‖f x‖ ^ q.toReal) (p / q) μ
⊢ MemLp f p μ
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inl
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
i : ι
hi : i ∈ s
H : ∀ i ∈ s, w i = 0
⊢ w i * f i = 0

pp: case inr
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
i : ι
hi : i ∈ s
H : ∀ i ∈ s, w i = 0 ∨ f i = 0
⊢ w i * f i = 0

Tactic:
<;>

Goal state after:
case inl
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
i : ι
hi : i ∈ s
H : ∀ i ∈ s, w i = 0
⊢ w i * f i = 0

case inr
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
i : ι
hi : i ∈ s
H : ∀ i ∈ s, w i = 0 ∨ f i = 0
⊢ w i * f i = 0
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case neg
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) ≠ 0 ∧ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ ≠ 0
⊢ ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹

Tactic:
by_cases H' : (∑ i ∈ s, w i) ^ (1 - p⁻¹) = ⊤ ∨ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ = ⊤

Goal state after:
case pos
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) ≠ 0 ∧ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ ≠ 0
H' : (∑ i ∈ s, w i) ^ (1 - p⁻¹) = ∞ ∨ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ = ∞
⊢ ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹

case neg
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) ≠ 0 ∧ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ ≠ 0
H' : ¬((∑ i ∈ s, w i) ^ (1 - p⁻¹) = ∞ ∨ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ = ∞)
⊢ ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case pos.inl
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) ≠ 0 ∧ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ ≠ 0
H' : (∑ i ∈ s, w i) ^ (1 - p⁻¹) = ∞
⊢ ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹

pp: case pos.inr
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) ≠ 0 ∧ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ ≠ 0
H' : (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ = ∞
⊢ ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹

Tactic:
<;>

Goal state after:
case pos.inl
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) ≠ 0 ∧ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ ≠ 0
H' : (∑ i ∈ s, w i) ^ (1 - p⁻¹) = ∞
⊢ ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹

case pos.inr
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) ≠ 0 ∧ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ ≠ 0
H' : (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ = ∞
⊢ ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹