mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsFiniteMeasure μ
h₁ : NullMeasurableSet s μ
⊢ μ.real sᶜ = μ.real univ - μ.real s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ.real s₂ ≤ μ.real s₁
ht : t₁ ⊆ t₂
htμ : μ.real t₂ ≤ μ.real t₁
h₁ : μ s₂ ≠ ∞
h₂ : μ t₂ ≠ ∞
⊢ μ.real (s₁ ∪ t₁) = μ.real (s₂ ∪ t₂)

Tactic:
by

Goal state after:
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 : (↑s).PairwiseDisjoint t
⊢ ∀ a ∈ s, μ (t a) ≠ ∞

Tactic:
by

Goal state after:
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 : (↑s).PairwiseDisjoint t
⊢ μ univ ≠ ∞

Tactic:
by

Goal state after:
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 : (↑s).PairwiseDisjoint t
⊢ ∑ i ∈ s, μ.real (t i) ≤ μ.real univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
s : Set α
μ₁ μ₂ : Measure α
h₁ : μ₁ s ≠ ∞
h₂ : μ₂ s ≠ ∞
⊢ (μ₁ + μ₂).real s = μ₁.real s + μ₂.real s

Tactic:
by

Goal state after:
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 : (μ univ).toReal < ∑ i ∈ s, (μ (t i)).toReal
⊢ μ univ ≠ ∞

Tactic:
by

Goal state after:
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 : (μ univ).toReal < ∑ i ∈ s, (μ (t i)).toReal
⊢ ∀ a ∈ s, μ (t a) ≠ ∞

Tactic:
by

Goal state after:
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)
⊢ ∃ i ∈ s, ∃ j ∈ s, ∃ (_ : i ≠ j), (t i ∩ t j).Nonempty

Tactic:
by

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 ≠ ∞
⊢ (s ∩ t).Nonempty

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsProbabilityMeasure μ
h : NullMeasurableSet s μ
⊢ μ.real sᶜ = 1 - μ.real s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IndicatorFunction

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f g : α → M
l : Filter α
hf : f =ᶠ[l ⊓ 𝓟 s] g
hs : s =ᶠ[l] t
x : α
hst : x ∈ s ↔ x ∈ t
hfg : x ∈ s → f x = g x
hxs : x ∈ s
⊢ s.mulIndicator f x = t.mulIndicator g x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IndicatorFunction

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f g : α → M
l : Filter α
hf : f =ᶠ[l ⊓ 𝓟 s] g
hs : s =ᶠ[l] t
x : α
hst : x ∈ s ↔ x ∈ t
hfg : x ∈ s → f x = g x
hxs : x ∉ s
⊢ s.mulIndicator f x = t.mulIndicator g x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IndicatorFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : One β
s : ι → Set α
hs : Monotone s
f : α → β
a : α
⊢ (fun i ↦ (s i).mulIndicator f a) =ᶠ[atTop] fun x ↦ (⋃ i, s i).mulIndicator f a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IndicatorFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : One β
s : ι → Set α
hs : Antitone s
f : α → β
a : α
⊢ (fun i ↦ (s i).mulIndicator f a) =ᶠ[atTop] fun x ↦ (⋂ i, s i).mulIndicator f a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IndicatorFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_5
inst✝ : One β
s : ι → Set α
f : α → β
a : α
⊢ (fun n ↦ (⋃ i ∈ n, s i).mulIndicator f a) =ᶠ[atTop] fun x ↦ (iUnion s).mulIndicator f a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IndicatorFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : One β
l : Filter α
f : α → β
s : Set α
hf : f =ᶠ[l] 1
⊢ s.mulIndicator 1 =ᶠ[l] 1

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IndicatorFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : One β
l : Filter α
f : α → β
hf : ∀ᶠ (x : α) in l, f x ≠ 1
s✝ t : Set α
h : s✝.mulIndicator f =ᶠ[l] t.mulIndicator f
s : Set α
⊢ Function.mulSupport (s.mulIndicator f) =ᶠ[l] s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IndicatorFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : One β
l : Filter α
f : α → β
hf : ∀ᶠ (x : α) in l, f x ≠ 1
s t : Set α
h : s.mulIndicator f =ᶠ[l] t.mulIndicator f
⊢ s =ᶠ[l] t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
hp : 0 ≠ ∞
s : Set α
x✝ : μ s ≤ ↑1
⊢ eLpNorm (s.indicator fun x ↦ c) 0 μ ≤ ε

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
⊢ Tendsto (fun x ↦ ↑(‖c‖₊ * x ^ (1 / p.toReal))) (𝓝 0) (𝓝 ↑0)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
⊢ ∃ η, 0 < η ∧ ‖c‖ₑ * ↑η ^ (1 / p.toReal) ≤ ε

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ η, 0 < η ∧ ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun x ↦ c) p μ ≤ ε

Tactic:
by

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

Goal state before:
pp: E : Type u_2
p : ℝ≥0∞
inst✝³ : NormedAddCommGroup E
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasureOnCompacts μ
f : X → E
hf : HasCompactSupport f
h2f : AEStronglyMeasurable f μ
C : ℝ
hfC : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
⊢ MemLp f p μ

Tactic:
by

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

Goal state before:
pp: E : Type u_2
p : ℝ≥0∞
inst✝³ : NormedAddCommGroup E
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasureOnCompacts μ
f : X → E
hf : HasCompactSupport f
h2f : AEStronglyMeasurable f μ
C : ℝ≥0∞
hfC : ∀ᵐ (x : X) ∂μ, ‖f x‖ₑ ≤ C
hC : C ≠ ∞
⊢ MemLp f p μ

Tactic:
by

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

Goal state before:
pp: E : Type u_2
p : ℝ≥0∞
inst✝⁴ : NormedAddCommGroup E
X : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : OpensMeasurableSpace X
f : X → E
hf : Continuous[inst✝³, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
⊢ MemLp f p μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c c' : E
⊢ indicatorConstLp p hs hμs c + indicatorConstLp p hs hμs c' = indicatorConstLp p hs hμs (c + c')

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c c' : E
⊢ indicatorConstLp p hs hμs c - indicatorConstLp p hs hμs c' = indicatorConstLp p hs hμs (c - c')

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ ‖indicatorConstLp p hs hμs c‖ = ‖c‖ * μ.real s ^ (1 / p.toReal)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
hμs_ne_zero : μ s ≠ 0
⊢ ‖indicatorConstLp ∞ hs hμs c‖ = ‖c‖

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
hp_pos : p ≠ 0
hμs_pos : μ s ≠ 0
⊢ ‖indicatorConstLp p hs hμs c‖ = ‖c‖ * μ.real s ^ (1 / p.toReal)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
⊢ 0 ≤ ‖c‖ * μ.real s ^ (1 / p.toReal)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
⊢ ‖indicatorConstLp p hs hμs c‖ ≤ ‖c‖ * μ.real s ^ (1 / p.toReal)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
⊢ ‖indicatorConstLp p hs hμs c‖ₑ ≤ ‖c‖ₑ * μ s ^ (1 / p.toReal)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
⊢ μ (s ∆ t) ≠ ∞

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
⊢ edist (indicatorConstLp p hs hμs c) (indicatorConstLp p ht hμt c) = ‖indicatorConstLp p ⋯ ⋯ c‖ₑ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
⊢ dist (indicatorConstLp p hs hμs c) (indicatorConstLp p ht hμt c) = ‖indicatorConstLp p ⋯ ⋯ c‖

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : Finite ι
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : TopologicalSpace F
inst✝² : AddCommGroup F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : Module 𝕜 F
⊢ Continuous[instTopologicalSpaceProd, inst✝³] fun fx ↦ fx.1 fx.2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
hp₁ : Fact (1 ≤ p)
β : Type u_3
l : Filter β
t : β → Set α
ht : ∀ (b : β), MeasurableSet (t b)
hμt : ∀ (b : β), μ (t b) ≠ ∞
hp : p ≠ ∞
h : Tendsto (fun b ↦ μ (t b ∆ s)) l (𝓝 0)
⊢ Tendsto (fun b ↦ indicatorConstLp p ⋯ ⋯ c) l (𝓝 (indicatorConstLp p hs hμs c))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
⊢ μ ∅ ≠ ∞

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
c : E
⊢ indicatorConstLp p ⋯ ⋯ c = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s t : Set α
hs : MeasurableSet s
hsμ : μ s ≠ ∞
ht : MeasurableSet t
htμ : μ t ≠ ∞
c : E
hc : c ≠ 0
⊢ indicatorConstLp p hs hsμ c = indicatorConstLp p ht htμ c ↔ s =ᵐ[μ] t

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : Finite ι
inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁷ : TopologicalSpace F
inst✝⁶ : AddCommGroup F
inst✝⁵ : IsTopologicalAddGroup F
inst✝⁴ : Module 𝕜 F
G : Type u_5
inst✝³ : AddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : Module 𝕜 G
inst✝ : ContinuousConstSMul 𝕜 F
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
⊢ Continuous[instTopologicalSpaceProd, inst✝⁷] fun p ↦ (f p.1) p.2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
⊢ MemLp f 1 μ ↔ Integrable f μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
c : ε
hc : ‖c‖ₑ ≠ ∞
⊢ Integrable (fun x ↦ c) μ ↔ ‖c‖ₑ = 0 ∨ IsFiniteMeasure μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
c : β
⊢ Integrable (fun x ↦ c) μ ↔ c = 0 ∨ IsFiniteMeasure μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
c : ε
hc : ‖c‖ₑ ≠ 0
hc' : ‖c‖ₑ ≠ ∞
⊢ Integrable (fun x ↦ c) μ ↔ IsFiniteMeasure μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
c : β
hc : c ≠ 0
⊢ Integrable (fun x ↦ c) μ ↔ IsFiniteMeasure μ

