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

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst✝ : NormedAddCommGroup β
μ : Measure α
hp' : p ≠ ∞
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ x ∈ s, dist (f x) (g x) ≤ c
hp : ¬p = 0
this : ∀ (x : α), ‖s.indicator (f - g) x‖ ≤ ‖s.indicator (fun x ↦ c) x‖
⊢ ENNReal.ofReal ‖c‖ * μ s ^ (1 / p.toReal) ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal)

Tactic:
Real.norm_eq_abs,

Goal state after:
case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst✝ : NormedAddCommGroup β
μ : Measure α
hp' : p ≠ ∞
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ x ∈ s, dist (f x) (g x) ≤ c
hp : ¬p = 0
this : ∀ (x : α), ‖s.indicator (f - g) x‖ ≤ ‖s.indicator (fun x ↦ c) x‖
⊢ ENNReal.ofReal |c| * μ s ^ (1 / p.toReal) ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case e_a
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
⊢ q * (1 / q) = 1

Tactic:
one_div,

Goal state after:
case e_a
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
⊢ q * q⁻¹ = 1
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: case inr
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_7
inst✝ : NormedAddCommGroup β
hp_top : p ≠ ∞
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε✝ : ε ≠ 0
hp₀ : p ≠ 0
s : Set α
hsm : MeasurableSet s
hs : μ s < ∞
hε : ∫⁻ (a : α) in sᶜ, ‖f a‖ₑ ^ p.toReal ∂μ < ε ^ p.toReal
⊢ (∫⁻ (x : α) in sᶜ, ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) < ε

Tactic:
one_div,

Goal state after:
case inr
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_7
inst✝ : NormedAddCommGroup β
hp_top : p ≠ ∞
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε✝ : ε ≠ 0
hp₀ : p ≠ 0
s : Set α
hsm : MeasurableSet s
hs : μ s < ∞
hε : ∫⁻ (a : α) in sᶜ, ‖f a‖ₑ ^ p.toReal ∂μ < ε ^ p.toReal
⊢ (∫⁻ (x : α) in sᶜ, ‖f x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ < ε
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case e_a
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
⊢ q * (1 / q) = 1

Tactic:
one_div,

Goal state after:
case e_a
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
⊢ q * q⁻¹ = 1
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 * μ s ^ (1 / p.toReal) ≤ (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

Tactic:
one_div,

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 * μ s ^ p.toReal⁻¹ ≤ (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
hμ : NeZero μ
hp : ¬p = 0
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖C‖ₑ
⊢ ‖C‖ₑ * μ Set.univ ^ (1 / p.toReal) = C • μ Set.univ ^ p.toReal⁻¹

Tactic:
one_div,

Goal state after:
case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
hμ : NeZero μ
hp : ¬p = 0
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖C‖ₑ
⊢ ‖C‖ₑ * μ Set.univ ^ p.toReal⁻¹ = 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 * (1 / q) * q)

Tactic:
one_div,

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⁻¹ * 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 ∂μ) ^ (1 / p) = (∫⁻ (a : α), ‖f a‖ₑ ^ (p * q) ∂μ) ^ (1 / p * (1 / q) * q)

Tactic:
one_div,

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⁻¹ * 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 : α), ENNReal.ofReal ‖‖f a‖ ^ q‖ ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ^ (p * q) ∂μ) ^ p⁻¹

Tactic:
Real.norm_eq_abs,

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 : α), ENNReal.ofReal |‖f a‖ ^ q| ^ p ∂μ) ^ p⁻¹ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ^ (p * q) ∂μ) ^ p⁻¹
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
⊢ 1 + p * s ≠ 1

Tactic:
contrapose hs'

Goal state after:
s : ℝ
hs✝ : -1 ≤ s
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs' : 1 + p * s = 1
⊢ s = 0
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
⊢ 1 + p * s ≠ 1

Tactic:
contrapose hs'

