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

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

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
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
s : Finset ι
his : i ∉ s
Hrec : ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
⊢ ‖f (s.piecewise m₂ m₁) - f ((insert i s).piecewise m₂ m₁)‖ ≤
    C * ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure β
⊢ IntegrableAtFilter f (map e l) μ ↔ IntegrableAtFilter (f ∘ e) l (Measure.comap e μ)

Tactic:
by

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 ε
inst✝² : Preorder α
inst✝¹ : IsCodirectedOrder α
inst✝ : Nonempty α
⊢ IntegrableAtFilter f atBot μ ↔ ∃ a, IntegrableOn f (Iic a) μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
l : Filter α
⊢ univ ∈ l

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] {ι : Type v} [inst_6 : Finite ι]
    (ξ : Basis ι 𝕜 E) (this : Fintype ι),
    let this_1 := IsTopologicalAddGroup.rightUniformSpace E;
    let this_2 := ⋯;
    Fintype.card ι = n → Continuous[_, Pi.topologicalSpace] ⇑ξ.equivFun
E : Type v
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : T2Space E
ι : Type v
inst✝ : Finite ι
ξ : Basis ι 𝕜 E
this✝³ : Fintype ι
this✝² : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this✝¹ : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
hn : Fintype.card ι = n + 1
this✝ : FiniteDimensional 𝕜 E
s : Submodule 𝕜 E
s_dim : finrank 𝕜 ↥s = n
this : IsUniformAddGroup ↥s := AddSubgroup.isUniformAddGroup s.toAddSubgroup
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s)) 𝕜 ↥s := Basis.ofVectorSpace 𝕜 ↥s
⊢ Fintype.card ↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) = n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
l : Filter α
inst✝ : ContinuousAdd ε'
f g : α → ε'
hf : IntegrableAtFilter f l μ
hg : IntegrableAtFilter g l μ
⊢ IntegrableAtFilter (f + g) l μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
hf : IntegrableAtFilter f l μ
⊢ IntegrableAtFilter (-f) l μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
⊢ IntegrableAtFilter (-f) l μ ↔ IntegrableAtFilter f l μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
l : Filter α
f g : α → E
hf : IntegrableAtFilter f l μ
hg : IntegrableAtFilter g l μ
⊢ IntegrableAtFilter (f - g) l μ

Tactic:
by

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

Goal state before:
pp: case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → E
⊢ AEMeasurable (fun x ↦ (f x).toNNReal) μ

Tactic:
· exact hf.ennreal_toNNReal

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

Goal state before:
pp: α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
l : Filter α
𝕜 : Type u_7
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : α → E
hf : IntegrableAtFilter f l μ
c : 𝕜
⊢ IntegrableAtFilter (c • f) l μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → E
⊢ Integrable g (μ.withDensity f) ↔ Integrable (fun x ↦ (f x).toReal • g x) μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝² : NormedAddCommGroup E
μ : Measure α
l : Filter α
𝕜 : Type u_7
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → E
c : 𝕜
hc : c ≠ 0
⊢ IntegrableAtFilter (c • f) l μ ↔ IntegrableAtFilter f l μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ
⊢ (fun x ↦ g x * (f x).toReal) = fun x ↦ (f x).toReal • g x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝² : NormedAddCommGroup E
μ : Measure α
l : Filter α
𝕜 : Type u_7
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → E
c : 𝕜
⊢ IntegrableAtFilter (c • f) l μ ↔ c = 0 ∨ IntegrableAtFilter f l μ

Tactic:
by

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 α
⊢ IntegrableAtFilter f (l ⊓ ae μ) μ ↔ IntegrableAtFilter f l μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
ε' : Type u_7
inst✝² : TopologicalSpace ε'
inst✝¹ : ENormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
⊢ IntegrableAtFilter f ⊤ μ ↔ Integrable f μ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ
⊢ Integrable g (μ.withDensity f) ↔ Integrable (fun x ↦ g x * (f x).toReal) μ

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
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
s : Finset ι
his : i ∉ s
Hrec : ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
I :
  ‖f (s.piecewise m₂ m₁) - f ((insert i s).piecewise m₂ m₁)‖ ≤
    C * ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
⊢ ‖f m₁ - f ((insert i s).piecewise m₂ m₁)‖ ≤
    ‖f m₁ - f (s.piecewise m₂ m₁)‖ + ‖f (s.piecewise m₂ m₁) - f ((insert i s).piecewise m₂ m₁)‖

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] {ι : Type v} [inst_6 : Finite ι]
    (ξ : Basis ι 𝕜 E) (this : Fintype ι),
    let this_1 := IsTopologicalAddGroup.rightUniformSpace E;
    let this_2 := ⋯;
    Fintype.card ι = n → Continuous[_, Pi.topologicalSpace] ⇑ξ.equivFun
E : Type v
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : T2Space E
ι : Type v
inst✝ : Finite ι
ξ : Basis ι 𝕜 E
this✝³ : Fintype ι
this✝² : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this✝¹ : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
hn : Fintype.card ι = n + 1
this✝ : FiniteDimensional 𝕜 E
s : Submodule 𝕜 E
s_dim : finrank 𝕜 ↥s = n
this : IsUniformAddGroup ↥s := AddSubgroup.isUniformAddGroup s.toAddSubgroup
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s)) 𝕜 ↥s := Basis.ofVectorSpace 𝕜 ↥s
⊢ IsUniformEmbedding ⇑b.equivFun.symm.toEquiv

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
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
s : Finset ι
his : i ∉ s
Hrec : ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
I :
  ‖f (s.piecewise m₂ m₁) - f ((insert i s).piecewise m₂ m₁)‖ ≤
    C * ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
