mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case refine_2
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
⊢ Seminorm.IsBounded (fun i ↦ (Finset.Iic i).sup p) p LinearMap.id

Tactic:
intro i

Goal state after:
case refine_2
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ ∃ s C, (p i).comp LinearMap.id ≤ C • s.sup fun i ↦ (Finset.Iic i).sup p
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case refine_1
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
t : TopologicalSpace E
hp : WithSeminorms p
e : ι' ≃ ι
⊢ Seminorm.IsBounded p (p ∘ ⇑e) LinearMap.id

Tactic:
intro i

Goal state after:
case refine_1
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
t : TopologicalSpace E
hp : WithSeminorms p
e : ι' ≃ ι
i : ι'
⊢ ∃ s C, ((p ∘ ⇑e) i).comp LinearMap.id ≤ C • s.sup p
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case refine_2
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
t : TopologicalSpace E
hp : WithSeminorms p
e : ι' ≃ ι
⊢ Seminorm.IsBounded (p ∘ ⇑e) p LinearMap.id

Tactic:
intro i

Goal state after:
case refine_2
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
t : TopologicalSpace E
hp : WithSeminorms p
e : ι' ≃ ι
i : ι
⊢ ∃ s C, (p i).comp LinearMap.id ≤ C • s.sup (p ∘ ⇑e)
Module: Mathlib.Order.Filter.Germ.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝¹ : Monoid M
inst✝ : MulAction M β
c₁ c₂ : M
f✝ : l.Germ β
f : α → β
⊢ (c₁ * c₂) • ↑f = c₁ • c₂ • ↑f

Tactic:
norm_cast

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝¹ : Monoid M
inst✝ : MulAction M β
c₁ c₂ : M
f✝ : l.Germ β
f : α → β
⊢ (c₁ * c₂) • f =ᶠ[l] c₁ • c₂ • f
Module: Mathlib.Order.Filter.Germ.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝¹ : Monoid M
inst✝ : MulAction M β
f✝ : l.Germ β
f : α → β
⊢ 1 • ↑f = ↑f

Tactic:
norm_cast

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝¹ : Monoid M
inst✝ : MulAction M β
f✝ : l.Germ β
f : α → β
⊢ 1 • f =ᶠ[l] f
Module: Mathlib.Order.Filter.Germ.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝¹ : Monoid M
inst✝ : MulAction M β
c₁✝ c₂✝ : l.Germ M
f✝ : l.Germ β
c₁ c₂ : α → M
f : α → β
⊢ (↑c₁ * ↑c₂) • ↑f = ↑c₁ • ↑c₂ • ↑f

Tactic:
norm_cast

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝¹ : Monoid M
inst✝ : MulAction M β
c₁✝ c₂✝ : l.Germ M
f✝ : l.Germ β
c₁ c₂ : α → M
f : α → β
⊢ (c₁ * c₂) • f =ᶠ[l] c₁ • c₂ • f
Module: Mathlib.Order.Filter.Germ.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g✝¹ h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction M N
c : M
f✝ g✝ : l.Germ N
f g : α → N
⊢ c • (↑f + ↑g) = c • ↑f + c • ↑g

Tactic:
norm_cast

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g✝¹ h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction M N
c : M
f✝ g✝ : l.Germ N
f g : α → N
⊢ c • (f + g) =ᶠ[l] c • f + c • g
Module: Mathlib.Order.Filter.Germ.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g✝¹ h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction M N
c✝ : l.Germ M
f✝ g✝ : l.Germ N
c : α → M
f g : α → N
⊢ ↑c • (↑f + ↑g) = ↑c • ↑f + ↑c • ↑g

Tactic:
norm_cast

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g✝¹ h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction M N
c✝ : l.Germ M
f✝ g✝ : l.Germ N
c : α → M
f g : α → N
⊢ c • (f + g) =ᶠ[l] c • f + c • g
Module: Mathlib.Order.Filter.Germ.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c₁ c₂ : R
f✝ : l.Germ M
f : α → M
⊢ (c₁ + c₂) • ↑f = c₁ • ↑f + c₂ • ↑f

Tactic:
norm_cast

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c₁ c₂ : R
f✝ : l.Germ M
f : α → M
⊢ (c₁ + c₂) • f =ᶠ[l] c₁ • f + c₂ • f
Module: Mathlib.Order.Filter.Germ.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f✝ : l.Germ M
f : α → M
⊢ 0 • ↑f = 0

