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

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

Tactic:
have h_rpow_surj := (ENNReal.rpow_left_bijective hq_pos.ne.symm).2

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

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
c : ℝ≥0∞
hc : c ≠ 0
f : α → ε
p : ℝ≥0∞
μ : Measure α
hp0 : ¬p = 0
hp_top : p = ∞
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

pp: case neg
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
c : ℝ≥0∞
hc : c ≠ 0
f : α → ε
p : ℝ≥0∞
μ : Measure α
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Tactic:
· simp [*]

Goal state after:
case neg
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
c : ℝ≥0∞
hc : c ≠ 0
f : α → ε
p : ℝ≥0∞
μ : Measure α
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: case refine_2
p q r : ℝ≥0
hr : r ≠ 0
h : p.HolderTriple q r
⊢ (↑p).HolderTriple ↑q ↑r

Tactic:
rw [holderTriple_iff]

Goal state after:
case refine_2
p q r : ℝ≥0
hr : r ≠ 0
h : p.HolderTriple q r
⊢ (↑p)⁻¹ + (↑q)⁻¹ = (↑r)⁻¹
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case e'_3
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
⊢ (z₁ + z₂) ^ p = (1 / 2 * (2 * z₁) + 1 / 2 * (2 * z₂)) ^ p

Tactic:
simp [← mul_assoc, ENNReal.inv_mul_cancel two_ne_zero ofNat_ne_top]

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

Goal state before:
pp: case neg
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p q : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun x ↦ 1
h_rw : ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ = ∫⁻ (a : α), (‖f a‖ₑ * g a) ^ p ∂μ
r : ℝ := p * q / (q - p)
hpqr : 1 / p = 1 / q + 1 / r
⊢ (∫⁻ (a : α), (‖f a‖ₑ * g a) ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) * μ Set.univ ^ (1 / p - 1 / q)

Tactic:
calc
    (∫⁻ a : α, (‖f a‖ₑ * g a) ^ p ∂μ) ^ (1 / p) ≤
        (∫⁻ a : α, ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) * (∫⁻ a : α, g a ^ r ∂μ) ^ (1 / r) :=
      ENNReal.lintegral_Lp_mul_le_Lq_mul_Lr hp0_lt hpq hpqr μ hf.enorm aemeasurable_const
    _ = (∫⁻ a : α, ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) * μ Set.univ ^ (1 / p - 1 / q) := by
      rw [hpqr]; simp [r, g]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

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

Tactic:
by
  obtain rfl | hp := hp.eq_or_lt
  · simp
  calc
    _ = ∑ i ∈ s, w i ^ (1 - p⁻¹) * (w i ^ p⁻¹ * f i) := ?_
    _ ≤ (∑ i ∈ s, (w i ^ (1 - p⁻¹)) ^ (1 - p⁻¹)⁻¹) ^ (1 / (1 - p⁻¹)⁻¹) *
          (∑ i ∈ s, (w i ^ p⁻¹ * f i) ^ p) ^ (1 / p) :=
        inner_le_Lp_mul_Lq _ _ _ (.symm <| Real.holderConjugate_iff.mpr ⟨hp, by simp⟩)
    _ = _ := ?_
  · congr with i
    rw [← mul_assoc, ← rpow_of_add_eq _ one_ne_zero, rpow_one]
    simp
  · have hp₀ : p ≠ 0 := by positivity
    have hp₁ : 1 - p⁻¹ ≠ 0 := by simp [sub_eq_zero, hp.ne']
    simp [mul_rpow, div_inv_eq_mul, one_mul, one_div, hp₀, hp₁]

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
inst✝¹ : Nonempty ι
inst✝ : SemilatticeSup ι
hp : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
⊢ CauchySeq f ↔ Tendsto (fun n ↦ eLpNorm (↑↑(f n.1) - ↑↑(f n.2)) p μ) atTop (𝓝 0)

Tactic:
simp_rw [cauchySeq_iff_tendsto_dist_atTop_0, dist_def]
  rw [← ENNReal.toReal_zero, ENNReal.tendsto_toReal_iff (fun n => ?_) ENNReal.zero_ne_top]
  rw [eLpNorm_congr_ae (Lp.coeFn_sub _ _).symm]
  exact eLpNorm_ne_top _

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
⊢ MemLp (fun x ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ

Tactic:
by
  refine ⟨(hf.1.enorm.pow_const q.toReal).aestronglyMeasurable, ?_⟩
  by_cases q_top : q = ∞
  · simp [q_top]
  by_cases q_zero : q = 0
  · simp only [q_zero, ENNReal.toReal_zero]
    by_cases p_zero : p = 0
    · simp [p_zero]
    rw [ENNReal.div_zero p_zero]
    simpa only [ENNReal.rpow_zero, eLpNorm_exponent_top] using (memLp_top_const_enorm (by simp)).2
  rw [eLpNorm_enorm_rpow _ (ENNReal.toReal_pos q_zero q_top)]
  apply ENNReal.rpow_lt_top_of_nonneg ENNReal.toReal_nonneg
  rw [ENNReal.ofReal_toReal q_top, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top,
    mul_one]
  exact hf.2.ne

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
f : ↥(Lp E p μ)
⊢ MemLp (↑(AEEqFun.comp g ⋯ ↑f)) p μ

Tactic:
exact (hg.comp_memLp g0 (Lp.memLp f)).ae_eq (AEEqFun.coeFn_comp _ hg.continuous _).symm

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

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoEMetricSpace E
inst✝ : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
h1 :
  ∀ (ns : ℕ → ℕ),
    StrictMono ns → ∃ ns', StrictMono ns' ∧ ∀ᵐ (ω : α) ∂μ, Tendsto (fun i ↦ f (ns (ns' i)) ω) atTop (𝓝 (g ω))
⊢ ∀ (ε : ℝ≥0∞), 0 < ε → Tendsto (fun i ↦ (μ {x | ε ≤ edist (f i x) (g x)}).toNNReal) atTop (𝓝 0)

Tactic:
by_contra! ⟨ε, hε, h2⟩

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoEMetricSpace E
inst✝ : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
h1 :
  ∀ (ns : ℕ → ℕ),
    StrictMono ns → ∃ ns', StrictMono ns' ∧ ∀ᵐ (ω : α) ∂μ, Tendsto (fun i ↦ f (ns (ns' i)) ω) atTop (𝓝 (g ω))
ε : ℝ≥0∞
hε : 0 < ε
h2 : ¬Tendsto (fun i ↦ (μ {x | ε ≤ edist (f i x) (g x)}).toNNReal) atTop (𝓝 0)
⊢ False
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 : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ eLpNorm f_lim p μ < ∞

Tactic:
rw [h_add]

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ eLpNorm (f_lim - f N + f N) p μ < ∞
Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : V ∈ 𝓝 0
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x✝ : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁷, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), t i ∈ 𝓝 0
hft : (↑I).pi t ⊆ ⇑f ⁻¹' V
c : ι → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : ∏ i ∈ I, c i ≠ 0
a : 𝕜
ha : a ∈ {y | ‖y‖ < ‖∏ i ∈ I, c i‖}
x : (i : ι) → E i
hx : x ∈ s
i₀ : ι
y : (i : ι) → E i := I.piecewise (fun i ↦ c i • x i) x
i : ι
hi : i ∈ ↑I
⊢ update y i₀ ((a / ∏ i ∈ I, c i) • y i₀) i ∈ t i

Tactic:
by
        rcases eq_or_ne i i₀ with rfl | hne
        · simp_rw [update_self, y, I.piecewise_eq_of_mem _ _ hi, smul_smul]
          refine hc _ _ ?_ _ hx
          calc
            ‖(a / ∏ i ∈ I, c i) * c i‖ ≤ (‖∏ i ∈ I, c i‖ / ‖∏ i ∈ I, c i‖) * ‖c i‖ := by
              rw [norm_mul, norm_div]; gcongr; exact ha.out.le
            _ ≤ 1 * ‖c i‖ := by gcongr; apply div_self_le_one
            _ = ‖c i‖ := one_mul _
        · simp_rw [update_of_ne hne, y, I.piecewise_eq_of_mem _ _ hi]
          exact hc _ _ le_rfl _ hx

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
a✝ : Nontrivial R
t : R
ht : ‖t‖ < ‖↑x⁻¹‖⁻¹
⊢ (↑(x.add t ht))⁻¹ʳ = (1 + ↑x⁻¹ * t)⁻¹ʳ * ↑x⁻¹

Tactic:
inverse_unit,

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
a✝ : Nontrivial R
t : R
ht : ‖t‖ < ‖↑x⁻¹‖⁻¹
⊢ ↑(x.add t ht)⁻¹ = (1 + ↑x⁻¹ * t)⁻¹ʳ * ↑x⁻¹
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
hst : s ⊆ t
ε : ℝ
ht' : μ t ≠ ∞
⊢ μ.real (t \ s) ≤ ε ↔ μ.real t ≤ μ.real s + ε

Tactic:
measureReal_sdiff hst hs ht',

Goal state after:
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
hst : s ⊆ t
ε : ℝ
ht' : μ t ≠ ∞
⊢ μ.real t - μ.real s ≤ ε ↔ μ.real t ≤ μ.real s + ε
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
ι : Type u_3
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : μ.real univ < ∑ i ∈ s, μ.real (t i)
⊢ μ univ < ∑ i ∈ s, μ (t i)

Tactic:
simp only [Measure.real] at H

Goal state after:
α : Type u_1
ι : Type u_3
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (μ univ).toReal < ∑ i ∈ s, (μ (t i)).toReal
⊢ μ univ < ∑ i ∈ s, μ (t i)
Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator

Goal state before:
pp: case refine_2
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hfg : MemLp (f + g) p μ
⊢ MemLp g p μ

Tactic:
rw [← Set.indicator_add_eq_right h]; exact hfg.indicator (measurableSet_support hg.measurable)

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

Goal state before:
pp: case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
h : Integrable f μ
hne : μ ≠ 0
⊢ Integrable f ((μ univ)⁻¹ • μ)

Tactic:
apply h.smul_measure
    simpa

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
s t : Set α
μ : Measure α
ε' : Type u_7
inst✝² : TopologicalSpace ε'
inst✝¹ : ENormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
ht : NullMeasurableSet t μ
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
⊢ IntegrableOn f t μ

Tactic:
have hu : IntegrableOn f u μ := hf.mono_set fun x hx => hx.1

Goal state after:
α : Type u_1
mα : MeasurableSpace α
s t : Set α
μ : Measure α
ε' : Type u_7
inst✝² : TopologicalSpace ε'
inst✝¹ : ENormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
ht : NullMeasurableSet t μ
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u μ
⊢ IntegrableOn f t μ
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᵐ[μ] f
h_le₂ : f ≤ᵐ[μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
h_le_add : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖
⊢ Integrable f μ

Tactic:
exact Integrable.mono (by fun_prop) hf h_le_add

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : ¬AEStronglyMeasurable (fun x ↦ ↑(f x) • g x) μ
⊢ Integrable g (μ.withDensity fun x ↦ ↑(f x)) ↔ Integrable (fun x ↦ ↑(f x) • g x) μ

Tactic:
· simp only [Integrable, aestronglyMeasurable_withDensity_iff hf, H, false_and]

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

Goal state before:
pp: α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
l : Filter α
t : Set α
ht : t ∈ l
u : Set α
hu : u ∈ ae μ
hf : IntegrableOn f (t ∩ u) μ
⊢ IntegrableAtFilter f l μ

Tactic:
refine ⟨t, ht, hf.congr_set_ae <| eventuallyEq_set.2 ?_⟩

Goal state after:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
l : Filter α
t : Set α
ht : t ∈ l
u : Set α
hu : u ∈ ae μ
hf : IntegrableOn f (t ∩ u) μ
⊢ ∀ᵐ (x : α) ∂μ, x ∈ t ↔ x ∈ t ∩ u
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_meas_ae : AEStronglyMeasurable f (μ'.trim hm)
hf : HasFiniteIntegral f (μ'.trim hm)
⊢ HasFiniteIntegral f μ'

Tactic:
simpa [HasFiniteIntegral, lintegral_trim_ae hm hf_meas_ae.enorm] using hf

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

Goal state before:
pp: X : Type u_1
ε : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f g : X → ε
μ : Measure X
s : Set X
h : f =ᵐ[μ.restrict s] g
hf : LocallyIntegrableOn f s μ
⊢ LocallyIntegrableOn g s μ

Tactic:
by
  intro x hx
  obtain ⟨t, hxt, hft⟩ := hf x hx
  refine ⟨s ∩ t, inter_mem self_mem_nhdsWithin hxt, ?_⟩
  refine (hft.mono_set inter_subset_right).congr ?_
  refine h.filter_mono ?_
  gcongr
  exact inter_subset_left

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

Goal state before:
pp: X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
T : Set (Set X)
T_count : T.Countable
T_open : ∀ u ∈ T, IsOpen[inst✝³] u
sT : s ⊆ ⋃ u ∈ T, u
hT : ∀ u ∈ T, IntegrableOn f (u ∩ s) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
⊢ ∃ u, (∀ (n : ℕ), IsOpen[inst✝³] (u n)) ∧ s ⊆ ⋃ n, u n ∧ ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ

Tactic:
refine ⟨u, ?_, ?_, ?_⟩

Goal state after:
case refine_1
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
T : Set (Set X)
T_count : T.Countable
T_open : ∀ u ∈ T, IsOpen[inst✝³] u
sT : s ⊆ ⋃ u ∈ T, u
hT : ∀ u ∈ T, IntegrableOn f (u ∩ s) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
⊢ ∀ (n : ℕ), IsOpen[inst✝³] (u n)

case refine_2
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
T : Set (Set X)
T_count : T.Countable
T_open : ∀ u ∈ T, IsOpen[inst✝³] u
sT : s ⊆ ⋃ u ∈ T, u
hT : ∀ u ∈ T, IntegrableOn f (u ∩ s) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
⊢ s ⊆ ⋃ n, u n

case refine_3
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
T : Set (Set X)
T_count : T.Countable
T_open : ∀ u ∈ T, IsOpen[inst✝³] u
sT : s ⊆ ⋃ u ∈ T, u
hT : ∀ u ∈ T, IntegrableOn f (u ∩ s) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
⊢ ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
ε : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst✝¹ : PseudoMetrizableSpace ε
inst✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : ℕ → Set X
su : s ⊆ ⋃ n, u n
hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ
⊢ s = ⋃ n, u n ∩ s

Tactic:
← iUnion_inter

Goal state after:
X : Type u_1
ε : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst✝¹ : PseudoMetrizableSpace ε
inst✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
u : ℕ → Set X
su : s ⊆ ⋃ n, u n
hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ
⊢ s = (⋃ i, u i) ∩ s
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: case refine_1
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
h : LocallyIntegrable f (Measure.map (⇑e) μ)
x : X
⊢ IntegrableAtFilter (f ∘ ⇑e) (𝓝 x) μ

Tactic:
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

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

Goal state before:
pp: X : Type u_1
R : Type u_8
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
μ : Measure X
inst✝⁴ : OpensMeasurableSpace X
inst✝³ : LocallyCompactSpace X
inst✝² : T2Space X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
f g : X → R
s : Set X
hf : LocallyIntegrableOn f s μ
hg : ContinuousOn g s
hs : IsLocallyClosed s
⊢ LocallyIntegrableOn (fun x ↦ g x * f x) s μ

Tactic:
rw [MeasureTheory.locallyIntegrableOn_iff hs] at hf ⊢
  exact fun k hk_sub hk_c => (hf k hk_sub hk_c).continuousOn_mul (hg.mono hk_sub) hk_c

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_6
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝³ : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
inst✝² : SeminormedAddGroup 𝕜
inst✝¹ : DistribSMul 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
hT : DominatedFinMeasAdditive μ T C
c : 𝕜
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ‖c‖ * ‖T s‖ ≤ ‖c‖ * C * μ.real s

Tactic:
rw [mul_assoc]

Goal state after:
α : Type u_1
𝕜 : Type u_6
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝³ : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
inst✝² : SeminormedAddGroup 𝕜
inst✝¹ : DistribSMul 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
hT : DominatedFinMeasAdditive μ T C
c : 𝕜
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ‖c‖ * ‖T s‖ ≤ ‖c‖ * (C * μ.real s)
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : 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 : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : ∀ (y : E), y ≠ 0 → μ (⇑g ⁻¹' {y}) < ∞
x : E
hx_ne : x ≠ 0
⊢ μ (⇑g ⁻¹' {-x}) < ∞

Tactic:
refine hg (-x) ?_

Goal state after:
α : 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 : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : ∀ (y : E), y ≠ 0 → μ (⇑g ⁻¹' {y}) < ∞
x : E
hx_ne : x ≠ 0
⊢ -x ≠ 0
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝⁶ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : CompleteSpace E
c : 𝕜
f : ↥(Lp E 1 μ)
⊢ integral (c • f) = c • integral f

Tactic:
integral_eq' 𝕜 f,

Goal state after:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝⁶ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : CompleteSpace E
c : 𝕜
f : ↥(Lp E 1 μ)
⊢ integral (c • f) = c • (integralCLM' 𝕜) f
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace E
f : α →ₛ E
hfi : Integrable (⇑f) μ
⊢ integral μ f = L1.integral ↑(f.toLp ⋯)

Tactic:
L1.SimpleFunc.integral_L1_eq_integral,

Goal state after:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace E
f : α →ₛ E
hfi : Integrable (⇑f) μ
⊢ integral μ f = L1.SimpleFunc.integral (f.toLp ⋯)
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case cons
α : Type u_1
ι : Type u_2
β : Type u_3
inst✝ : NormedField β
l : Filter α
f g : ι → α → β
i : ι
L : List ι
ihL :
  (∀ i ∈ L, f i ~[l] g i) →
    (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) L).prod) ~[l] fun x ↦ (List.map (fun x_1 ↦ g x_1 x) L).prod
h : ∀ i_1 ∈ i :: L, f i_1 ~[l] g i_1
⊢ (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) (i :: L)).prod) ~[l] fun x ↦ (List.map (fun x_1 ↦ g x_1 x) (i :: L)).prod

Tactic:
simp only [List.forall_mem_cons, List.map_cons, List.prod_cons] at h ⊢
    exact h.1.mul (ihL h.2)

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : IsOrderedModule ℝ E
inst✝¹ : ClosedIciTopology E
β : Type u_6
inst✝ : Preorder β
f : α → β → E
s : Set β
hf_mono : ∀ᵐ (x : α) ∂μ, MonotoneOn (f x) s
hf_int : ∀ a ∈ s, Integrable (fun x ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
hab : a ≤ b
⊢ (fun x ↦ f x a) ≤ᵐ[μ] fun x ↦ f x b

Tactic:
filter_upwards [hf_mono] with x hx

Goal state after:
α : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : IsOrderedModule ℝ E
inst✝¹ : ClosedIciTopology E
β : Type u_6
inst✝ : Preorder β
f : α → β → E
s : Set β
hf_mono : ∀ᵐ (x : α) ∂μ, MonotoneOn (f x) s
hf_int : ∀ a ∈ s, Integrable (fun x ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
hab : a ≤ b
x : α
hx : MonotoneOn (f x) s
⊢ f x a ≤ f x b