Goal state after:
s : ℝ
hs✝ : -1 ≤ s
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs' : 1 + p * s = 1
⊢ s = 0
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q : ℝ
h : p.HolderConjugate q
⊢ (ENNReal.ofReal p).HolderConjugate (ENNReal.ofReal q)

Tactic:
simpa using Real.HolderTriple.ennrealOfReal h

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

Goal state before:
pp: x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
⊢ ∀ ⦃a b : ℝ⦄, 0 < a → 0 < b → a + b = 1 → a • log x + b • log y < log (a • x + b • y)

Tactic:
a

Goal state after:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a : ℝ
⊢ ∀ ⦃b : ℝ⦄, 0 < a → 0 < b → a + b = 1 → a • log x + b • log y < log (a • x + b • y)
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
⊢ (a ^ p + b ^ p) ^ (1 / p) ≤ a + b

Tactic:
one_div,

Goal state after:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
⊢ (a ^ p + b ^ p) ^ p⁻¹ ≤ a + b
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p q : ℝ
hp✝ : 0 ≤ p
hq✝ : 0 ≤ q
hpq : p + q = 1
hp : 0 < p
hq : 0 < q
⊢ 1 < 1 / p

Tactic:
one_div,

Goal state after:
α : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
p q : ℝ
hp✝ : 0 ≤ p
hq✝ : 0 ≤ q
hpq : p + q = 1
hp : 0 < p
hq : 0 < q
⊢ 1 < p⁻¹
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ (a ^ p + b ^ p) ^ (1 / p) ≤ a + b

Tactic:
one_div,

Goal state after:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ (a ^ p + b ^ p) ^ p⁻¹ ≤ a + b
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p : ℝ≥0∞
h : p ∈ Set.Ioo 0 1
⊢ 0 ≤ 1 / p.toReal - 1

Tactic:
one_div,

Goal state after:
p : ℝ≥0∞
h : p ∈ Set.Ioo 0 1
⊢ 0 ≤ p.toReal⁻¹ - 1
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
q : ℝ
hq_pos : 0 < q
h_le : ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ ≤ ∫⁻ (x : α), eLpNormEssSup f μ ^ q ∂μ
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) ≤ (eLpNormEssSup f μ ^ q) ^ q⁻¹ * μ Set.univ ^ (1 / q)

Tactic:
one_div,

Goal state after:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
q : ℝ
hq_pos : 0 < q
h_le : ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ ≤ ∫⁻ (x : α), eLpNormEssSup f μ ^ q ∂μ
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ q⁻¹ ≤ (eLpNormEssSup f μ ^ q) ^ q⁻¹ * μ Set.univ ^ q⁻¹
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: case refine_2
α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
⊢ ∑ i ∈ insertNone s, i.elim q p = 1

Tactic:
simp_rw [sum_insertNone, Option.elim]
    exact hpq

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

Goal state before:
pp: α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
p q : ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ 1 / q ≤ 1 / p

Tactic:
one_div,

Goal state after:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
p q : ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ q⁻¹ ≤ 1 / p
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
p q : ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ q⁻¹ ≤ 1 / p

Tactic:
one_div,

Goal state after:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
p q : ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ q⁻¹ ≤ p⁻¹
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
p q : ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ 0 ≤ 1 / p - 1 / q

Tactic:
rwa [le_sub_comm, sub_zero, one_div, one_div, inv_le_inv₀ hq_pos hp_pos]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : ∑ i ∈ s, f i ^ p ≤ 1
hg : ∑ i ∈ s, g i ^ q ≤ 1
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
⊢ 1 / p.toNNReal + 1 / q.toNNReal = 1

Tactic:
one_div,