⊢ ((C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) +
      C * ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) =
    C * ∑ i ∈ insert i s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
l l' : Filter α
⊢ IntegrableAtFilter f (l ⊔ l') μ ↔ IntegrableAtFilter f l μ ∧ IntegrableAtFilter f l' μ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] {ι : Type v} [inst_6 : Finite ι]
    (ξ : Basis ι 𝕜 E) (this : Fintype ι),
    let this_1 := IsTopologicalAddGroup.rightUniformSpace E;
    let this_2 := ⋯;
    Fintype.card ι = n → Continuous[_, Pi.topologicalSpace] ⇑ξ.equivFun
E : Type v
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : T2Space E
ι : Type v
inst✝ : Finite ι
ξ : Basis ι 𝕜 E
this✝² : Fintype ι
this✝¹ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this✝ : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
hn : Fintype.card ι = n + 1
this : FiniteDimensional 𝕜 E
⊢ ∀ (s : Submodule 𝕜 E), finrank 𝕜 ↥s = n → IsClosed[inst✝⁴] ↑s

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
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
s : Finset ι
⊢ ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

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
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
⊢ ‖f m₁ - f m₂‖ ≤ C * ∑ i, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
f : α → E
l : Filter α
inst✝ : l.IsMeasurablyGenerated
hfm : StronglyMeasurableAtFilter f l μ
hμ : μ.FiniteAtFilter l
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l (norm ∘ f)
⊢ IntegrableAtFilter f l μ

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
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
⊢ (∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) ≤ ∏ j, update (fun x ↦ max ‖m₁‖ ‖m₂‖) i ‖m₁ - m₂‖ j

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
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
⊢ ∏ j, update (fun x ↦ max ‖m₁‖ ‖m₂‖) i ‖m₁ - m₂‖ j = ‖m₁ - m₂‖ * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ Integrable (f + g) μ ↔ Integrable f μ ∧ Integrable g μ

Tactic:
refine ⟨fun hfg => ⟨?_, ?_⟩, fun h => h.1.add h.2⟩
  · rw [← indicator_add_eq_left h]; exact hfg.indicator hf.measurableSet_support
  · rw [← indicator_add_eq_right h]; exact hfg.indicator hg.measurableSet_support

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

Goal state before:
pp: α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ Integrable (f + g) μ ↔ Integrable f μ ∧ Integrable g μ

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
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
⊢ ∀ (i : ι),
    (∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) ≤ ‖m₁ - m₂‖ * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1)

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
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
A :
  ∀ (i : ι),
    (∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) ≤ ‖m₁ - m₂‖ * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1)
⊢ (C * ∑ i, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) ≤
    C * ∑ _i, ‖m₁ - m₂‖ * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
h' : ∀ s ∈ l, μ s = ∞
a : E
hf : Tendsto f l (𝓝 a)
H : ¬a = 0
ε : ℝ
εpos : 0 < ε
hε : ε < ‖a‖
u : Set α
ul : u ∈ l
hu : IntegrableOn f u μ
v : Set α := u ∩ {b | ε < ‖f b‖}
hv : IntegrableOn f v μ
vl : v ∈ l
this : (μ.restrict v) v < ∞
⊢ μ v < ∞

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
h : IntegrableAtFilter f l μ
h' : ∀ s ∈ l, μ s = ∞
a : E
hf : Tendsto f l (𝓝 a)
⊢ a = 0

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
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
A :
  ∀ (i : ι),
    (∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) ≤ ‖m₁ - m₂‖ * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1)
⊢ C * ∑ _i, ‖m₁ - m₂‖ * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) =
    C * ↑(Fintype.card ι) * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖

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
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
⊢ ‖f m₁ - f m₂‖ ≤ C * ↑(Fintype.card ι) * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖

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
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
C : ℝ
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
D : ℝ := max C 1
D_pos : 0 ≤ D
m : (i : ι) → E i
⊢ 0 ≤ ∏ i, ‖m i‖

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
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
C : ℝ
D : ℝ := max C 1
D_pos : 0 ≤ D
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ D * ∏ i, ‖m i‖
m m' : (i : ι) → E i
h' : dist m' m < 1
⊢ max ‖m'‖ ‖m‖ ≤ ‖m‖ + 1

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
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
C : ℝ
D : ℝ := max C 1
D_pos : 0 ≤ D
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ D * ∏ i, ‖m i‖
m m' : (i : ι) → E i
h' : dist m' m < 1
this : max ‖m'‖ ‖m‖ ≤ ‖m‖ + 1
⊢ D * ↑(Fintype.card ι) * max ‖m'‖ ‖m‖ ^ (Fintype.card ι - 1) * ‖m' - m‖ ≤
    D * ↑(Fintype.card ι) * (‖m‖ + 1) ^ (Fintype.card ι - 1) * ‖m' - m‖

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
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
C : ℝ
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
⊢ Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑f

Tactic:
by

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

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

Tactic:
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
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
⊢ Continuous fun x ↦ x * ∏ i, ‖m i‖

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
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
⊢ IsLeast {c | 0 ≤ c ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ c * ∏ i, ‖m i‖} ‖f‖

Tactic:
by

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

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

Tactic:
by

Goal state after: