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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
⊢ c < essSup f (μ.restrict s)

Tactic:
obtain ⟨d, cd, hd⟩ : ∃ d, c < d ∧ d < essSup f μ := exists_between hc

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
d : ℝ≥0∞
cd : c < d
hd : d < essSup f μ
⊢ c < essSup f (μ.restrict s)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Defs

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
inst✝ : ENorm ε
μ : Measure α
f : α → ε
hq0_lt : 0 < q
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ = ((∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q)) ^ q

Tactic:
← ENNReal.rpow_mul,

Goal state after:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
inst✝ : ENorm ε
μ : Measure α
f : α → ε
hq0_lt : 0 < q
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ = (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q * q)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ ∀ j ∈ Finset.univ,
    j ≠ i → (μ j).toOuterMeasure (eval j '' (t ∩ (fun b ↦ b i) ⁻¹' s)) ≤ (μ j).toOuterMeasure (eval j '' t)

Tactic:
rintro j - _; gcongr; apply inter_subset_left

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst✝ : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (map (fun x i ↦ f i (x i)) (Measure.pi μ)) (univ.pi s) = ∏ i, (map (f i) (μ i)) (s i)

Tactic:
map_apply_of_aemeasurable _ (.univ_pi hs)

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst✝ : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (Measure.pi μ) ((fun x i ↦ f i (x i)) ⁻¹' univ.pi s) = ∏ i, (map (f i) (μ i)) (s i)

ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst✝ : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ AEMeasurable (fun x i ↦ f i (x i)) (Measure.pi μ)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov

Goal state before:
pp: α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ p.toReal ≠ 0

Tactic:
rw [Ne, ENNReal.toReal_eq_zero_iff]

Goal state after:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ ¬(p = 0 ∨ p = ∞)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
c : ε
s : Set α
hs : NullMeasurableSet s μ
hp : p ≠ 0
hp_top : p ≠ ∞
hp_pos : 0 < p.toReal
⊢ (‖c‖ₑ ^ p.toReal) ^ (1 / p.toReal) * μ s ^ (1 / p.toReal) = ‖c‖ₑ * μ s ^ (1 / p.toReal)

pp: case hz
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
c : ε
s : Set α
hs : NullMeasurableSet s μ
hp : p ≠ 0
hp_top : p ≠ ∞
hp_pos : 0 < p.toReal
⊢ 0 ≤ 1 / p.toReal

Tactic:
← ENNReal.rpow_mul,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
c : ε
s : Set α
hs : NullMeasurableSet s μ
hp : p ≠ 0
hp_top : p ≠ ∞
hp_pos : 0 < p.toReal
⊢ ‖c‖ₑ ^ (p.toReal * (1 / p.toReal)) * μ s ^ (1 / p.toReal) = ‖c‖ₑ * μ s ^ (1 / p.toReal)

case hz
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
c : ε
s : Set α
hs : NullMeasurableSet s μ
hp : p ≠ 0
hp_top : p ≠ ∞
hp_pos : 0 < p.toReal
⊢ 0 ≤ 1 / p.toReal
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 : ℝ
hp : 0 < p
⊢ ((∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p ≤ ↑c ^ p * ((∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p

Tactic:
← ENNReal.rpow_mul,

Goal state after:
α : 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 : ℝ
hp : 0 < p
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p * p) ≤ ↑c ^ p * (∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p * p)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ
p : ℝ
hp : 0 < p
⊢ ((∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p ≤ ↑c ^ p * ((∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p

Tactic:
← ENNReal.rpow_mul,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ
p : ℝ
hp : 0 < p
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p * p) ≤ ↑c ^ p * (∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p * p)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : ¬c = ∞
this : c ^ p ≠ ∞
⊢ ((∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p ≤ c ^ p * ((∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p

Tactic:
← ENNReal.rpow_mul,

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : ¬c = ∞
this : c ^ p ≠ ∞
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p * p) ≤ c ^ p * (∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p * p)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_1
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ∞
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
⊢ ↑C ^ p.toReal * (μ s ^ p.toReal⁻¹) ^ p.toReal ≤ ∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ

Tactic:
← ENNReal.rpow_mul,

Goal state after:
α : Type u_1
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ∞
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
⊢ ↑C ^ p.toReal * μ s ^ (p.toReal⁻¹ * p.toReal) ≤ ∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
C : ℝ
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ eLpNorm f p μ ≤ μ Set.univ ^ p.toReal⁻¹ * ENNReal.ofReal C

Tactic:
← mul_comm

Goal state after:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
C : ℝ
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ eLpNorm f p μ ≤ ENNReal.ofReal C * μ Set.univ ^ p.toReal⁻¹
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
f : α → ε
p q : ℝ
hq_pos : 0 < q
⊢ (∫⁻ (a : α), ‖‖f a‖ₑ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = ((∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / (p * q))) ^ q

Tactic:
← ENNReal.rpow_mul,

Goal state after:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
f : α → ε
p q : ℝ
hq_pos : 0 < q
⊢ (∫⁻ (a : α), ‖‖f a‖ₑ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / (p * q) * q)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
f : α → ε
p q : ℝ
hq_pos : 0 < q
⊢ (∫⁻ (a : α), ‖‖f a‖ₑ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * (q⁻¹ * q))

Tactic:
inv_mul_cancel₀ hq_pos.ne.symm,

Goal state after:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
f : α → ε
p q : ℝ
hq_pos : 0 < q
⊢ (∫⁻ (a : α), ‖‖f a‖ₑ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * 1)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
f : α → ε
p q : ℝ
hq_pos : 0 < q
⊢ (∫⁻ (a : α), (‖f a‖ₑ ^ q) ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ p⁻¹

Tactic:
← ENNReal.rpow_mul,

Goal state after:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
f : α → ε
p q : ℝ
hq_pos : 0 < q
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ (q * p) ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ p⁻¹
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
p q : ℝ
hq_pos : 0 < q
⊢ (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = ((∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / (p * q))) ^ q

Tactic:
← ENNReal.rpow_mul,

Goal state after:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
p q : ℝ
hq_pos : 0 < q
⊢ (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / (p * q) * q)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
p q : ℝ
hq_pos : 0 < q
⊢ (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * (q⁻¹ * q))

Tactic:
inv_mul_cancel₀ hq_pos.ne.symm,

Goal state after:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
p q : ℝ
hq_pos : 0 < q
⊢ (∫⁻ (a : α), ‖‖f a‖ ^ q‖ₑ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (p⁻¹ * 1)
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) < (f y - f x) / (y - x)
⊢ StrictConcaveOn 𝕜 s f

Tactic:
by
  rw [← neg_strictConvexOn_iff]
  refine strictConvexOn_of_slope_strict_mono_adjacent hs fun hx hz hxy hyz => ?_
  simp only [Pi.neg_apply]
  linear_combination hf hx hz hxy hyz

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

Goal state before:
pp: case pos
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ∞
h_rpow : essSup (fun x ↦ ‖‖f x‖ₑ ^ q‖ₑ) μ = essSup (fun x ↦ ‖f x‖ₑ ^ q) μ
⊢ essSup (fun x ↦ ‖f x‖ₑ ^ q) μ = essSup (fun x ↦ ‖f x‖ₑ) μ ^ q

Tactic:
have h_rpow_mono := ENNReal.strictMono_rpow_of_pos hq_pos

Goal state after:
case pos
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ∞
h_rpow : essSup (fun x ↦ ‖‖f x‖ₑ ^ q‖ₑ) μ = essSup (fun x ↦ ‖f x‖ₑ ^ q) μ
h_rpow_mono : StrictMono fun x ↦ x ^ q
⊢ essSup (fun x ↦ ‖f x‖ₑ ^ q) μ = essSup (fun x ↦ ‖f x‖ₑ) μ ^ q
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q r : ℝ≥0
h : p.HolderTriple q r
⊢ r⁻¹ - q⁻¹ = p⁻¹

Tactic:
have := h.symm.inv_lt_inv.le
  exact_mod_cast h.coe.inv_sub_inv_eq_inv

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 ε
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
hμ'_le : μ' ≤ c • μ
f : α → ε
hf : MemLp f p μ
⊢ eLpNorm f p μ' < ∞

Tactic:
grw [eLpNorm_le_of_measure_le_smul hμ'_le]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
hμ'_le : μ' ≤ c • μ
f : α → ε
hf : MemLp f p μ
⊢ c ^ (1 / p).toReal • eLpNorm f 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

Tactic:
by
  -- If some number `z i` equals zero and has non-zero weight, then LHS is 0 and RHS is nonnegative.
  by_cases! A : ∃ i ∈ s, z i = 0 ∧ w i ≠ 0
  · rcases A with ⟨i, his, hzi, hwi⟩
    rw [prod_eq_zero his]
    · exact sum_nonneg fun j hj => mul_nonneg (hw j hj) (hz j hj)
    · rw [hzi]
      exact zero_rpow hwi
  -- If all numbers `z i` with non-zero weight are positive, then we apply Jensen's inequality
  -- for `exp` and numbers `log (z i)` with weights `w i`.
  · have := convexOn_exp.map_sum_le hw hw' fun i _ => Set.mem_univ <| log (z i)
    simp only [exp_sum, smul_eq_mul, mul_comm (w _) (log _)] at this
    convert! this using 1 <;> [apply prod_congr rfl; apply sum_congr rfl] <;> intro i hi
    · rcases eq_or_lt_of_le (hz i hi) with hz | hz
      · simp [A i hi hz.symm]
      · exact rpow_def_of_pos hz _
    · rcases eq_or_lt_of_le (hz i hi) with hz | hz
      · simp [A i hi hz.symm]
      · rw [exp_log hz]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: case hr
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ (ENNReal.ofReal q)⁻¹ ≠ ∞

Tactic:
simp [hpq.symm.pos]

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case pos
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : a + b = 0
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

pp: case neg
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Tactic:
· simp [add_eq_zero.mp h_zero, hp_pos.ne']

Goal state after:
case neg
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p q : ℝ
a✝ b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
a : ℝ≥0∞
⊢ a ^ q = (a ^ p) ^ (q / p)

Tactic:
← ENNReal.rpow_mul,

Goal state after:
p q : ℝ
a✝ b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
a : ℝ≥0∞
⊢ a ^ q = a ^ (p * (q / p))
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ (((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / q)) ^ p ≤ a ^ p + b ^ p

Tactic:
← ENNReal.rpow_mul,

Goal state after:
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / q * p) ≤ a ^ p + b ^ p
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p : ℝ≥0∞
hp : 1 ≤ p
⊢ p.LpAddConst = 1

Tactic:
rw [LpAddConst, if_neg]

Goal state after:
case hnc
p : ℝ≥0∞
hp : 1 ≤ p
⊢ p ∉ Set.Ioo 0 1
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: ⊢ LpAddConst 0 = 1

Tactic:
rw [LpAddConst, if_neg]

Goal state after:
case hnc
⊢ 0 ∉ Set.Ioo 0 1
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case h0
ι : Type u
s : Finset ι
w z : ι → ℝ
hs : s.Nonempty
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 < z i
p_pos : 0 < ∏ i ∈ s, (z i)⁻¹ ^ w i
s_pos : 0 < ∑ i ∈ s, w i * (z i)⁻¹
this : (∑ i ∈ s, w i * (z i)⁻¹)⁻¹ ≤ (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹
p_pos₂ : 0 < (∏ i ∈ s, z i ^ w i)⁻¹
⊢ ∀ i ∈ s, 0 ≤ (z i ^ w i)⁻¹

Tactic:
exact fun i hi ↦ by positivity [hz i hi]

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

Goal state before:
pp: case pos
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : p = ∞
hq_top : q = ∞
⊢ eLpNorm f ∞ μ < ∞

Tactic:
rwa [hq_top] at hfq_lt_top

Goal state after:
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_2
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
p2 : ℝ := q / p
q2 : ℝ := p2.conjExponent
hp2q2 : p2.HolderConjugate q2
⊢ ((∫⁻ (a : α), f a ^ (p * p2) ∂μ) ^ (1 / p2)) ^ (1 / p) * ((∫⁻ (a : α), g a ^ (p * q2) ∂μ) ^ (1 / q2)) ^ (1 / p) =
    (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)

Tactic:
← ENNReal.rpow_mul,

Goal state after:
α : Type u_2
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
p2 : ℝ := q / p
q2 : ℝ := p2.conjExponent
hp2q2 : p2.HolderConjugate q2
⊢ (∫⁻ (a : α), f a ^ (p * p2) ∂μ) ^ (1 / p2 * (1 / p)) * ((∫⁻ (a : α), g a ^ (p * q2) ∂μ) ^ (1 / q2)) ^ (1 / p) =
    (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a ≠ ∞ ∧ b ≠ ∞
⊢ q.toNNReal ≠ 0

Tactic:
simp [hpq.symm.pos]

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

Goal state before:
pp: α : Type u_1
ε' : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε'
inst✝ : ESeminormedAddMonoid ε'
p q : ℝ≥0∞
f : α → ε'
hfq : MemLp f q μ
s : Set α
hf : ∀ x ∉ s, f x = 0
hs : μ s ≠ ∞
hpq : p ≤ q
⊢ (toMeasurable μ s).indicator f = f

Tactic:
apply Set.indicator_eq_self.2

Goal state after:
α : Type u_1
ε' : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε'
inst✝ : ESeminormedAddMonoid ε'
p q : ℝ≥0∞
f : α → ε'
hfq : MemLp f q μ
s : Set α
hf : ∀ x ∉ s, f x = 0
hs : μ s ≠ ∞
hpq : p ≤ q
⊢ Function.support f ⊆ toMeasurable μ s
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h0 : a ≠ 0 ∧ b ≠ 0
h : a ≠ ∞ ∧ b ≠ ∞
⊢ q.toNNReal ≠ 0

Tactic:
simp [hpq.symm.pos]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hf : Summable fun i ↦ f i ^ p
hg : Summable fun i ↦ g i ^ q
⊢ (∑' (i : ι), (f i * g i) ^ r) ^ (1 / r) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)

Tactic:
convert!
    rpow_le_rpow_iff (inv_eq_one_div r ▸ inv_pos.mpr hpqr.pos') |>.mpr <|
      Lr_rpow_le_Lp_mul_Lq_tsum hpqr hf hg

Goal state after:
ι : Type u
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hf : Summable fun i ↦ f i ^ p
hg : Summable fun i ↦ g i ^ q
⊢ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q) =
    ((∑' (i : ι), f i ^ p) ^ (r / p) * (∑' (i : ι), g i ^ q) ^ (r / q)) ^ (1 / r)
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:

Tactic:
(∫⁻ a, (f + g) a ^ p ∂μ) ^ (1 / p) ≤ ((∫⁻ a, f a ^ p ∂μ) + ∫⁻ a, g a ^ p ∂μ) ^ (1 / p) := by
      rw [← lintegral_add_left' (hf.pow_const p)]
      gcongr with a
      exact rpow_add_le_add_rpow _ _ hp0 hp1
    _ ≤ (2 : ℝ≥0∞) ^ (1 / p - 1) * ((∫⁻ a, f a ^ p ∂μ) ^ (1 / p) + (∫⁻ a, g a ^ p ∂μ) ^ (1 / p)) :=
      rpow_add_le_mul_rpow_add_rpow _ _ ((one_le_div hp).2 hp1)

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : SeminormedAddGroup E
f : ℕ → α → E
p : ℝ
hp_pos : 0 < p
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
h_pow_liminf : liminf (fun n ↦ eLpNorm' (f n) p μ) atTop ^ p = liminf (fun n ↦ eLpNorm' (f n) p μ ^ p) atTop
⊢ liminf (fun i ↦ ∫⁻ (a : α), ‖f i a‖ₑ ^ p ∂μ) atTop =
    liminf (fun n ↦ ((∫⁻ (a : α), ‖f n a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p) atTop

Tactic:
← ENNReal.rpow_mul,

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : SeminormedAddGroup E
f : ℕ → α → E
p : ℝ
hp_pos : 0 < p
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
h_pow_liminf : liminf (fun n ↦ eLpNorm' (f n) p μ) atTop ^ p = liminf (fun n ↦ eLpNorm' (f n) p μ ^ p) atTop
⊢ liminf (fun i ↦ ∫⁻ (a : α), ‖f i a‖ₑ ^ p ∂μ) atTop =
    liminf (fun n ↦ (∫⁻ (a : α), ‖f n a‖ₑ ^ p ∂μ) ^ (1 / p * p)) atTop
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 : α → E
hf : MemLp f p μ
⊢ ‖MemLp.toLp f hf‖ = (eLpNorm f p μ).toReal

Tactic:
by
  rw [norm_def, eLpNorm_congr_ae (MemLp.coeFn_toLp hf)]

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
g✝ : E → F
c✝ : ℝ≥0
inst✝ : NormedSpace ℝ E
ν : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
h : μ ≤ c • ν
f g : ↥(Lp E p ν)
this : μ ≪ ν
⊢ ↑↑(f + g) =ᵐ[ν] ↑↑f + ↑↑g

Tactic:
grw [Lp.coeFn_add]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpOrder

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝⁴ : NormedAddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Fact (1 ≤ p)
inst✝ : ClosedIciTopology E
f : ℕ → ↥(Lp E p μ)
f₀ : ↥(Lp E p μ)
hf : ∀ (n : ℕ), 0 ≤ f n
h_tendsto : Filter.Tendsto f Filter.atTop (nhds f₀)
⊢ f₀ ∈ {x | 0 ≤ x}

Tactic:
by
    simp only [← coeFn_nonneg] at hf ⊢
    obtain ⟨φ, -, hφ⟩ := tendstoInMeasure_of_tendsto_Lp h_tendsto |>.exists_seq_tendsto_ae
    filter_upwards [countable_iInter_mem.mpr hf, hφ] with x hx hφx
    exact ge_of_tendsto' hφx fun _ ↦ Set.mem_iInter.mp hx _

Goal state after: