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

Goal state before:
pp: case pos
β : 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
⊢ Tendsto (fun n ↦ eLpNorm (⇑(approxOn f hf s y₀ h₀ n) - f) p μ) atTop (𝓝 0)

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
⊢ Tendsto (fun n ↦ eLpNorm (⇑(approxOn f hf s y₀ h₀ n) - f) p μ) atTop (𝓝 0)

Tactic:
·

Goal state after:
case pos
β : 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
⊢ Tendsto (fun n ↦ eLpNorm (⇑(approxOn f hf s y₀ h₀ n) - f) p μ) atTop (𝓝 0)
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case h₁
𝕜 : 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 ι
α : Type u_1
inst✝¹ : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : α ≃ ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : (i : { a // a ∉ s }) → E₁ ↑i
m : α → (i : ι) → E₁ i
⊢ ∏ i ∈ s.toFinsetᶜ, ‖if h : i ∈ s then m (e.symm ⟨i, ⋯⟩) i else x ⟨i, ⋯⟩‖ ≤ ∏ i, ‖x i‖

pp: case h₂
𝕜 : 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 ι
α : Type u_1
inst✝¹ : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : α ≃ ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : (i : { a // a ∉ s }) → E₁ ↑i
m : α → (i : ι) → E₁ i
⊢ ∏ i ∈ s.toFinset, ‖if h : i ∈ s then m (e.symm ⟨i, ⋯⟩) i else x ⟨i, ⋯⟩‖ ≤ ∏ i, ‖m i‖

Tactic:
·

Goal state after:
case h₁
𝕜 : 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 ι
α : Type u_1
inst✝¹ : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : α ≃ ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : (i : { a // a ∉ s }) → E₁ ↑i
m : α → (i : ι) → E₁ i
⊢ ∏ i ∈ s.toFinsetᶜ, ‖if h : i ∈ s then m (e.symm ⟨i, ⋯⟩) i else x ⟨i, ⋯⟩‖ ≤ ∏ i, ‖x i‖
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: case hf
X : Type u_1
E : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := ⋯
hK : IsCompact K
this : (K.indicator fun x ↦ g x • f x) = fun x ↦ g x • f x
⊢ Integrable (K.indicator f) μ

pp: case hφ
X : Type u_1
E : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := ⋯
hK : IsCompact K
this : (K.indicator fun x ↦ g x • f x) = fun x ↦ g x • f x
⊢ MemLp g ∞ μ

Tactic:
·

Goal state after:
case hf
X : Type u_1
E : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := ⋯
hK : IsCompact K
this : (K.indicator fun x ↦ g x • f x) = fun x ↦ g x • f x
⊢ Integrable (K.indicator f) μ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: case hφ
X : Type u_1
E : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := ⋯
hK : IsCompact K
this : (K.indicator fun x ↦ g x • f x) = fun x ↦ g x • f x
⊢ MemLp g ∞ μ

Tactic:
·

Goal state after:
case hφ
X : Type u_1
E : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := ⋯
hK : IsCompact K
this : (K.indicator fun x ↦ g x • f x) = fun x ↦ g x • f x
⊢ MemLp g ∞ μ
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case h₂
𝕜 : 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 ι
α : Type u_1
inst✝¹ : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : α ≃ ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : (i : { a // a ∉ s }) → E₁ ↑i
m : α → (i : ι) → E₁ i
⊢ ∏ i ∈ s.toFinset, ‖if h : i ∈ s then m (e.symm ⟨i, ⋯⟩) i else x ⟨i, ⋯⟩‖ ≤ ∏ i, ‖m i‖

Tactic:
·

Goal state after:
case h₂
𝕜 : 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 ι
α : Type u_1
inst✝¹ : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : α ≃ ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : (i : { a // a ∉ s }) → E₁ ↑i
m : α → (i : ι) → E₁ i
⊢ ∏ i ∈ s.toFinset, ‖if h : i ∈ s then m (e.symm ⟨i, ⋯⟩) i else x ⟨i, ⋯⟩‖ ≤ ∏ i, ‖m i‖
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case h₁
𝕜 : 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 ι
α : Type u_1
inst✝¹ : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : α ≃ ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : (i : ι) → E₁ i
⊢ ‖f.iteratedFDerivComponent e‖ ≤ ‖f‖

pp: case h1
𝕜 : 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 ι
α : Type u_1
inst✝¹ : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : α ≃ ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : (i : ι) → E₁ i
i : { a // a ∉ s }
a✝ : i ∈ univ
⊢ ‖x ↑i‖ ≤ ‖x‖

Tactic:
·

Goal state after:
case h₁
𝕜 : 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 ι
α : Type u_1
inst✝¹ : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : α ≃ ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : (i : ι) → E₁ i
⊢ ‖f.iteratedFDerivComponent e‖ ≤ ‖f‖
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case h1
𝕜 : 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 ι
α : Type u_1
inst✝¹ : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : α ≃ ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : (i : ι) → E₁ i
i : { a // a ∉ s }
a✝ : i ∈ univ
⊢ ‖x ↑i‖ ≤ ‖x‖

Tactic:
·

Goal state after:
case h1
𝕜 : 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 ι
α : Type u_1
inst✝¹ : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : α ≃ ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : (i : ι) → E₁ i
i : { a // a ∉ s }
a✝ : i ∈ univ
⊢ ‖x ↑i‖ ≤ ‖x‖
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: case hφ
X : Type u_1
E : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := ⋯
hK : IsCompact K
this : (K.indicator fun x ↦ f x • g x) = fun x ↦ f x • g x
⊢ Integrable (K.indicator f) μ

pp: case hf
X : Type u_1
E : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := ⋯
hK : IsCompact K
this : (K.indicator fun x ↦ f x • g x) = fun x ↦ f x • g x
⊢ MemLp g ∞ μ

Tactic:
·

Goal state after:
case hφ
X : Type u_1
E : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := ⋯
hK : IsCompact K
this : (K.indicator fun x ↦ f x • g x) = fun x ↦ f x • g x
⊢ Integrable (K.indicator f) μ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: case hf
X : Type u_1
E : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := ⋯
hK : IsCompact K
this : (K.indicator fun x ↦ f x • g x) = fun x ↦ f x • g x
⊢ MemLp g ∞ μ

Tactic:
·

Goal state after:
case hf
X : Type u_1
E : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := ⋯
hK : IsCompact K
this : (K.indicator fun x ↦ f x • g x) = fun x ↦ f x • g x
⊢ MemLp g ∞ μ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: case mp
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
⊢ Integrable f μ → (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ

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

Goal state after:
case mp
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
⊢ Integrable f μ → (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ
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:
·

Goal state after:
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 μ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: case mp
X : Type u_1
ε : Type u_3
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace ε
inst✝⁴ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝³ : PseudoMetrizableSpace ε
inst✝² : LinearOrder X
inst✝¹ : OrderTop X
inst✝ : CompactIccSpace X
⊢ Integrable f μ → IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ

pp: case mpr
X : Type u_1
ε : Type u_3
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace ε
inst✝⁴ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝³ : PseudoMetrizableSpace ε
inst✝² : LinearOrder X
inst✝¹ : OrderTop X
inst✝ : CompactIccSpace X
⊢ IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ → Integrable f μ

Tactic:
·

Goal state after:
case mp
X : Type u_1
ε : Type u_3
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace ε
inst✝⁴ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝³ : PseudoMetrizableSpace ε
inst✝² : LinearOrder X
inst✝¹ : OrderTop X
inst✝ : CompactIccSpace X
⊢ Integrable f μ → IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: case mpr
X : Type u_1
ε : Type u_3
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace ε
inst✝⁴ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝³ : PseudoMetrizableSpace ε
inst✝² : LinearOrder X
inst✝¹ : OrderTop X
inst✝ : CompactIccSpace X
⊢ IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ → Integrable f μ

Tactic:
·

Goal state after:
case mpr
X : Type u_1
ε : Type u_3
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace ε
inst✝⁴ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝³ : PseudoMetrizableSpace ε
inst✝² : LinearOrder X
inst✝¹ : OrderTop X
inst✝ : CompactIccSpace X
⊢ IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ → Integrable f μ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: case mp
X : Type u_1
ε : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝⁴ : PseudoMetrizableSpace ε
a : X
inst✝³ : LinearOrder X
inst✝² : CompactIccSpace X
inst✝¹ : NoMinOrder X
inst✝ : OrderTopology X
⊢ IntegrableOn f (Iio a) μ →
    IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f (𝓝[<] a) μ ∧ LocallyIntegrableOn f (Iio a) μ

pp: case mpr
X : Type u_1
ε : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝⁴ : PseudoMetrizableSpace ε
a : X
inst✝³ : LinearOrder X
inst✝² : CompactIccSpace X
inst✝¹ : NoMinOrder X
inst✝ : OrderTopology X
⊢ IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f (𝓝[<] a) μ ∧ LocallyIntegrableOn f (Iio a) μ →
    IntegrableOn f (Iio a) μ

Tactic:
·

Goal state after:
case mp
X : Type u_1
ε : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝⁴ : PseudoMetrizableSpace ε
a : X
inst✝³ : LinearOrder X
inst✝² : CompactIccSpace X
inst✝¹ : NoMinOrder X
inst✝ : OrderTopology X
⊢ IntegrableOn f (Iio a) μ →
    IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f (𝓝[<] a) μ ∧ LocallyIntegrableOn f (Iio a) μ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: case mpr
X : Type u_1
ε : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝⁴ : PseudoMetrizableSpace ε
a : X
inst✝³ : LinearOrder X
inst✝² : CompactIccSpace X
inst✝¹ : NoMinOrder X
inst✝ : OrderTopology X
⊢ IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f (𝓝[<] a) μ ∧ LocallyIntegrableOn f (Iio a) μ →
    IntegrableOn f (Iio a) μ

Tactic:
·

Goal state after:
case mpr
X : Type u_1
ε : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝⁴ : PseudoMetrizableSpace ε
a : X
inst✝³ : LinearOrder X
inst✝² : CompactIccSpace X
inst✝¹ : NoMinOrder X
inst✝ : OrderTopology X
⊢ IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f (𝓝[<] a) μ ∧ LocallyIntegrableOn f (Iio a) μ →
    IntegrableOn f (Iio a) μ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: case inl
X : Type u_1
E : Type u_6
inst✝⁹ : MeasurableSpace X
inst✝⁸ : TopologicalSpace X
inst✝⁷ : NormedAddCommGroup E
μ : Measure X
inst✝⁶ : BorelSpace X
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : ConditionallyCompleteLinearOrder E
inst✝³ : OrderTopology X
inst✝² : OrderTopology E
inst✝¹ : SecondCountableTopology E
p : ℝ≥0∞
f : X → E
inst✝ : IsFiniteMeasureOnCompacts μ
hs : IsCompact ∅
hmono : MonotoneOn f ∅
⊢ MemLp f p (μ.restrict ∅)

pp: case inr
X : Type u_1
E : Type u_6
inst✝⁹ : MeasurableSpace X
inst✝⁸ : TopologicalSpace X
inst✝⁷ : NormedAddCommGroup E
μ : Measure X
s : Set X
inst✝⁶ : BorelSpace X
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : ConditionallyCompleteLinearOrder E
inst✝³ : OrderTopology X
inst✝² : OrderTopology E
inst✝¹ : SecondCountableTopology E
p : ℝ≥0∞
f : X → E
inst✝ : IsFiniteMeasureOnCompacts μ
hs : IsCompact s
hmono : MonotoneOn f s
h : s.Nonempty
⊢ MemLp f p (μ.restrict s)

Tactic:
·

Goal state after:
case inl
X : Type u_1
E : Type u_6
inst✝⁹ : MeasurableSpace X
inst✝⁸ : TopologicalSpace X
inst✝⁷ : NormedAddCommGroup E
μ : Measure X
inst✝⁶ : BorelSpace X
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : ConditionallyCompleteLinearOrder E
inst✝³ : OrderTopology X
inst✝² : OrderTopology E
inst✝¹ : SecondCountableTopology E
p : ℝ≥0∞
f : X → E
inst✝ : IsFiniteMeasureOnCompacts μ
hs : IsCompact ∅
hmono : MonotoneOn f ∅
⊢ MemLp f p (μ.restrict ∅)
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: case inr
X : Type u_1
E : Type u_6
inst✝⁹ : MeasurableSpace X
inst✝⁸ : TopologicalSpace X
inst✝⁷ : NormedAddCommGroup E
μ : Measure X
s : Set X
inst✝⁶ : BorelSpace X
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : ConditionallyCompleteLinearOrder E
inst✝³ : OrderTopology X
inst✝² : OrderTopology E
inst✝¹ : SecondCountableTopology E
p : ℝ≥0∞
f : X → E
inst✝ : IsFiniteMeasureOnCompacts μ
hs : IsCompact s
hmono : MonotoneOn f s
h : s.Nonempty
⊢ MemLp f p (μ.restrict s)

Tactic:
·

Goal state after:
case inr
X : Type u_1
E : Type u_6
inst✝⁹ : MeasurableSpace X
inst✝⁸ : TopologicalSpace X
inst✝⁷ : NormedAddCommGroup E
μ : Measure X
s : Set X
inst✝⁶ : BorelSpace X
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : ConditionallyCompleteLinearOrder E
inst✝³ : OrderTopology X
inst✝² : OrderTopology E
inst✝¹ : SecondCountableTopology E
p : ℝ≥0∞
f : X → E
inst✝ : IsFiniteMeasureOnCompacts μ
hs : IsCompact s
hmono : MonotoneOn f s
h : s.Nonempty
⊢ MemLp f p (μ.restrict s)
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
⊢ (∀ i ∈ ∅, μ (S i) ≠ ∞) → (∀ i ∈ ∅, ∀ j ∈ ∅, i ≠ j → Disjoint (S i) (S j)) → T (⋃ i ∈ ∅, S i) = ∑ i ∈ ∅, T (S i)

pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ((∀ i ∈ s, μ (S i) ≠ ∞) →
          (∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)) → T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)) →
        (∀ i ∈ insert a s, μ (S i) ≠ ∞) →
          (∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)) →
            T (⋃ i ∈ insert a s, S i) = ∑ i ∈ insert a s, T (S i)

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
⊢ (∀ i ∈ ∅, μ (S i) ≠ ∞) → (∀ i ∈ ∅, ∀ j ∈ ∅, i ≠ j → Disjoint (S i) (S j)) → T (⋃ i ∈ ∅, S i) = ∑ i ∈ ∅, T (S i)