Tactic:
by

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

Goal state before:
pp: α : 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
⊢ MemLp (f + g) p μ ↔ MemLp f p μ ∧ MemLp g p μ

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s✝ : Set α
hs✝ : MeasurableSet s✝
hμs✝ : μ s✝ ≠ ∞
c✝ : E
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ∞
hμt : μ t ≠ ∞
hst : Disjoint s t
c : E
⊢ μ (s ∪ t) ≠ ∞

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
p : ℝ≥0∞
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ Integrable (fun x ↦ ‖f x‖ ^ p.toReal) μ

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
inst✝ : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : MemLp f p μ
⊢ Integrable (fun x ↦ ‖f x‖ ^ p.toReal) μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
p : ℕ
hf : MemLp f (↑p) μ
hp : p ≠ 0
⊢ ↑p ≠ ∞

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
p : ℕ
hf : MemLp f (↑p) μ
hp : p ≠ 0
⊢ Integrable (fun x ↦ ‖f x‖ₑ ^ p) μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
p : ℕ
hf : MemLp f (↑p) μ
hp : p ≠ 0
⊢ ↑p ≠ ∞

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
p : ℕ
hf : MemLp f (↑p) μ
hp : p ≠ 0
⊢ Integrable (fun x ↦ ‖f x‖ ^ p) μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
inst✝ : IsFiniteMeasure μ
f : α → ε
p : ℕ
hf : MemLp f (↑p) μ
⊢ Integrable (fun x ↦ ‖f x‖ₑ ^ p) μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
inst✝ : IsFiniteMeasure μ
f : α → β
p : ℕ
hf : MemLp f (↑p) μ
⊢ Integrable (fun x ↦ ‖f x‖ ^ p) μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ∞
hμt : μ t ≠ ∞
hst : Disjoint s t
c : E
⊢ indicatorConstLp p ⋯ ⋯ c = indicatorConstLp p hs hμs c + indicatorConstLp p ht hμt c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
c : E
⊢ indicatorConstLp p ⋯ ⋯ c = (Lp.const p μ) c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
p : ℝ≥0∞
hf : AEStronglyMeasurable f μ
p_zero : p ≠ 0
p_top : p ≠ ∞
⊢ Integrable (fun x ↦ ‖f x‖ₑ ^ p.toReal) μ ↔ MemLp f p μ

Tactic:
by

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

Goal state before:
pp: 𝕜 : 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
f : MultilinearMap 𝕜 E G
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑f
m : (i : ι) → E i
i : ι
hi : ‖m i‖ = 0
⊢ ‖f m‖ = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
p : ℝ≥0∞
hf : AEStronglyMeasurable f μ
p_zero : p ≠ 0
p_top : p ≠ ∞
⊢ Integrable (fun x ↦ ‖f x‖ ^ p.toReal) μ ↔ MemLp f p μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : IsFiniteMeasure μ
c : E
inst✝ : NeZero μ
hp_zero : p ≠ 0
⊢ ‖(Lp.const p μ) c‖ = ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
inst✝ : IsFiniteMeasure μ
f : α → β
hf : AEStronglyMeasurable f μ
p q : ℝ
hp✝ : 0 ≤ p
hq✝ : 0 ≤ q
hpq : p ≤ q
hint : Integrable (fun x ↦ ‖f x‖ ^ q) μ
hp : 0 < p
hq : 0 < q
⊢ ENNReal.ofReal p ≠ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
c : E
hp_zero : p ≠ 0
hp_top : p ≠ ∞
⊢ ‖(Lp.const p μ) c‖ = ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
inst✝ : IsFiniteMeasure μ
f : α → β
hf : AEStronglyMeasurable f μ
p q : ℝ
hp✝ : 0 ≤ p
hq✝ : 0 ≤ q
hpq : p ≤ q
hint : Integrable (fun x ↦ ‖f x‖ ^ q) μ
hp : 0 < p
hq : 0 < q
⊢ ENNReal.ofReal p ≠ ∞

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
c : E
⊢ ‖(Lp.const p μ) c‖ ≤ ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Fact (1 ≤ p)
⊢ 0 ≤ μ.real Set.univ ^ (1 / p.toReal)

Tactic:
by

Goal state after: