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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
s : Set α
f : α → ε
⊢ eLpNormEssSup (s.indicator f) μ ≤ eLpNormEssSup f μ

Tactic:
refine essSup_mono_ae (.of_forall fun x => ?_)

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
s : Set α
f : α → ε
x : α
⊢ (fun x ↦ ‖s.indicator f x‖ₑ) x ≤ (fun x ↦ ‖f x‖ₑ) x
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
s : Set α
f : α → ε
⊢ eLpNormEssSup (s.indicator f) μ ≤ eLpNormEssSup f μ

Tactic:
refine essSup_mono_ae (.of_forall fun x => ?_)
  simp_rw [enorm_indicator_eq_indicator_enorm]
  exact Set.indicator_le_self s _ x

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
s : Set α
c : ε
hμs : μ s ≠ 0
⊢ eLpNormEssSup (s.indicator fun x ↦ c) μ = ‖c‖ₑ

Tactic:
refine le_antisymm (eLpNormEssSup_indicator_const_le s c) ?_

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
s : Set α
c : ε
hμs : μ s ≠ 0
⊢ ‖c‖ₑ ≤ eLpNormEssSup (s.indicator fun x ↦ c) μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:

Tactic:
eLpNorm (s.indicator fun _ => c) p μ ≤ eLpNorm (t.indicator fun _ ↦ c) p μ :=
      eLpNorm_mono_enorm (enorm_indicator_le_of_subset (subset_toMeasurable _ _) _)
    _ = ‖c‖ₑ * μ t ^ (1 / p.toReal) :=
      eLpNorm_indicator_const (measurableSet_toMeasurable ..) hp h'p
    _ = ‖c‖ₑ * μ s ^ (1 / p.toReal) := by rw [measure_toMeasurable]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ≥0∞
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ

Tactic:
by
  by_cases h0 : p = 0
  · simp [h0]
  by_cases h_top : p = ∞
  · rw [h_top]
    exact eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul h
  simp_rw [eLpNorm_eq_eLpNorm' h0 h_top]
  exact eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul h (ENNReal.toReal_pos h0 h_top)

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u
α : ι → Type v
inst✝¹ : Fintype ι
inst✝ : IsEmpty ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
⊢ MeasurePreserving (⇑(MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit)) (Measure.pi μ) (Measure.dirac ())

Tactic:
set e := MeasurableEquiv.ofUniqueOfUnique (∀ i, α i) Unit

Goal state after:
ι : Type u
α : ι → Type v
inst✝¹ : Fintype ι
inst✝ : IsEmpty ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
e : ((i : ι) → α i) ≃ᵐ Unit := MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit
⊢ MeasurePreserving (⇑e) (Measure.pi μ) (Measure.dirac ())
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: ⊢ 1 = 1⁻¹

Tactic:
norm_num

Goal state after:
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: case h0
⊢ 2 ≠ 0

Tactic:
norm_num

Goal state after:
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: case ht
⊢ 2 ≠ ∞

Tactic:
norm_num

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: ⊢ ∀ {x y z : ℝ}, x ∈ Ioi 0 → z ∈ Ioi 0 → x < y → y < z → (log z - log y) / (z - y) < (log y - log x) / (y - x)

Tactic:
intro x y z (hx : 0 < x) (hz : 0 < z) hxy hyz

Goal state after:
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
⊢ (log z - log y) / (z - y) < (log y - log x) / (y - x)
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: ⊢ 2⁻¹ + 2⁻¹ = 1⁻¹

Tactic:
norm_num

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
h : MemLp f p μ
⊢ eLpNorm (fun x ↦ ‖f x‖ₑ) p μ < ∞

Tactic:
by simp_rw [MeasureTheory.eLpNorm_enorm, h.eLpNorm_lt_top]

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case inl
hp : 1 ≤ 1
⊢ ConvexOn ℝ (Ici 0) fun x ↦ x ^ 1

pp: case inr
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ ConvexOn ℝ (Ici 0) fun x ↦ x ^ p

Tactic:
· simpa using! convexOn_id (convex_Ici _)

Goal state after:
case inr
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ ConvexOn ℝ (Ici 0) fun x ↦ x ^ p
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_3
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
this : ∏ x ∈ s, rexp (log (z x) * w x) ≤ ∑ x ∈ s, w x * rexp (log (z x))
i : ι
⊢ i ∈ s → z i ^ w i = rexp (log (z i) * w i)

Tactic:
hi

Goal state after:
case e'_3
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
this : ∏ x ∈ s, rexp (log (z x) * w x) ≤ ∑ x ∈ s, w x * rexp (log (z x))
i : ι
hi : i ∈ s
⊢ z i ^ w i = rexp (log (z i) * w i)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_4
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
this : ∏ x ∈ s, rexp (log (z x) * w x) ≤ ∑ x ∈ s, w x * rexp (log (z x))
i : ι
⊢ i ∈ s → w i * z i = w i * rexp (log (z i))

Tactic:
hi

Goal state after:
case e'_4
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
this : ∏ x ∈ s, rexp (log (z x) * w x) ≤ ∑ x ∈ s, w x * rexp (log (z x))
i : ι
hi : i ∈ s
⊢ w i * z i = w i * rexp (log (z i))
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case hx
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
i : ι
⊢ i ∈ s → 0 ≤ w i * z i ^ p

Tactic:
hi

Goal state after:
case hx
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
i : ι
hi : i ∈ s
⊢ 0 ≤ w i * z i ^ p
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
i : ι
⊢ i ∈ s → 0 ≤ w i * z i

Tactic:
hi

Goal state after:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
i : ι
hi : i ∈ s
⊢ 0 ≤ w i * z i
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
i : ι
⊢ i ∈ s → 0 ≤ w i * z i ^ p

Tactic:
hi

Goal state after:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
i : ι
hi : i ∈ s
⊢ 0 ≤ w i * z i ^ p
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_1.h₁
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
i : ι
⊢ i ∈ s → z i ^ w i = rexp (log (z i) * w i)

Tactic:
hi

Goal state after:
case e'_1.h₁
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
i : ι
hi : i ∈ s
⊢ z i ^ w i = rexp (log (z i) * w i)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_1.h₂
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
i : ι
⊢ i ∈ s → w i * z i = w i * rexp (log (z i))

Tactic:
hi

Goal state after:
case e'_1.h₂
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
i : ι
hi : i ∈ s
⊢ w i * z i = w i * rexp (log (z i))
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : (fun x ↦ f x ^ p) =ᵐ[μ] 0
x : α
⊢ f x ^ p = 0 x → f x = 0 x

Tactic:
Pi.zero_apply,

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : (fun x ↦ f x ^ p) =ᵐ[μ] 0
x : α
⊢ f x ^ p = 0 → f x = 0
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
h_top_rpow_sum : (∑ i ∈ s, w i * z i) ^ p ≠ ∞
a✝ : ∑ i ∈ s, w i * z i ^ p ≠ ∞
h_top : ∀ a ∈ s, w a * z a ≠ ∞
i : ι
⊢ i ∈ s → w i * z i ^ p ≠ ∞

Tactic:
hi

Goal state after:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
h_top_rpow_sum : (∑ i ∈ s, w i * z i) ^ p ≠ ∞
a✝ : ∑ i ∈ s, w i * z i ^ p ≠ ∞
h_top : ∀ a ∈ s, w a * z a ≠ ∞
i : ι
hi : i ∈ s
⊢ w i * z i ^ p ≠ ∞
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
⊢ ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i → ∀ j ∈ s, ∀ k ∈ s, z j = z k

Tactic:
grind [geom_mean_eq_arith_mean_weighted_iff_of_pos' s w z hw hw' hz]

Goal state after:
Module: Mathlib.Analysis.Convex.Mul

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : CommRing 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
n : ℕ
⊢ ConvexOn 𝕜 univ fun x ↦ (x ^ 2) ^ n

Tactic:
refine ConvexOn.pow ⟨convex_univ, fun x _ y _ a b ha hb hab ↦ sub_nonneg.1 ?_⟩
    (fun _ _ ↦ by positivity) _

Goal state after:
𝕜 : Type u_1
inst✝² : CommRing 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
n : ℕ
x : 𝕜
x✝¹ : x ∈ univ
y : 𝕜
x✝ : y ∈ univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ 0 ≤ a • x ^ 2 + b • y ^ 2 - (a • x + b • y) ^ 2
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case neg
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h0 : a ≠ 0 ∧ b ≠ 0
h : a ≠ ∞ ∧ b ≠ ∞
⊢ a.toNNReal * b.toNNReal = a.toNNReal ^ p / p.toNNReal + b.toNNReal ^ q / q.toNNReal ↔
    ↑a.toNNReal = ∞ ∧ ↑b.toNNReal ≠ 0 ∨ ↑a.toNNReal ≠ 0 ∧ ↑b.toNNReal = ∞ ∨ ↑(a.toNNReal ^ p) = ↑(b.toNNReal ^ q)

Tactic:
coe_inj

Goal state after:
case neg
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h0 : a ≠ 0 ∧ b ≠ 0
h : a ≠ ∞ ∧ b ≠ ∞
⊢ a.toNNReal * b.toNNReal = a.toNNReal ^ p / p.toNNReal + b.toNNReal ^ q / q.toNNReal ↔
    ↑a.toNNReal = ∞ ∧ ↑b.toNNReal ≠ 0 ∨ ↑a.toNNReal ≠ 0 ∧ ↑b.toNNReal = ∞ ∨ a.toNNReal ^ p = b.toNNReal ^ q
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

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

Tactic:
refine (ENNReal.lintegral_mul_le_Lp_mul_Lq μ hpq hf (hg.pow_const _)).trans_eq ?_
  simp [← ENNReal.rpow_mul, hpq.sub_one_mul_conj]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: case h₁
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hro_lt : 0 < r
hrp : r < p
hpqr : 1 / r = 1 / p + 1 / q
⊢ ∫⁻ (a : α), ‖b (f a) (g a)‖ₑ ^ r ∂μ ≤ ∫⁻ (a : α), ‖↑c • ‖f a‖ * ‖g a‖‖ₑ ^ r ∂μ

Tactic:
refine lintegral_mono_ae <| h.mono fun a ha ↦ ?_

Goal state after:
case h₁
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p q r : ℝ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hro_lt : 0 < r
hrp : r < p
hpqr : 1 / r = 1 / p + 1 / q
a : α
ha : ‖b (f a) (g a)‖₊ ≤ c * ‖f a‖₊ * ‖g a‖₊
⊢ ‖b (f a) (g a)‖ₑ ^ r ≤ ‖↑c • ‖f a‖ * ‖g a‖‖ₑ ^ r
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inl
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 = p
⊢ (∑ i ∈ s, f i) ^ p ≤ ↑(#s) ^ (p - 1) * ∑ i ∈ s, f i ^ p

pp: case inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ (∑ i ∈ s, f i) ^ p ≤ ↑(#s) ^ (p - 1) * ∑ i ∈ s, f i ^ p

Tactic:
· simp [← hp]

Goal state after:
case inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ (∑ i ∈ s, f i) ^ p ≤ ↑(#s) ^ (p - 1) * ∑ i ∈ s, f i ^ p
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
hpq : p.HolderConjugate p.conjExponent
this :
  IsGreatest ((fun g_1 ↦ ∑ i ∈ s, (f + g) i * g_1 i) '' {g | ∑ i ∈ s, g i ^ p.conjExponent ≤ 1})
    ((∑ i ∈ s, (f + g) i ^ p) ^ (1 / p))
⊢ (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)

Tactic:
simp only [Pi.add_apply, add_mul, sum_add_distrib] at this

Goal state after:
case inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
hpq : p.HolderConjugate p.conjExponent
this :
  IsGreatest ((fun a ↦ ∑ x ∈ s, f x * a x + ∑ x ∈ s, g x * a x) '' {g | ∑ i ∈ s, g i ^ p.conjExponent ≤ 1})
    ((∑ x ∈ s, (f x + g x) ^ p) ^ (1 / p))
⊢ (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

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

Tactic:
have hp1_lt : 1 < p := by
    refine lt_of_le_of_ne hp1 ?_
    symm
    exact h1

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
h1 : ¬p = 1
hp1_lt : 1 < p
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: case inl
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : 0 ≤ 0
hp1 : 0 ≤ 1
⊢ 1 ≤ 2 ^ (-1) * (1 + 1)

Tactic:
norm_num

Goal state after:
case inl
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : 0 ≤ 0
hp1 : 0 ≤ 1
⊢ 1 ≤ 2 ^ (-1) * 2
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 : ι
⊢ i ∈ s → f i ^ p = |f i| ^ p

Tactic:
hi

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
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
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 : ι
⊢ i ∈ s → g i ^ q = |g i| ^ q

Tactic:
hi

Goal state after:
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.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
hf : ∀ (i : ι), 0 ≤ f i
hg : ∀ (i : ι), 0 ≤ g i
hf_sum : Summable fun i ↦ f i ^ p
hg_sum : Summable fun i ↦ g i ^ q
⊢ (Summable fun i ↦ f i * g i) ∧
    ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)

Tactic:
simpa using summable_and_Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg hpq hf hg hf_sum hg_sum

Goal state after:
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
f g : ↥(Lp E p μ)
⊢ dist f g = (eLpNorm (-↑↑f + ↑↑g) p μ).toReal

Tactic:
simp_rw [dist, norm_def]

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : ↥(Lp E p μ)
⊢ (eLpNorm (↑↑(-f + g)) p μ).toReal = (eLpNorm (-↑↑f + ↑↑g) p μ).toReal
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
p q : ℝ
hpq : p.HolderConjugate q
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
f : ι → ℝ≥0
hf_sum : HasSum (fun i ↦ (fun i ↦ ↑(f i)) i ^ p) (A ^ p)
g : ι → ℝ≥0
hg_sum : HasSum (fun i ↦ (fun i ↦ ↑(g i)) i ^ q) (B ^ q)
⊢ ∃ C, 0 ≤ C ∧ C ≤ A * B ∧ HasSum (fun i ↦ (fun i ↦ ↑(f i)) i * (fun i ↦ ↑(g i)) i) C

Tactic:
lift A to ℝ≥0 using hA

Goal state after:
ι : Type u
p q : ℝ
hpq : p.HolderConjugate q
B : ℝ
hB : 0 ≤ B
f g : ι → ℝ≥0
hg_sum : HasSum (fun i ↦ (fun i ↦ ↑(g i)) i ^ q) (B ^ q)
A : ℝ≥0
hf_sum : HasSum (fun i ↦ (fun i ↦ ↑(f i)) i ^ p) (↑A ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A * B ∧ HasSum (fun i ↦ (fun i ↦ ↑(f i)) i * (fun i ↦ ↑(g i)) i) C
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 : ι
⊢ i ∈ s → f i = |f i|

Tactic:
hi

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|
Module: Mathlib.Analysis.MeanInequalities

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

Tactic:
hi

Goal state after:
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 : ι
⊢ i ∈ s → (f i + g i) ^ p = |f i + g i| ^ p

Tactic:
hi

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
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        ∑' (i : ℕ), B i < ∞ →
          (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) →
            ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : ℕ → ℝ := fun n ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → dist (f n) (f m_1) < B N
M : ℝ
hB : HasSum B M
B1 : ℕ → ℝ≥0∞ := fun n ↦ ENNReal.ofReal (B n)
h_tsum_B1 : ∑' (i : ℕ), B1 i = ENNReal.ofReal M
⊢ HasSum B1 (ENNReal.ofReal M)

Tactic:
have h_sum := (@ENNReal.summable _ B1).hasSum

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        ∑' (i : ℕ), B i < ∞ →
          (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) →
            ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : ℕ → ℝ := fun n ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → dist (f n) (f m_1) < B N
M : ℝ
hB : HasSum B M
B1 : ℕ → ℝ≥0∞ := fun n ↦ ENNReal.ofReal (B n)
h_tsum_B1 : ∑' (i : ℕ), B1 i = ENNReal.ofReal M
h_sum : HasSum B1 (∑' (b : ℕ), B1 b)
⊢ HasSum B1 (ENNReal.ofReal M)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
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 : ι
⊢ i ∈ s → f i ^ p = |f i| ^ p

Tactic:
hi

Goal state after:
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
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
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 : ι
⊢ i ∈ s → g i ^ p = |g i| ^ p

Tactic:
hi

Goal state after:
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: ι : Type u
p : ℝ
hp : 1 ≤ p
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
f : ι → ℝ≥0
hfA : HasSum (fun i ↦ (fun i ↦ ↑(f i)) i ^ p) (A ^ p)
g : ι → ℝ≥0
hgB : HasSum (fun i ↦ (fun i ↦ ↑(g i)) i ^ p) (B ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ A + B ∧ HasSum (fun i ↦ ((fun i ↦ ↑(f i)) i + (fun i ↦ ↑(g i)) i) ^ p) (C ^ p)

Tactic:
lift A to ℝ≥0 using hA

Goal state after:
ι : Type u
p : ℝ
hp : 1 ≤ p
B : ℝ
hB : 0 ≤ B
f g : ι → ℝ≥0
hgB : HasSum (fun i ↦ (fun i ↦ ↑(g i)) i ^ p) (B ^ p)
A : ℝ≥0
hfA : HasSum (fun i ↦ (fun i ↦ ↑(f i)) i ^ p) (↑A ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A + B ∧ HasSum (fun i ↦ ((fun i ↦ ↑(f i)) i + (fun i ↦ ↑(g i)) i) ^ p) (C ^ p)
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
inst✝ : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ C
⊢ ‖f‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * C

Tactic:
by
  by_cases hμ : μ = 0
  · simp [hμ, nnnorm_def]
  rw [← ENNReal.coe_le_coe, nnnorm_def, ENNReal.coe_toNNReal (eLpNorm_ne_top _)]
  refine (eLpNorm_le_of_ae_nnnorm_bound hfC).trans_eq ?_
  rw [← coe_measureUnivNNReal μ, ← ENNReal.coe_rpow_of_ne_zero (measureUnivNNReal_pos hμ).ne',
    ENNReal.coe_mul, mul_comm, ENNReal.smul_def, smul_eq_mul]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inl
ι : Type u
s : Finset ι
f : ι → ℝ≥0∞
p : ℝ
hp✝ : 1 ≤ p
hp : 1 = p
⊢ (∑ i ∈ s, f i) ^ p ≤ ↑(#s) ^ (p - 1) * ∑ i ∈ s, f i ^ p

pp: case inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0∞
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ (∑ i ∈ s, f i) ^ p ≤ ↑(#s) ^ (p - 1) * ∑ i ∈ s, f i ^ p

Tactic:
· simp [← hp]

Goal state after:
case inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0∞
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ (∑ i ∈ s, f i) ^ p ≤ ↑(#s) ^ (p - 1) * ∑ i ∈ s, f i ^ p