mathlib-initiative/mathlib-tactics huggingface dataset:
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
hp1_lt : 1 < p
hpq : p.HolderConjugate p.conjExponent
h0 : ¬∫⁻ (a : α), (f + g) a ^ p ∂μ = 0
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)

Tactic:
exact lintegral_Lp_add_le_aux hpq hf hg h0
    (lintegral_rpow_add_lt_top_of_lintegral_rpow_lt_top hf hf_top hg_top hp1).ne

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

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

Tactic:
simp [sum_nonneg, rpow_nonneg, abs_nonneg, le_trans zero_le_one hp, abs_add_le,
      rpow_le_rpow]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

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

Tactic:
simp [sum_nonneg, rpow_nonneg, abs_nonneg, le_trans zero_le_one hp, abs_add_le,
      rpow_le_rpow]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

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

Tactic:
simp [sum_nonneg, rpow_nonneg, abs_nonneg, le_trans zero_le_one hp, abs_add_le,
      rpow_le_rpow]

Goal state after:
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
inst✝ : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
⊢ TendstoInMeasure μ f l g ↔ ∀ (ε : ℝ≥0∞), 0 < ε → Tendsto (fun i ↦ (μ {x | ε ≤ edist (f i x) (g x)}).toNNReal) l (𝓝 0)

Tactic:
have hfin ε i : μ { x | ε ≤ edist (f i x) (g x) } ≠ ⊤ :=
    measure_ne_top μ {x | ε ≤ edist (f i x) (g x)}

Goal state after:
α : 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)} ≠ ∞
⊢ TendstoInMeasure μ f l g ↔ ∀ (ε : ℝ≥0∞), 0 < ε → Tendsto (fun i ↦ (μ {x | ε ≤ edist (f i x) (g x)}).toNNReal) l (𝓝 0)
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) ^ (1 - p⁻¹ + p⁻¹)

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

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) ^ 1

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.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 μ)
h : ↑↑f =ᵐ[μ] ↑↑g
⊢ ↑↑f =ᵐ[μ] ↑↑g

