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

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : EDist E
inst✝ : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin : ∀ (ε : ℝ≥0∞) (i : ι), μ {x | ε ≤ edist (f i x) (g x)} ≠ ∞
h : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
hf : (fun i ↦ (μ {x | ε ≤ edist (f i x) (g x)}).toNNReal) = ENNReal.toNNReal ∘ fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}
⊢ Tendsto (fun x ↦ μ {x_1 | ε ≤ edist (f x x_1) (g x_1)}) l (𝓝 ↑0)

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : EDist E
inst✝ : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin : ∀ (ε : ℝ≥0∞) (i : ι), μ {x | ε ≤ edist (f i x) (g x)} ≠ ∞
h : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
hf : (fun i ↦ (μ {x | ε ≤ edist (f i x) (g x)}).toNNReal) = ENNReal.toNNReal ∘ fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}
⊢ Tendsto (fun x ↦ μ {x_1 | ε ≤ edist (f x x_1) (g x_1)}) l (𝓝 ↑0)
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : EDist E
inst✝ : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin : ∀ (ε : ℝ≥0∞) (i : ι), μ {x | ε ≤ edist (f i x) (g x)} ≠ ∞
h : ∀ (ε : ℝ≥0∞), 0 < ε → Tendsto (fun i ↦ (μ {x | ε ≤ edist (f i x) (g x)}).toNNReal) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
⊢ Tendsto (ENNReal.toNNReal ∘ fun x ↦ μ {x_1 | ε ≤ edist (f x x_1) (g x_1)}) l (𝓝 (ENNReal.toNNReal 0))

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : EDist E
inst✝ : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin : ∀ (ε : ℝ≥0∞) (i : ι), μ {x | ε ≤ edist (f i x) (g x)} ≠ ∞
h : ∀ (ε : ℝ≥0∞), 0 < ε → Tendsto (fun i ↦ (μ {x | ε ≤ edist (f i x) (g x)}).toNNReal) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
⊢ Tendsto (ENNReal.toNNReal ∘ fun x ↦ μ {x_1 | ε ≤ edist (f x x_1) (g x_1)}) l (𝓝 (ENNReal.toNNReal 0))
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 (fun b ↦ dist (f b) f_lim) fi (𝓝 0) ↔ Tendsto (fun n ↦ eLpNorm (↑↑(f n) - ↑↑f_lim) p μ) fi (𝓝 0)

Tactic:
]

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.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 (fun b ↦ eLpNorm (↑↑(f b) - ↑↑f_lim) p μ) fi (𝓝 0) ↔
    Tendsto (fun n ↦ eLpNorm (↑↑(f n) - ↑↑f_lim) p μ) fi (𝓝 0)

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 μ)
n : ι
⊢ eLpNorm (↑↑(f n) - ↑↑f_lim) p μ ≠ ∞

Tactic:
]

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 μ)
n : ι
⊢ eLpNorm (↑↑(f n) - ↑↑f_lim) 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
ι : Type u_4
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : ↥(Lp E p μ)
n : ι
⊢ eLpNorm (↑↑(f n - f_lim)) p μ ≠ ∞

Tactic:
]

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 μ)
n : ι
⊢ eLpNorm (↑↑(f n - f_lim)) p μ ≠ ∞
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_3.a
ι : Type u_1
s : Finset ι
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
i : ι
hi : i ∈ s
⊢ f i * g i = f i * g i

Tactic:
]

Goal state after:
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 : α → E
f_lim_ℒp : MemLp f_lim p μ
⊢ Tendsto (fun n ↦ eLpNorm (↑↑(f n) - ↑↑(MemLp.toLp f_lim f_lim_ℒp)) p μ) fi (𝓝 0) ↔
    Tendsto (fun n ↦ eLpNorm (↑↑(f n) - f_lim) p μ) fi (𝓝 0)