Tactic:
norm_cast

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f✝ : l.Germ M
f : α → M
⊢ 0 • f =ᶠ[l] 0
Module: Mathlib.Order.Filter.Germ.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c₁✝ c₂✝ : l.Germ R
f✝ : l.Germ M
c₁ c₂ : α → R
f : α → M
⊢ (↑c₁ + ↑c₂) • ↑f = ↑c₁ • ↑f + ↑c₂ • ↑f

Tactic:
norm_cast

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c₁✝ c₂✝ : l.Germ R
f✝ : l.Germ M
c₁ c₂ : α → R
f : α → M
⊢ (c₁ + c₂) • f =ᶠ[l] c₁ • f + c₂ • f
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: case intro.a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
⊢ ∀ (i : ι), MeasurableSpace.comap (fun b ↦ b i) ((fun i ↦ generateFrom (C i)) i) ≤ generateFrom (univ.pi '' univ.pi C)

Tactic:
intro i

Goal state after:
case intro.a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
i : ι
⊢ MeasurableSpace.comap (fun b ↦ b i) ((fun i ↦ generateFrom (C i)) i) ≤ generateFrom (univ.pi '' univ.pi C)
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: case e_6
α : Type u_1
inst✝⁴ : TopologicalSpace α
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalSemiring R
inst✝ : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
h✝ : Nonempty α
inhabited_h : Inhabited α
f : C(α, R)
x' : α
⊢ x' = default

Tactic:
simp [eq_iff_true_of_subsingleton]

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: case a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ univ.pi C
⊢ ∀ (b : ι), MeasurableSet (eval b ⁻¹' s b)

Tactic:
intro i

Goal state after:
case a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ univ.pi C
i : ι
⊢ MeasurableSet (eval i ⁻¹' s i)
Module: Mathlib.MeasureTheory.Function.EssSup

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : ConditionallyCompleteLinearOrder β
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology β
inst✝ : OrderTopology β
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) (ae μ) f
⊢ μ {y | ¬essInf f μ ≤ f y} = 0

Tactic:
exact ae_essInf_le hf

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteLinearOrder β
f : α → β
h : ∀ ⦃x : α⦄ ⦃a : β⦄, a < f x → μ {y | a < f y} ≠ 0
⊢ ∀ (i : α), f i ≤ essSup f μ

Tactic:
intro i

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteLinearOrder β
f : α → β
h : ∀ ⦃x : α⦄ ⦃a : β⦄, a < f x → μ {y | a < f y} ≠ 0
i : α
⊢ f i ≤ essSup f μ
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : ↑f ≤ᵐ[μ] ↑f'
hg : ↑g ≤ᵐ[μ] ↑f'
⊢ ↑(f ⊔ g) ≤ᵐ[μ] ↑f'

Tactic:
filter_upwards [hf, hg, coeFn_sup f g] with _ haf hag ha_sup

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : ↑f ≤ᵐ[μ] ↑f'
hg : ↑g ≤ᵐ[μ] ↑f'
a✝ : α
haf : ↑f a✝ ≤ ↑f' a✝
hag : ↑g a✝ ≤ ↑f' a✝
ha_sup : ↑(f ⊔ g) a✝ = ↑f a✝ ⊔ ↑g a✝
⊢ ↑(f ⊔ g) a✝ ≤ ↑f' a✝
Module: Mathlib.MeasureTheory.Function.EssSup

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
g : α → ℝ≥0∞
hs : MeasurableSet s
⊢ essSup (s.piecewise f g) μ = max (essSup f (μ.restrict s)) (essSup g (μ.restrict sᶜ))

Tactic:
simp only [essSup, limsup_piecewise, blimsup_eq_limsup, ae_restrict_eq, hs, hs.compl]; rfl

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
⊢ ∀ (i : ι), MeasurableSpace.comap (fun b ↦ b i) (inst✝ i) ≤ (OuterMeasure.pi fun i ↦ (μ i).toOuterMeasure).caratheodory

Tactic:
intro i

Goal state after:
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
⊢ MeasurableSpace.comap (fun b ↦ b i) (inst✝ i) ≤ (OuterMeasure.pi fun i ↦ (μ i).toOuterMeasure).caratheodory
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), generateFrom (C i) = inst✝ i
h2C : ∀ (i : ι), IsPiSystem (C i)
h3C : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
μν : Measure ((i : ι) → α i)
h₁ : ∀ (s : (i : ι) → Set (α i)), (∀ (i : ι), s i ∈ C i) → μν (univ.pi s) = ∏ i, (μ i) (s i)
⊢ ∀ (i : ι), ∀ s ∈ C i, MeasurableSet s

Tactic:
intro i

Goal state after:
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), generateFrom (C i) = inst✝ i
h2C : ∀ (i : ι), IsPiSystem (C i)
h3C : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
μν : Measure ((i : ι) → α i)
h₁ : ∀ (s : (i : ι) → Set (α i)), (∀ (i : ι), s i ∈ C i) → μν (univ.pi s) = ∏ i, (μ i) (s i)
i : ι
⊢ ∀ s ∈ C i, MeasurableSet s
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
⊢ ∀ x ∈ Finset.univ.erase i, (μ x) univ = 1

Tactic:
exact fun _ _ ↦ measure_univ

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Pi

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

Tactic:
intro i

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst✝ : NormedAddCommGroup β
μ : Measure α
hp' : p ≠ ∞
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ x ∈ s, dist (f x) (g x) ≤ c
⊢ eLpNorm (s.indicator (f - g)) p μ ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal)

Tactic:
by_cases hp : p = 0

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst✝ : NormedAddCommGroup β
μ : Measure α
hp' : p ≠ ∞
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ x ∈ s, dist (f x) (g x) ≤ c
hp : p = 0
⊢ eLpNorm (s.indicator (f - g)) p μ ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal)

case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst✝ : NormedAddCommGroup β
μ : Measure α
hp' : p ≠ ∞
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ x ∈ s, dist (f x) (g x) ≤ c
hp : ¬p = 0
⊢ eLpNorm (s.indicator (f - g)) p μ ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
h0 : ¬p = 0
h_top : p = ∞
⊢ eLpNorm 0 p μ = 0

Tactic:
simp only [h_top, eLpNorm_exponent_top, eLpNormEssSup_zero]

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

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
⊢ ‖c‖ₑ ^ q ≠ ∞

Tactic:
· finiteness [show ‖c‖ₑ ≠ 0 by simp [hc_ne_zero]]

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

Goal state before:
pp: case inr
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
hμ : NeZero μ
⊢ eLpNorm f p μ ≤ C • μ Set.univ ^ p.toReal⁻¹

Tactic:
by_cases hp : p = 0

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
hμ : NeZero μ
hp : p = 0
⊢ eLpNorm f p μ ≤ C • μ Set.univ ^ p.toReal⁻¹

case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
hμ : NeZero μ
hp : ¬p = 0
⊢ eLpNorm f p μ ≤ C • μ Set.univ ^ p.toReal⁻¹
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hμν : ν ≪ μ
⊢ eLpNormEssSup f ν ≤ eLpNormEssSup f μ

Tactic:
simp_rw [eLpNormEssSup]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hμν : ν ≪ μ
⊢ essSup (fun x ↦ ‖f x‖ₑ) ν ≤ essSup (fun x ↦ ‖f x‖ₑ) μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝⁵ : ENorm ε
R : Type u_7
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : Module R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
f : α → ε
⊢ eLpNormEssSup f (c • μ) = eLpNormEssSup f μ

Tactic:
simp_rw [eLpNormEssSup]

Goal state after:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝⁵ : ENorm ε
R : Type u_7
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : Module R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
f : α → ε
⊢ essSup (fun x ↦ ‖f x‖ₑ) (c • μ) = essSup (fun x ↦ ‖f x‖ₑ) μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
c : ℝ≥0∞
hc : c ≠ 0
f : α → ε
⊢ eLpNormEssSup f (c • μ) = eLpNormEssSup f μ

Tactic:
simp_rw [eLpNormEssSup]

Goal state after:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
c : ℝ≥0∞
hc : c ≠ 0
f : α → ε
⊢ essSup (fun x ↦ ‖f x‖ₑ) (c • μ) = essSup (fun x ↦ ‖f x‖ₑ) μ
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q : ℝ≥0
h : p.HolderConjugate q
⊢ ↑p⁻¹ + ↑q⁻¹ = 1

Tactic:
norm_cast

Goal state after:
p q : ℝ≥0
h : p.HolderConjugate q
⊢ p⁻¹ + q⁻¹ = 1
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q : ℝ≥0
⊢ 1 < ↑p ∧ (↑p)⁻¹ + (↑q)⁻¹ = 1 ↔ 1 < p ∧ p⁻¹ + q⁻¹ = 1

Tactic:
← coe_one

Goal state after:
p q : ℝ≥0
⊢ ↑1 < ↑p ∧ (↑p)⁻¹ + (↑q)⁻¹ = ↑1 ↔ 1 < p ∧ p⁻¹ + q⁻¹ = 1
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p : ℝ≥0
hp : 1 < p
⊢ ↑(p / (p - 1)) = 1 + (↑p - 1)⁻¹