Tactic:
exact h

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
⊢ (∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i

Tactic:
have h_nnnorm_nonneg :
    (fun a => ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p) = fun a =>
      (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p := by
    ext1 a
    congr
    simp_rw [← ofReal_norm]
    rw [← ENNReal.ofReal_sum_of_nonneg]
    · rw [Real.norm_of_nonneg _]
      exact Finset.sum_nonneg fun x _ => norm_nonneg _
    · exact fun x _ => norm_nonneg _

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
h_nnnorm_nonneg :
  (fun a ↦ ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p) = fun a ↦
    (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p
⊢ (∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
Module: Mathlib.Analysis.MeanInequalities

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

Tactic:
replace H : (∀ i ∈ s, w i = 0) ∨ ∀ i ∈ s, w i = 0 ∨ f i = 0 := by
      simpa [hp₀, hp₁, hp₀.not_gt, hp₁.not_gt, sum_eq_zero_iff_of_nonneg] using H

Goal state after:
case pos
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : (∀ i ∈ s, w i = 0) ∨ ∀ i ∈ s, w i = 0 ∨ f i = 0
⊢ ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: case pos.refine_1
α : Type u_1
m✝ : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
hp : 1 ≤ ∞
hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → essSup (fun x ↦ ‖(f n - f m) x‖ₑ) μ < B N
x : α
n m N : ℕ
hx : ‖(f n - f m) x‖ₑ < B N
hnN : N ≤ n
hmN : N ≤ m
⊢ ENNReal.ofReal ‖f n x - f m x‖ ≤ B N

Tactic:
ofReal_norm

Goal state after:
case pos.refine_1
α : Type u_1
m✝ : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
hp : 1 ≤ ∞
hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → essSup (fun x ↦ ‖(f n - f m) x‖ₑ) μ < B N
x : α
n m N : ℕ
hx : ‖(f n - f m) x‖ₑ < B N
hnN : N ≤ n
hmN : N ≤ m
⊢ ‖f n x - f m x‖ₑ ≤ B N
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
x✝ : R
⊢ (↑x + x✝)⁻¹ʳ - ↑x⁻¹ + ↑x⁻¹ * x✝ * ↑x⁻¹ = (↑x + x✝)⁻¹ʳ - (∑ i ∈ range 2, (-↑x⁻¹ * x✝) ^ i) * ↑x⁻¹

Tactic:
simp only [sum_range_succ, sum_range_zero, zero_add, pow_zero, pow_one, add_mul, one_mul,
    ← sub_sub, neg_mul, sub_neg_eq_add]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real s + μ.real t
hu : μ u ≠ ∞
⊢ (μ u).toReal < (μ s).toReal + (μ t).toReal

Tactic:
exact h

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

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
f g : α → ε'
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : IntegrableOn f s μ
hg : IntegrableOn g sᶜ μ
⊢ Integrable (s.piecewise f g) μ

Tactic:
by
  rw [IntegrableOn] at hf hg
  rw [← memLp_one_iff_integrable] at hf hg ⊢
  exact MemLp.piecewise hs hf hg

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst✝⁹ : MeasurableSpace δ
inst✝⁸ : NormedAddCommGroup β
inst✝⁷ : NormedAddCommGroup γ
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
inst✝⁴ : TopologicalSpace ε'
inst✝³ : ContinuousENorm ε'
inst✝² : ENorm ε''
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
⊢ ∀ (x y : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))),
    MemLp.toLp (fun x_1 ↦ f x_1 • ↑↑(x + y) x_1) ⋯ =
      MemLp.toLp (fun x_1 ↦ f x_1 • ↑↑x x_1) ⋯ + MemLp.toLp (fun x ↦ f x • ↑↑y x) ⋯

Tactic:
intro u v

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst✝⁹ : MeasurableSpace δ
inst✝⁸ : NormedAddCommGroup β
inst✝⁷ : NormedAddCommGroup γ
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
inst✝⁴ : TopologicalSpace ε'
inst✝³ : ContinuousENorm ε'
inst✝² : ENorm ε''
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u v : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
⊢ MemLp.toLp (fun x ↦ f x • ↑↑(u + v) x) ⋯ = MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯ + MemLp.toLp (fun x ↦ f x • ↑↑v x) ⋯
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
a✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ AEMeasurable f (μ.restrict s)

Tactic:
have : (Set.piecewise s f fun _ => f default) =ᵐ[μ.restrict s] f := piecewise_ae_eq_restrict hs

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
a✝ : Nontrivial α
inhabited_h : Inhabited α
this : (s.piecewise f fun x ↦ f default) =ᵐ[μ.restrict s] f
⊢ AEMeasurable f (μ.restrict s)
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : SeminormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
k n : ℕ
f : MultilinearMap 𝕜 (fun x ↦ G) G'
s : Finset (Fin n)
hk : #s = k
z : G
C : ℝ
H : ∀ (m : Fin n → G), ‖f m‖ ≤ C * ∏ i, ‖m i‖
v : Fin k → G
⊢ ‖(f.restr s hk z) v‖ ≤ C * ‖z‖ ^ (n - k) * ∏ i, ‖v i‖

Tactic:
rw [mul_right_comm, mul_assoc]
  convert! H _ using 2
  simp only [apply_dite norm, Fintype.prod_dite, prod_const ‖z‖, Finset.card_univ,
    Fintype.card_of_subtype sᶜ fun _ => mem_compl, card_compl, Fintype.card_fin, hk, ←
    (s.orderIsoOfFin hk).symm.bijective.prod_comp fun x => ‖v x‖]
  convert! rfl

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s t : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
ht : MeasurableSet t
hts : t ⊆ s
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ IsSeparable (f '' s)

Tactic:
exact (hs.image_of_continuousOn hf).isSeparable

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
E : Type u_9
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
a✝ : AEStronglyMeasurable f μ
⊢ ∫⁻ (a : α), ‖f a‖ₑ * ‖c‖ₑ ∂μ < ∞ ↔ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞

Tactic:
lintegral_mul_const' _ _ enorm_ne_top,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
E : Type u_9
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
a✝ : AEStronglyMeasurable f μ
⊢ (∫⁻ (a : α), ‖f a‖ₑ ∂μ) * ‖c‖ₑ < ∞ ↔ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
H : Type u_8
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f μ'
hf : StronglyMeasurable f
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ' < ∞

Tactic:
exact hf_int.2

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case a
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : IsEmpty ι
x✝ : G
x : (i : ι) → E i
⊢ ‖(constOfIsEmpty 𝕜 E x✝) x‖ ≤ ‖x✝‖ * ∏ i, ‖x i‖

Tactic:
Fintype.prod_empty,

Goal state after:
case a
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : IsEmpty ι
x✝ : G
x : (i : ι) → E i
⊢ ‖(constOfIsEmpty 𝕜 E x✝) x‖ ≤ ‖x✝‖ * 1
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
Y : Type u_2
ε'' : Type u_5
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace ε''
inst✝² : ESeminormedAddMonoid ε''
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → ε''
μ : Measure X
⊢ LocallyIntegrable f (Measure.map (⇑e) μ) ↔ LocallyIntegrable (f ∘ ⇑e) μ

Tactic:
by
  refine ⟨fun h x => ?_, fun h x => ?_⟩
  · rcases h (e x) with ⟨U, hU, h'U⟩
    refine ⟨e ⁻¹' U, e.continuous.continuousAt.preimage_mem_nhds hU, ?_⟩
    exact (integrableOn_map_equiv e.toMeasurableEquiv).1 h'U
  · rcases h (e.symm x) with ⟨U, hU, h'U⟩
    refine ⟨e.symm ⁻¹' U, e.symm.continuous.continuousAt.preimage_mem_nhds hU, ?_⟩
    apply (integrableOn_map_equiv e.toMeasurableEquiv).2
    simp only [Homeomorph.toMeasurableEquiv_coe]
    convert! h'U
    ext x
    simp only [mem_preimage, Homeomorph.symm_apply_apply]

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

Goal state before:
pp: case mpr
X : Type u_1
ε'' : Type u_5
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace ε''
inst✝³ : ESeminormedAddMonoid ε''
μ : Measure X
inst✝² : PseudoMetrizableSpace ε''
f : X → ε''
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
⊢ (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ → Integrable f μ

Tactic:
refine fun h ↦ integrable_iff_integrableAtFilter_cocompact.mpr ⟨?_, h.2⟩
    exact (IntegrableAtFilter.sup_iff.mpr h.1).filter_mono cocompact_le_atBot_atTop

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

Goal state before:
pp: case neg
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm (fun x ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
hp : 0 < p.toReal
hF_meas : ∀ (n : ℕ), Measurable fun x ↦ ‖(approxOn f hf s y₀ h₀ n) x - f x‖ₑ ^ p.toReal
h_bound : ∀ (n : ℕ), (fun x ↦ ‖(approxOn f hf s y₀ h₀ n) x - f x‖ₑ ^ p.toReal) ≤ᵐ[μ] fun x ↦ ‖f x - y₀‖ₑ ^ p.toReal
h_fin : ∫⁻ (a : β), ‖f a - y₀‖ₑ ^ p.toReal ∂μ ≠ ∞
⊢ Tendsto (fun n ↦ ∫⁻ (x : β), ‖(approxOn f hf s y₀ h₀ n) x - f x‖ₑ ^ p.toReal ∂μ) atTop (𝓝 0)

Tactic:
have h_lim :
    ∀ᵐ a : β ∂μ, Tendsto (‖approxOn f hf s y₀ h₀ · a - f a‖ₑ ^ p.toReal) atTop (𝓝 0) := by
    filter_upwards [hμ] with a ha
    have : Tendsto (fun n => (approxOn f hf s y₀ h₀ n) a - f a) atTop (𝓝 (f a - f a)) :=
      (tendsto_approxOn hf h₀ ha).sub tendsto_const_nhds
    convert! continuous_rpow_const.continuousAt.tendsto.comp (tendsto_coe.mpr this.nnnorm)
    simp [zero_rpow_of_pos hp]

Goal state after:
case neg
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm (fun x ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
hp : 0 < p.toReal
hF_meas : ∀ (n : ℕ), Measurable fun x ↦ ‖(approxOn f hf s y₀ h₀ n) x - f x‖ₑ ^ p.toReal
h_bound : ∀ (n : ℕ), (fun x ↦ ‖(approxOn f hf s y₀ h₀ n) x - f x‖ₑ ^ p.toReal) ≤ᵐ[μ] fun x ↦ ‖f x - y₀‖ₑ ^ p.toReal
h_fin : ∫⁻ (a : β), ‖f a - y₀‖ₑ ^ p.toReal ∂μ ≠ ∞
h_lim : ∀ᵐ (a : β) ∂μ, Tendsto (fun x ↦ ‖(approxOn f hf s y₀ h₀ x) a - f a‖ₑ ^ p.toReal) atTop (𝓝 0)
⊢ Tendsto (fun n ↦ ∫⁻ (x : β), ‖(approxOn f hf s y₀ h₀ n) x - f x‖ₑ ^ p.toReal ∂μ) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F'
h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T s = 0
f : α →ₛ E
hf : Integrable (⇑f) μ
x : E
x✝ : x ∈ f.range
hx0 : x = 0
⊢ (T (⇑f ⁻¹' {x})) x = 0

Tactic:
simp [hx0]

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
f g : ↥(simpleFunc G p μ)
⊢ ↑↑↑f ≤ᵐ[μ] ↑↑↑g ↔ ↑f ≤ ↑g

Tactic:
← Lp.coeFn_le

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
f g : ↥(simpleFunc G p μ)
⊢ ↑↑↑f ≤ᵐ[μ] ↑↑↑g ↔ ↑↑↑f ≤ᵐ[μ] ↑↑↑g
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
T : Set α → E →L[ℝ] F
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ‖T s‖ ≤ C * μ.real s
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ C * ∑ x ∈ f.range, μ.real (⇑f ⁻¹' {x}) * ‖x‖ = C * integral μ (map norm f)

Tactic:
by
      rw [map_integral f norm hf norm_zero]; simp_rw [smul_eq_mul]

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

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F
h : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T s = T' s
f : α →ₛ E
hf : Integrable (⇑f) μ
x : E
x✝ : x ∈ f.range
hx0 : x = 0
⊢ (T (⇑f ⁻¹' {x})) x = (T' (⇑f ⁻¹' {x})) x

Tactic:
simp [hx0]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
⊢ ∫ (x : α), 0 ∂μ = 0

Tactic:
by
  simp only [integral_eq_setToFun]
  apply setToFun_zero

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst✝ : NormedAddCommGroup P
f : α → P
hf : AEStronglyMeasurable f μ
⊢ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal = (∫⁻ (x : α), ‖f x‖ₑ ∂μ).toReal

Tactic:
ofReal_norm

Goal state after:
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
β : Type u_3
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ ∃ φ, ∃ (_ : Tendsto φ l (𝓝 1⁻¹)), u⁻¹ =ᶠ[l] φ * v⁻¹

Tactic:
refine ⟨fun x ↦ (φ x)⁻¹, Tendsto.inv₀ hφ (by simp), ?_⟩

Goal state after:
α : Type u_1
β : Type u_3
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ u⁻¹ =ᶠ[l] (fun x ↦ (φ x)⁻¹) * v⁻¹
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : NormedField β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst✝ : ClosedIicTopology β
h : u ~[l] v
⊢ ∃ φ, (∀ᶠ (x : α) in l, 0 < φ x) ∧ u =ᶠ[l] φ * v

Tactic:
by
  obtain ⟨φ, hφ, h_eq⟩ := h.exists_eq_mul
  exact ⟨φ, hφ.eventually_const_lt (zero_lt_one' β), h_eq⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
⊢ ‖f z₁‖ ≤ c

Tactic:
apply h

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := ⋯
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
⊢ z₁ ∈ sphere 0 r
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 E
inst✝ : DistribSMul 𝕜 F
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : ↥(α →₁ₛ[μ] E)
⊢ setToL1S T (c • f) = c • setToL1S T f

Tactic:
simp_rw [setToL1S]
  rw [← SimpleFunc.setToSimpleFunc_smul T h_add h_smul c (SimpleFunc.integrable f)]
  refine SimpleFunc.setToSimpleFunc_congr T h_zero h_add (SimpleFunc.integrable _) ?_
  exact smul_toSimpleFunc c f

Goal state after: