mathlib-initiative/mathlib-tactics huggingface dataset:
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 ≤ ↑(c ^ p) * ‖g a‖ₑ ^ p

Tactic:
have aux (x) : (↑c) ^ p * ‖g x‖ₑ ^ p = (↑c * ‖g x‖ₑ) ^ p := by
    have : ¬(p < 0) := by linarith
    simp [ENNReal.mul_rpow_eq_ite, this]

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
aux : ∀ (x : α), ↑c ^ p * ‖g x‖ₑ ^ p = (↑c * ‖g x‖ₑ) ^ p
⊢ ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ^ p ≤ ↑(c ^ p) * ‖g a‖ₑ ^ p
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), (μ i).IsOpenPosMeasure
U : Set ((i : ι) → α i)
U_open : IsOpen[Pi.topologicalSpace] U
a : (i : ι) → α i
ha : a ∈ U
s : (a : ι) → Set (α a)
hs : ∀ (a_1 : ι), IsOpen[inst✝¹ a_1] (s a_1) ∧ a a_1 ∈ s a_1
hsU : univ.pi s ⊆ U
⊢ 0 < ∏ i, (μ i) (s i)

Tactic:
rw [CanonicallyOrderedAdd.prod_pos]

Goal state after:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), (μ i).IsOpenPosMeasure
U : Set ((i : ι) → α i)
U_open : IsOpen[Pi.topologicalSpace] U
a : (i : ι) → α i
ha : a ∈ U
s : (a : ι) → Set (α a)
hs : ∀ (a_1 : ι), IsOpen[inst✝¹ a_1] (s a_1) ∧ a a_1 ∈ s a_1
hsU : univ.pi s ⊆ U
⊢ ∀ i ∈ Finset.univ, 0 < (μ i) (s i)
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: case mpr
p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
⊢ q = 1 → p = ∞

Tactic:
rintro rfl
    rw [← inv_inv p, ← one_sub_inv 1 p]
    simp

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

Goal state before:
pp: p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < y - x
⊢ (y ^ p - x ^ p) / y ^ p < p * y ^ (p - 1) * (y - x) / y ^ p

Tactic:
_root_.sub_div,

Goal state after:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < y - x
⊢ y ^ p / y ^ p - x ^ p / y ^ p < p * y ^ (p - 1) * (y - x) / y ^ p
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < y - x
⊢ 1 + p * ((x - y) / y) < (1 + (x / y - 1)) ^ p

Tactic:
_root_.sub_div,

Goal state after:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < y - x
⊢ 1 + p * (x / y - y / y) < (1 + (x / y - 1)) ^ p
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
hf : f =ᵐ[μ] 0
⊢ eLpNorm f p μ = 0

Tactic:
rw [← eLpNorm_zero (p := p) (μ := μ) (α := α) (ε := ε)]
  exact eLpNorm_congr_ae hf

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

Goal state before:
pp: p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < z - y
⊢ p * y ^ (p - 1) * (z - y) / y ^ p < (z ^ p - y ^ p) / y ^ p

Tactic:
_root_.sub_div,

Goal state after:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < z - y
⊢ p * y ^ (p - 1) * (z - y) / y ^ p < z ^ p / y ^ p - y ^ p / y ^ p
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < z - y
⊢ 1 + p * ((z - y) / y) < (1 + (z / y - 1)) ^ p

Tactic:
_root_.sub_div,

Goal state after:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < z - y
⊢ 1 + p * (z / y - y / y) < (1 + (z / y - 1)) ^ p
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case pos
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
hmem : (ENNReal.ofReal p)⁻¹ ∈ Set.Ioo 0 1
⊢ (z₁ + z₂) ^ p ≤ (ENNReal.ofReal p)⁻¹.LpAddConst * (z₁ ^ p + z₂ ^ p)

Tactic:
rw [show LpAddConst (ENNReal.ofReal p)⁻¹ =
        (2 : ℝ≥0∞) ^ (1 / ((ENNReal.ofReal p)⁻¹).toReal - 1) by
      rw [LpAddConst, if_pos hmem]]

Goal state after:
case pos
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
hmem : (ENNReal.ofReal p)⁻¹ ∈ Set.Ioo 0 1
⊢ (z₁ + z₂) ^ p ≤ 2 ^ (1 / (ENNReal.ofReal p)⁻¹.toReal - 1) * (z₁ ^ p + z₂ ^ p)
Module: Mathlib.Analysis.MeanInequalities

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

Tactic:
by
  constructor
  · intro h
    by_contra! h_contra
    rw [(geom_mean_eq_arith_mean_weighted_iff_of_pos' s w z hw hw' hz).mpr ?_] at h
    · exact (lt_self_iff_false _).mp h
    · intro j hjs
      rw [← arith_mean_weighted_of_constant s w (fun _ => z j) (z j) hw' fun _ _ => congrFun rfl]
      apply sum_congr rfl (fun x a => congrArg (HMul.hMul (w x)) (h_contra j hjs x a))
  · rintro ⟨j, hjs, k, hks, hzjk⟩
    have := geom_mean_le_arith_mean_weighted s w z (fun i a => le_of_lt (hw i a)) hw' hz
    by_contra! h
    apply le_antisymm this at h
    apply (geom_mean_eq_arith_mean_weighted_iff_of_pos' s w z hw hw' hz).mp at h
    simp only [h j hjs, h k hks, ne_eq, not_true_eq_false] at hzjk

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case pos
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a = ∞ ∨ b = ∞
⊢ ∞ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹

Tactic:
rcases h with h | h <;> rw [h]

Goal state after:
case pos.inl
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a = ∞
⊢ ∞ = ∞ ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹

case pos.inr
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : b = ∞
⊢ ∞ = a ^ p * (ENNReal.ofReal p)⁻¹ + ∞ ^ q * (ENNReal.ofReal q)⁻¹
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 M

Tactic:
← hB.tsum_eq

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

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

Tactic:
rwa [h_tsum_B1] at h_sum

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
p : ℝ
hp : 1 ≤ p
f g : ι → ℝ≥0
A : ℝ≥0
hfA : HasSum (fun i ↦ ↑(f i) ^ p) (↑A ^ p)
B : ℝ≥0
hgB : HasSum (fun i ↦ ↑(g i) ^ p) (↑B ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A + ↑B ∧ HasSum (fun i ↦ ((fun i ↦ ↑(f i)) i + (fun i ↦ ↑(g i)) i) ^ p) (C ^ p)

Tactic:
norm_cast at hfA hgB

Goal state after:
ι : Type u
p : ℝ
hp : 1 ≤ p
f g : ι → ℝ≥0
A B : ℝ≥0
hfA : HasSum (fun a ↦ f a ^ p) (A ^ p)
hgB : HasSum (fun a ↦ g a ^ p) (B ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A + ↑B ∧ HasSum (fun i ↦ ((fun i ↦ ↑(f i)) i + (fun i ↦ ↑(g i)) i) ^ p) (C ^ p)
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
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N
n : ℕ
⊢ eLpNorm' (fun x ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i

Tactic:
let f_norm_diff i x := ‖f (i + 1) x - f i x‖
  have hgf_norm_diff :
    ∀ n,
      (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) =
        ∑ i ∈ Finset.range (n + 1), f_norm_diff i :=
    fun n => funext fun x => by simp [f_norm_diff]
  rw [hgf_norm_diff]
  refine (eLpNorm'_sum_le (fun i _ => ((hf (i + 1)).sub (hf i)).norm) hp1).trans ?_
  simp_rw [eLpNorm'_norm]
  refine (Finset.sum_le_sum ?_).trans <| ENNReal.sum_le_tsum _
  exact fun m _ => (h_cau m (m + 1) m (Nat.le_succ m) (le_refl m)).le

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
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h : ∀ (n : ℕ), ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
hp_pos : 0 < p
g : ℕ → ℝ≥0∞
⊢ liminf (fun n ↦ ∑ i ∈ Finset.range n, g i) atTop = liminf (fun n ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop

Tactic:
← liminf_nat_add _ 1

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h : ∀ (n : ℕ), ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
hp_pos : 0 < p
g : ℕ → ℝ≥0∞
⊢ liminf (fun i ↦ ∑ i ∈ Finset.range (i + 1), g i) atTop = liminf (fun n ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop
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
𝕜 : Type u_6
𝕜' : Type u_7
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜'
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' F✝
σ : 𝕜 →+* 𝕜'
inst✝⁴ : RingHomIsometric σ
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : G →L[𝕜] E →L[𝕜] F
c : 𝕜
g : G
f : ↥(Lp E p μ)
⊢ ↑↑((compLpₗ p μ (B (c • g))) f) =ᵐ[μ] ↑↑(((RingHom.id 𝕜) c • compLpₗ p μ (B g)) f)

Tactic:
filter_upwards [(c • B g).coeFn_compLp f, (B g).coeFn_compLp f,
      Lp.coeFn_smul c ((B g).compLp f)] with x hx hg hsmul

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✝
g✝ : E → F✝
c✝ : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜'
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' F✝
σ : 𝕜 →+* 𝕜'
inst✝⁴ : RingHomIsometric σ
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : G →L[𝕜] E →L[𝕜] F
c : 𝕜
g : G
f : ↥(Lp E p μ)
x : α
hx : ↑↑((c • B g).compLp f) x = (c • B g) (↑↑f x)
hg : ↑↑((B g).compLp f) x = (B g) (↑↑f x)
hsmul : ↑↑(c • (B g).compLp f) x = (c • ↑↑((B g).compLp f)) x
⊢ ↑↑((compLpₗ p μ (B (c • g))) f) x = ↑↑(((RingHom.id 𝕜) c • compLpₗ p μ (B g)) f) x
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst✝² : SeminormedAddGroup E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → E
g : α → E
C p : ℝ≥0∞
bound : ∀ᶠ (i : ι) in u, eLpNorm (f i) p μ ≤ C
h_tendsto : TendstoInMeasure μ f u g
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
⊢ eLpNorm g p μ ≤ C

Tactic:
obtain ⟨l, hl⟩ := h_tendsto.exists_seq_tendsto_ae'

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst✝² : SeminormedAddGroup E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → E
g : α → E
C p : ℝ≥0∞
bound : ∀ᶠ (i : ι) in u, eLpNorm (f i) p μ ≤ C
h_tendsto : TendstoInMeasure μ f u g
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
l : ℕ → ι
hl : Tendsto l atTop u ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ f (l i) x) atTop (𝓝 (g x))
⊢ eLpNorm g p μ ≤ C
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst✝ : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (fun n ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
⊢ TendstoInMeasure μ f l g

Tactic:
refine TendstoInMeasure.congr (fun i => (hf i).ae_eq_mk.symm) hg.ae_eq_mk.symm ?_
  refine tendstoInMeasure_of_tendsto_eLpNorm_of_stronglyMeasurable
    hp_ne_zero hp_ne_top (fun i => (hf i).stronglyMeasurable_mk) hg.stronglyMeasurable_mk ?_
  have : (fun n => eLpNorm ((hf n).mk (f n) - hg.mk g) p μ) = fun n => eLpNorm (f n - g) p μ := by
    ext1 n; refine eLpNorm_congr_ae (EventuallyEq.sub (hf n).ae_eq_mk.symm hg.ae_eq_mk.symm)
  rw [this]
  exact hfg

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: case neg
𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜₂
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (⇑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : ¬f x = 0
⊢ ‖x‖ ≤ ↑(ε⁻¹ * ‖c‖₊) * ‖f x‖

Tactic:
have hc₀ : c ≠ 0 := norm_pos_iff.1 (one_pos.trans hc)

Goal state after:
case neg
𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜₂
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (⇑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : ¬f x = 0
hc₀ : c ≠ 0
⊢ ‖x‖ ≤ ↑(ε⁻¹ * ‖c‖₊) * ‖f x‖
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
⊢ μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂

Tactic:
rcases eq_top_or_lt_top (μ (s₁ ∪ s₂)) with h | h
  · simp only [Measure.real, h, ENNReal.toReal_top]
    exact add_nonneg ENNReal.toReal_nonneg ENNReal.toReal_nonneg
  · have A : μ s₁ ≠ ∞ := measure_ne_top_of_subset subset_union_left h.ne
    have B : μ s₂ ≠ ∞ := measure_ne_top_of_subset subset_union_right h.ne
    simp only [Measure.real, ← ENNReal.toReal_add A B]
    exact ENNReal.toReal_mono (by simp [A, B]) (measure_union_le _ _)

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

Goal state before:
pp: 𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
G' : Type wG'
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : SeminormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
g : ContinuousMultilinearMap 𝕜 E G'
x✝ : ℝ≥0
⊢ ‖f.prod g‖₊ ≤ x✝ ↔ max ‖f‖₊ ‖g‖₊ ≤ x✝

Tactic:
simp only [opNNNorm_le_iff, prod_apply, Prod.nnnorm_def, max_le_iff, forall_and]

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

Goal state before:
pp: 𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹⁰ : Fintype ι'
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : SeminormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
inst✝ : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
m : (i : ι) → E i
x : G
⊢ ‖{ toFun := fun x ↦ (f x) m, map_add' := ⋯, map_smul' := ⋯ } x‖ ≤ ‖f‖ * ‖x‖ * ∏ i, ‖m i‖

Tactic:
exact (f x).le_of_opNorm_le (f.le_opNorm x) _

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

Goal state before:
pp: 𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹¹ : Fintype ι'
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : SeminormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
inst✝¹ : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
inst✝ : DecidableEq ι
m : (i : ι) → E i
i : ι
c : 𝕜
x : E i
⊢ { toFun := fun x_1 ↦ (f x_1) (update m i (c • x)), map_add' := ⋯, map_smul' := ⋯ }.mkContinuous
      (‖f‖ * ∏ i_1, ‖update m i (c • x) i_1‖) ⋯ =
    c •
      { toFun := fun x_1 ↦ (f x_1) (update m i x), map_add' := ⋯, map_smul' := ⋯ }.mkContinuous
        (‖f‖ * ∏ i_1, ‖update m i x i_1‖) ⋯

Tactic:
by
        ext1
        simp only [FunLike.coe_smul, ContinuousMultilinearMap.map_update_smul, LinearMap.coe_mk,
          LinearMap.mkContinuous_apply, Pi.smul_apply, AddHom.coe_mk]

Goal state after:
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:
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.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝ : NormedAddCommGroup β
T : Set α → β
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hs_zero : μ s = 0
⊢ T s = 0

Tactic:
by
  refine norm_eq_zero.mp ?_
  refine ((hT.2 s hs (by simp [hs_zero])).trans (le_of_eq ?_)).antisymm (norm_nonneg _)
  rw [measureReal_def, hs_zero, ENNReal.toReal_zero, mul_zero]

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

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : μ s ≠ ∞
hνs : ν s ≠ ∞
⊢ weightedSMul (μ + ν) s = weightedSMul μ s + weightedSMul ν s

Tactic:
by
  ext1 x
  push_cast
  simp_rw [Pi.add_apply, weightedSMul_apply]
  rw [measureReal_add_apply, add_smul]

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
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g // 0 ≤ g }
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)

Tactic:
have zero_mem : (0 : G) ∈ (range (g : α → G) ∪ {0} : Set G) ∩ { y | 0 ≤ y } := by
    simp only [union_singleton, mem_inter_iff, mem_insert_iff, true_or,
      mem_ofPred_eq, le_refl, and_self_iff]

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g // 0 ≤ g }
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
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
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g // 0 ≤ g }
this✝¹ : MeasurableSpace G := ⋯
this✝ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := ⋯
n : ℕ
a : α
A : (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y} ⊆ {y | 0 ≤ y}
⊢ (x n) a ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}

Tactic:
exact SimpleFunc.approxOn_mem g_meas _ n a

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable (⇑f) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
⊢ integral μ (map (ENNReal.toReal ∘ g) f) = ((map g f).lintegral μ).toReal

Tactic:
rw [map_integral f _ hf, map_lintegral, ENNReal.toReal_sum]

Goal state after:
α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable (⇑f) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
⊢ ∑ x ∈ f.range, μ.real (⇑f ⁻¹' {x}) • (ENNReal.toReal ∘ g) x = ∑ a ∈ f.range, (g a * μ (⇑f ⁻¹' {a})).toReal

α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable (⇑f) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
⊢ ∀ a ∈ f.range, g a * μ (⇑f ⁻¹' {a}) ≠ ∞

α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable (⇑f) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
⊢ (ENNReal.toReal ∘ g) 0 = 0