Tactic:
norm_cast

Goal state after:
p : ℝ≥0
hp : 1 < p
⊢ ↑(p / (p - 1)) = 1 + (↑(p - 1))⁻¹
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p : ℝ≥0
hp : 1 < p
⊢ ↑(p / (p - 1)) = 1 + ↑(p - 1)⁻¹

Tactic:
norm_cast

Goal state after:
p : ℝ≥0
hp : 1 < p
⊢ p / (p - 1) = 1 + (p - 1)⁻¹
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
c : ℝ≥0
hc : c ≠ 0
f : α → ε
p : ℝ≥0∞
μ : Measure α
⊢ ↑c ^ p.toReal⁻¹ * eLpNorm f p μ = c ^ p.toReal⁻¹ • eLpNorm f p μ

Tactic:
norm_cast

Goal state after:
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q : ℝ≥0∞
hp : 1 < p.toReal
h : p.HolderConjugate q
⊢ 0 < q.toReal

Tactic:
rw [toReal_pos_iff]

Goal state after:
p q : ℝ≥0∞
hp : 1 < p.toReal
h : p.HolderConjugate q
⊢ 0 < q ∧ q < ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case inr.inr
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
hp₀ : p ≠ 0
hp : p ≠ ∞
⊢ ∃ c, ∀ (x : α), ↑(‖f x‖₊ ^ p.toReal) ≤ ↑c

Tactic:
norm_cast

Goal state after:
case inr.inr
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
hp₀ : p ≠ 0
hp : p ≠ ∞
⊢ ∃ c, ∀ (x : α), ‖f x‖₊ ^ p.toReal ≤ c
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: ⊢ StrictConcaveOn ℝ (Iio 0) log

Tactic:
refine ⟨convex_Iio _, ?_⟩

Goal state after:
⊢ ∀ ⦃x : ℝ⦄,
    x ∈ Iio 0 →
      ∀ ⦃y : ℝ⦄,
        y ∈ Iio 0 → x ≠ y → ∀ ⦃a b : ℝ⦄, 0 < a → 0 < b → a + b = 1 → a • log x + b • log y < log (a • x + b • y)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_3
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
this : ∏ x ∈ s, rexp (log (z x) * w x) ≤ ∑ x ∈ s, w x * rexp (log (z x))
⊢ ∀ x ∈ s, z x ^ w x = rexp (log (z x) * w x)

Tactic:
intro i

Goal state after:
case e'_3
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
this : ∏ x ∈ s, rexp (log (z x) * w x) ≤ ∑ x ∈ s, w x * rexp (log (z x))
i : ι
⊢ i ∈ s → z i ^ w i = rexp (log (z i) * w i)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_4
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
this : ∏ x ∈ s, rexp (log (z x) * w x) ≤ ∑ x ∈ s, w x * rexp (log (z x))
⊢ ∀ x ∈ s, w x * z x = w x * rexp (log (z x))

Tactic:
intro i

Goal state after:
case e'_4
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
this : ∏ x ∈ s, rexp (log (z x) * w x) ≤ ∑ x ∈ s, w x * rexp (log (z x))
i : ι
⊢ i ∈ s → w i * z i = w i * rexp (log (z i))
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case hx
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ ∀ i ∈ s, 0 ≤ w i * z i ^ p

Tactic:
intro i

Goal state after:
case hx
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
i : ι
⊢ i ∈ s → 0 ≤ w i * z i ^ p
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ ∀ i ∈ s, 0 ≤ w i * z i

Tactic:
intro i

Goal state after:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
i : ι
⊢ i ∈ s → 0 ≤ w i * z i
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ ∀ i ∈ s, 0 ≤ w i * z i ^ p

Tactic:
intro i

Goal state after:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
i : ι
⊢ i ∈ s → 0 ≤ w i * z i ^ p
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_1.h₁
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
⊢ ∀ x ∈ s, z x ^ w x = rexp (log (z x) * w x)

Tactic:
intro i

Goal state after:
case e'_1.h₁
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
i : ι
⊢ i ∈ s → z i ^ w i = rexp (log (z i) * w i)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_1.h₂
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
⊢ ∀ x ∈ s, w x * z x = w x * rexp (log (z x))

Tactic:
intro i

Goal state after:
case e'_1.h₂
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
i : ι
⊢ i ∈ s → w i * z i = w i * rexp (log (z i))