Goal state after:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : ∑ i ∈ s, f i ^ p ≤ 1
hg : ∑ i ∈ s, g i ^ q ≤ 1
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
⊢ p.toNNReal⁻¹ + q.toNNReal⁻¹ = 1
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: case h₂.inr.inr
α : 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 α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
⊢ (∫⁻ (x : α), ‖‖f x‖ * ‖g x‖‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) ≤
    essSup (fun x ↦ ‖f x‖ₑ) μ * (∫⁻ (x : α), ‖g x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

Tactic:
one_div,

Goal state after:
case h₂.inr.inr
α : 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 α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
⊢ (∫⁻ (x : α), ‖‖f x‖ * ‖g x‖‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ ≤
    essSup (fun x ↦ ‖f x‖ₑ) μ * (∫⁻ (x : α), ‖g x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inr.inr.refine_1
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
hg : 0 < ∑ i ∈ s, g i ^ q
f' : ι → ℝ≥0 := fun i ↦ f i / (∑ i ∈ s, f i ^ p) ^ (1 / p)
g' : ι → ℝ≥0 := fun i ↦ g i / (∑ i ∈ s, g i ^ q) ^ (1 / q)
⊢ (∑ i ∈ s, f i ^ p) / (∑ i ∈ s, f i ^ p) ^ (1 / p * p) = 1

Tactic:
one_div,

Goal state after:
case inr.inr.refine_1
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
hg : 0 < ∑ i ∈ s, g i ^ q
f' : ι → ℝ≥0 := fun i ↦ f i / (∑ i ∈ s, f i ^ p) ^ (1 / p)
g' : ι → ℝ≥0 := fun i ↦ g i / (∑ i ∈ s, g i ^ q) ^ (1 / q)
⊢ (∑ i ∈ s, f i ^ p) / (∑ i ∈ s, f i ^ p) ^ (p⁻¹ * p) = 1
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inr.inr.refine_2
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
hg : 0 < ∑ i ∈ s, g i ^ q
f' : ι → ℝ≥0 := fun i ↦ f i / (∑ i ∈ s, f i ^ p) ^ (1 / p)
g' : ι → ℝ≥0 := fun i ↦ g i / (∑ i ∈ s, g i ^ q) ^ (1 / q)
⊢ (∑ i ∈ s, g i ^ q) / (∑ i ∈ s, g i ^ q) ^ (1 / q * q) = 1

Tactic:
one_div,

Goal state after:
case inr.inr.refine_2
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
hg : 0 < ∑ i ∈ s, g i ^ q
f' : ι → ℝ≥0 := fun i ↦ f i / (∑ i ∈ s, f i ^ p) ^ (1 / p)
g' : ι → ℝ≥0 := fun i ↦ g i / (∑ i ∈ s, g i ^ q) ^ (1 / q)
⊢ (∑ i ∈ s, g i ^ q) / (∑ i ∈ s, g i ^ q) ^ (q⁻¹ * q) = 1
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case h.inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
⊢ ∑ i ∈ s, f i ^ p = (∑ i ∈ s, f i ^ p) ^ (1 / p + 1 / q)

pp: case h.inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / q) ≠ 0

Tactic:
one_div,

Goal state after:
case h.inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
⊢ ∑ i ∈ s, f i ^ p = (∑ i ∈ s, f i ^ p) ^ (p⁻¹ + 1 / q)

case h.inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / q) ≠ 0
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case h.inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
⊢ ∑ i ∈ s, f i ^ p = (∑ i ∈ s, f i ^ p) ^ (p⁻¹ + 1 / q)

pp: case h.inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / q) ≠ 0

Tactic:
one_div,

Goal state after:
case h.inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
⊢ ∑ i ∈ s, f i ^ p = (∑ i ∈ s, f i ^ p) ^ (p⁻¹ + q⁻¹)

case h.inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / q) ≠ 0
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i ↦ f i ^ p
hg : Summable fun i ↦ g i ^ p
pos : 0 < p
s : Finset ι
⊢ ∑ i ∈ s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p

Tactic:
one_div,

Goal state after:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i ↦ f i ^ p
hg : Summable fun i ↦ g i ^ p
pos : 0 < p
s : Finset ι
⊢ ∑ i ∈ s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ p⁻¹ + (∑' (i : ι), g i ^ p) ^ p⁻¹) ^ p
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
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
h1 : ¬p = 1
⊢ 1 < p

Tactic:
refine lt_of_le_of_ne hp1 ?_

Goal state after:
α : 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
⊢ 1 ≠ p
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i ↦ f i ^ p
hg : Summable fun i ↦ g i ^ p
pos : 0 < p
H₁ :
  ∀ (s : Finset ι), ∑ i ∈ s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p
bdd : BddAbove (Set.range fun s ↦ ∑ i ∈ s, (f i + g i) ^ p)
H₂ : Summable fun i ↦ (f i + g i) ^ p
⊢ (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)

Tactic:
one_div,

Goal state after:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i ↦ f i ^ p
hg : Summable fun i ↦ g i ^ p
pos : 0 < p
H₁ :
  ∀ (s : Finset ι), ∑ i ∈ s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p
bdd : BddAbove (Set.range fun s ↦ ∑ i ∈ s, (f i + g i) ^ p)
H₂ : Summable fun i ↦ (f i + g i) ^ p
⊢ (∑' (i : ι), (f i + g i) ^ p) ^ p⁻¹ ≤ (∑' (i : ι), f i ^ p) ^ p⁻¹ + (∑' (i : ι), g i ^ p) ^ p⁻¹
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))
⊢ (∫⁻ (a : α), liminf (fun x ↦ ‖f x a‖ₑ ^ p) atTop ∂μ) ^ (1 / p) ≤ liminf (fun n ↦ eLpNorm' (f n) p μ) atTop

Tactic:
one_div,

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))
⊢ (∫⁻ (a : α), liminf (fun x ↦ ‖f x a‖ₑ ^ p) atTop ∂μ) ^ p⁻¹ ≤ liminf (fun n ↦ eLpNorm' (f n) p μ) atTop
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : SeminormedAddCommGroup E
l : Filter ι
f : ι → α → E
g : α → E
⊢ TendstoInMeasure μ f l g ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ε ≠ ∞ → Tendsto (fun i ↦ μ {x | ε ≤ ‖f i x - g x‖ₑ}) l (𝓝 0)

Tactic:
by
  simp_rw [← edist_eq_enorm_sub]
  exact ⟨fun h ε hε hε_top ↦ h ε hε, tendstoInMeasure_of_ne_top⟩

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:
one_div,

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 ∂μ) ^ (p⁻¹ * p)) atTop
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
ι : Type u_4
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : ↥(Lp E p μ)
⊢ Tendsto f fi (𝓝 f_lim) ↔ Tendsto (fun n ↦ eLpNorm (↑↑(f n) - ↑↑f_lim) p μ) fi (𝓝 0)

Tactic:
tendsto_iff_dist_tendsto_zero

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝¹ : NormedAddCommGroup E
ι : Type u_4
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : ↥(Lp E p μ)
⊢ Tendsto (fun b ↦ dist (f b) f_lim) fi (𝓝 0) ↔ Tendsto (fun n ↦ eLpNorm (↑↑(f n) - ↑↑f_lim) p μ) fi (𝓝 0)
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ TendstoInMeasure μ f atTop g

Tactic:
have hg : AEStronglyMeasurable g μ := aestronglyMeasurable_of_tendsto_ae _ hf hfg

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
⊢ TendstoInMeasure μ f atTop g
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
hf_eq_ae : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) ⋯ x = f n x
x : α
hxf : ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) ⋯ x = f n x
hxg : g x = AEStronglyMeasurable.mk g hg x
hxfg : Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ Tendsto (fun n ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (g x))

Tactic:
funext fun n => hxf n

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
hf_eq_ae : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) ⋯ x = f n x
x : α
hxf : ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) ⋯ x = f n x
hxg : g x = AEStronglyMeasurable.mk g hg x
hxfg : Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))