Tactic:
]

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 : α → E
f_lim_ℒp : MemLp f_lim p μ
⊢ Tendsto (fun n ↦ eLpNorm (↑↑(f n) - ↑↑(MemLp.toLp f_lim f_lim_ℒp)) p μ) fi (𝓝 0) ↔
    Tendsto (fun n ↦ eLpNorm (↑↑(f n) - f_lim) p μ) fi (𝓝 0)
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 : α → E
f_lim_ℒp : MemLp f_lim p μ
h_eq : (fun n ↦ eLpNorm (↑↑(f n) - ↑↑(MemLp.toLp f_lim f_lim_ℒp)) p μ) = fun n ↦ eLpNorm (↑↑(f n) - f_lim) p μ
⊢ Tendsto (fun n ↦ eLpNorm (↑↑(f n) - f_lim) p μ) fi (𝓝 0) ↔ Tendsto (fun n ↦ eLpNorm (↑↑(f n) - f_lim) p μ) fi (𝓝 0)

Tactic:
]

Goal state after:
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 : ι → α → E
f_ℒp : ∀ (n : ι), MemLp (f n) p μ
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
⊢ Tendsto (fun n ↦ eLpNorm (↑↑(MemLp.toLp (f n) ⋯) - ↑↑(MemLp.toLp f_lim f_lim_ℒp)) p μ) fi (𝓝 0) ↔
    Tendsto (fun n ↦ eLpNorm (f n - f_lim) p μ) fi (𝓝 0)

Tactic:
]

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 : ι → α → E
f_ℒp : ∀ (n : ι), MemLp (f n) p μ
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
⊢ Tendsto (fun n ↦ eLpNorm (↑↑(MemLp.toLp (f n) ⋯) - ↑↑(MemLp.toLp f_lim f_lim_ℒp)) p μ) 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
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : EDist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
this : (fun i ↦ μ {x | ε ≤ edist (f' i x) (g' x)}) =ᶠ[l] fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}
⊢ Tendsto (fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}) l (𝓝 0)

Tactic:
]

Goal state after:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : EDist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
this : (fun i ↦ μ {x | ε ≤ edist (f' i x) (g' x)}) =ᶠ[l] fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}
⊢ Tendsto (fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
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 : ι → α → E
f_ℒp : ∀ (n : ι), MemLp (f n) p μ
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
n : ι
a✝ : α
hx₁ : ↑↑(MemLp.toLp (f n - f_lim) ⋯) a✝ = (f n - f_lim) a✝
hx₂ :
  ↑↑(MemLp.toLp (f n) ⋯ - MemLp.toLp f_lim f_lim_ℒp) a✝ = (↑↑(MemLp.toLp (f n) ⋯) - ↑↑(MemLp.toLp f_lim f_lim_ℒp)) a✝
⊢ ↑↑(MemLp.toLp (f n) ⋯ - MemLp.toLp f_lim f_lim_ℒp) a✝ = (f n - f_lim) a✝

Tactic:
]

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 : ι → α → E
f_ℒp : ∀ (n : ι), MemLp (f n) p μ
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
n : ι
a✝ : α
hx₁ : ↑↑(MemLp.toLp (f n - f_lim) ⋯) a✝ = (f n - f_lim) a✝
hx₂ :
  ↑↑(MemLp.toLp (f n) ⋯ - MemLp.toLp f_lim f_lim_ℒp) a✝ = (↑↑(MemLp.toLp (f n) ⋯) - ↑↑(MemLp.toLp f_lim f_lim_ℒp)) a✝
⊢ ↑↑(MemLp.toLp (f n) ⋯ - MemLp.toLp f_lim f_lim_ℒp) a✝ = (f n - f_lim) a✝
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ (∑ i ∈ s, w i * f i) / ↑(#s) ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ / ↑(#s)

pp: case hx
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ ↑(#s)

pp: case h
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 1 - p⁻¹ + p⁻¹ ≠ 0

pp: case hx
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ ∑ i ∈ s, w i * f i ^ p

pp: case hy
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ ↑(#s)

pp: case hx
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ ∑ i ∈ s, w i

pp: case hy
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ ↑(#s)

Tactic:
]

Goal state after:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ (∑ i ∈ s, w i * f i) / ↑(#s) ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ / ↑(#s)

case hx
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ ↑(#s)

case h
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 1 - p⁻¹ + p⁻¹ ≠ 0

case hx
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ ∑ i ∈ s, w i * f i ^ p

case hy
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ ↑(#s)

case hx
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ ∑ i ∈ s, w i

case hy
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ ↑(#s)
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
inst✝¹ : Nonempty ι
inst✝ : SemilatticeSup ι
hp : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
⊢ Tendsto (fun n ↦ eLpNorm (↑↑(f n.1) - ↑↑(f n.2)) p μ) atTop (𝓝 0) ↔
    Tendsto (fun n ↦ eLpNorm (↑↑(f n.1) - ↑↑(f n.2)) p μ) atTop (𝓝 0)

pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
ι : Type u_4
inst✝¹ : Nonempty ι
inst✝ : SemilatticeSup ι
hp : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
n : ι × ι
⊢ eLpNorm (↑↑(f n.1) - ↑↑(f n.2)) p μ ≠ ∞

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
ι : Type u_4
inst✝¹ : Nonempty ι
inst✝ : SemilatticeSup ι
hp : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
n : ι × ι
⊢ eLpNorm (↑↑(f n.1) - ↑↑(f n.2)) 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
ι : Type u_4
inst✝¹ : Nonempty ι
inst✝ : SemilatticeSup ι
hp : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
n : ι × ι
⊢ eLpNorm (↑↑(f n.1 - f n.2)) p μ ≠ ∞

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
ι : Type u_4
inst✝¹ : Nonempty ι
inst✝ : SemilatticeSup ι
hp : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
n : ι × ι
⊢ eLpNorm (↑↑(f n.1 - f n.2)) p μ ≠ ∞
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : EDist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
i : ι
h_ae_eq : f i =ᵐ[μ] f' i
x : α
hxf : f i x = f' i x
hxg : g x = g' x
⊢ {x | ε ≤ edist (f' i x) (g' x)} x ↔ {x | ε ≤ edist (f i x) (g x)} x

Tactic:
]

Goal state after:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : EDist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
i : ι
h_ae_eq : f i =ᵐ[μ] f' i
x : α
hxf : f i x = f' i x
hxg : g x = g' x
⊢ {x | ε ≤ edist (f' i x) (g' x)} x ↔ {x | ε ≤ edist (f i x) (g x)} x
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : EDist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᵐ[μ] f' i
h_right : g =ᵐ[μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
i : ι
h_ae_eq : f i =ᵐ[μ] f' i
x : α
hxf : f i x = f' i x
hxg : g x = g' x
⊢ ε ≤ edist (f' i x) (g' x) ↔ ε ≤ edist (f' i x) (g' x)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

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

Tactic:
lift g to ι → ℝ≥0 using hg

Goal state after:
ι : Type u
p q r : ℝ
hpqr : p.HolderTriple q r
f : ι → ℝ≥0
hf_sum : Summable fun i ↦ (fun i ↦ ↑(f i)) i ^ p
g : ι → ℝ≥0
hg_sum : Summable fun i ↦ (fun i ↦ ↑(g i)) i ^ q
⊢ (Summable fun i ↦ ((fun i ↦ ↑(f i)) i * (fun i ↦ ↑(g i)) i) ^ r) ∧
    ∑' (i : ι), ((fun i ↦ ↑(f i)) i * (fun i ↦ ↑(g i)) i) ^ r ≤
      (∑' (i : ι), (fun i ↦ ↑(f i)) i ^ p) ^ (r / p) * (∑' (i : ι), (fun i ↦ ↑(g i)) i ^ q) ^ (r / q)
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
α : Type ?u.18
E : Type u_6
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α →ₘ[μ] E
hf : f ∈ {f | eLpNorm (↑f) p μ < ∞}
⊢ eLpNorm (↑f) p μ < ∞

Tactic:
]

Goal state after:
α✝ : 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
α : Type ?u.18
E : Type u_6
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α →ₘ[μ] E
hf : f ∈ {f | eLpNorm (↑f) p μ < ∞}
⊢ eLpNorm (↑f) 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
ι : Type u_6
s : Finset ι
f : ι → ↥(Lp E p μ)
⊢ ∑ i ∈ s, ↑↑(f i) =ᵐ[μ] fun x ↦ ∑ i ∈ s, ↑↑(f i) x

Tactic:
]

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
ι : Type u_6
s : Finset ι
f : ι → ↥(Lp E p μ)
⊢ ∑ i ∈ s, ↑↑(f i) =ᵐ[μ] fun x ↦ ∑ i ∈ s, ↑↑(f i) x
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 μ
⊢ (eLpNorm f p μ).toReal = (eLpNorm f p μ).toReal

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
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
hf' : 0 ≤ ∑' (i : ι), f i ^ p
hg' : 0 ≤ ∑' (i : ι), g i ^ q
hr : 0 < r
⊢ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q) =
    (∑' (i : ι), f i ^ p) ^ (r / p * (1 / r)) * (∑' (i : ι), g i ^ q) ^ (r / q * (1 / r))

Tactic:
]

Goal state after:
ι : Type u
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
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
hf' : 0 ≤ ∑' (i : ι), f i ^ p
hg' : 0 ≤ ∑' (i : ι), g i ^ q
hr : 0 < r
⊢ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q) =
    (∑' (i : ι), f i ^ p) ^ (r / p * (1 / r)) * (∑' (i : ι), g i ^ q) ^ (r / q * (1 / r))
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: case neg
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable fun a ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
⊢ ∃ N, ∀ n ≥ N, μ {x | ε ≤ edist (f n x) (g x)} ≤ ↑δ

Tactic:
]

Goal state after:
case neg
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable fun a ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
⊢ ∃ N, ∀ n ≥ N, μ {x | ε ≤ edist (f n x) (g x)} ≤ ↑δ
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 μ)
⊢ (eLpNorm (↑↑f + -↑↑g) p μ).toReal = (eLpNorm (↑↑f + -↑↑g) p μ).toReal

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
hg : ∀ (i : ι), 0 ≤ g i
hg_sum : HasSum (fun i ↦ g i ^ q) (B ^ q)
f : ι → ℝ≥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 * g i) C

Tactic:
lift g to ι → ℝ≥0 using hg

Goal state after:
ι : 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
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 μ)
⊢ eLpNorm (↑↑f + -↑↑g) p μ = eLpNorm (↑↑f + -↑↑g) p μ

Tactic:
]

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 μ)
⊢ edist f g = eLpNorm (↑↑f - ↑↑g) p μ

Tactic:
by
  rw [edist_eq_eLpNorm_neg_add, ← eLpNorm_neg, neg_add, neg_neg, sub_eq_add_neg]

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

Goal state before:
pp: case neg
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable fun a ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : μ t ≤ ↑δ
hunif : TendstoUniformlyOn f g atTop tᶜ
⊢ ∃ N, ∀ n ≥ N, μ {x | ε ≤ edist (f n x) (g x)} ≤ ↑δ

Tactic:
]

Goal state after:
case neg
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable fun a ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : μ t ≤ ↑δ
hunif : TendstoUniformlyOn f g atTop tᶜ
⊢ ∃ N, ∀ n ≥ N, μ {x | ε ≤ edist (f n x) (g x)} ≤ ↑δ
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 μ)
⊢ eLpNorm (↑↑(f - g)) p μ = eLpNorm (↑↑(f - g)) p μ

Tactic:
]

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 : α → E
hf : MemLp f p μ
hg : MemLp g p μ
⊢ eLpNorm (↑↑(MemLp.toLp f hf) - ↑↑(MemLp.toLp g hg)) p μ = eLpNorm (f - g) p μ

Tactic:
]

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hg : MemLp g p μ
⊢ eLpNorm (↑↑(MemLp.toLp f hf) - ↑↑(MemLp.toLp g hg)) p μ = eLpNorm (f - g) 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
⊢ (eLpNorm (↑0) p μ).toNNReal = 0

Tactic:
]

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
⊢ (eLpNorm (↑0) p μ).toNNReal = 0
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)
⊢ ∑' (n : ℕ), ENNReal.ofReal (B n) = ENNReal.ofReal (∑' (b : ℕ), B b)

Tactic:
]

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)
⊢ ∑' (n : ℕ), ENNReal.ofReal (B n) = ENNReal.ofReal (∑' (b : ℕ), B b)