mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case inl
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
h✝ : IsEmpty ((i : ι) → A i)
⊢ ∫⁻ (x : (i : ι) → A i), f x ^ (1 - (↑#ι - 1) * p) * ∏ i, (∫⁻ (xᵢ : A i), f (update x i xᵢ) ∂μ i) ^ p ∂Measure.pi μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi μ) ^ (1 + p)

pp: case inr
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
h✝ : Nonempty ((i : ι) → A i)
⊢ ∫⁻ (x : (i : ι) → A i), f x ^ (1 - (↑#ι - 1) * p) * ∏ i, (∫⁻ (xᵢ : A i), f (update x i xᵢ) ∂μ i) ^ p ∂Measure.pi μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi μ) ^ (1 + p)

Tactic:
·

Goal state after:
case inl
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
h✝ : IsEmpty ((i : ι) → A i)
⊢ ∫⁻ (x : (i : ι) → A i), f x ^ (1 - (↑#ι - 1) * p) * ∏ i, (∫⁻ (xᵢ : A i), f (update x i xᵢ) ∂μ i) ^ p ∂Measure.pi μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi μ) ^ (1 + p)
Module: Mathlib.Analysis.InnerProductSpace.ExteriorPower

Goal state before:
pp: case pos
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
ι : Type u_2
inst✝ : LinearOrder ι
v : ι → E
hv : Orthonormal ℝ v
s t : ↑(Set.powersetCard ι n)
h : s = t
⊢ (innerProductForm ((ιMulti ℝ n) (v ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm s))))
      ((ιMulti ℝ n) (v ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm t))) =
    1

pp: case neg
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
ι : Type u_2
inst✝ : LinearOrder ι
v : ι → E
hv : Orthonormal ℝ v
s t : ↑(Set.powersetCard ι n)
h : ¬s = t
⊢ (innerProductForm ((ιMulti ℝ n) (v ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm s))))
      ((ιMulti ℝ n) (v ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm t))) =
    0

Tactic:
·

Goal state after:
case pos
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
ι : Type u_2
inst✝ : LinearOrder ι
v : ι → E
hv : Orthonormal ℝ v
s t : ↑(Set.powersetCard ι n)
h : s = t
⊢ (innerProductForm ((ιMulti ℝ n) (v ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm s))))
      ((ιMulti ℝ n) (v ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm t))) =
    1
Module: Mathlib.Analysis.InnerProductSpace.ExteriorPower

Goal state before:
pp: case neg
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
ι : Type u_2
inst✝ : LinearOrder ι
v : ι → E
hv : Orthonormal ℝ v
s t : ↑(Set.powersetCard ι n)
h : ¬s = t
⊢ (innerProductForm ((ιMulti ℝ n) (v ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm s))))
      ((ιMulti ℝ n) (v ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm t))) =
    0

Tactic:
·

Goal state after:
case neg
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
ι : Type u_2
inst✝ : LinearOrder ι
v : ι → E
hv : Orthonormal ℝ v
s t : ↑(Set.powersetCard ι n)
h : ¬s = t
⊢ (innerProductForm ((ιMulti ℝ n) (v ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm s))))
      ((ιMulti ℝ n) (v ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm t))) =
    0
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: ι : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
p : ℝ
hp : (↑#ι).HolderConjugate p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ ↑#ι - 1
x : ι → ℝ
i : ι
a✝ : i ∈ Finset.univ
⊢ ContDiff ℝ 1 (u ∘ update x i)

pp: ι : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
p : ℝ
hp : (↑#ι).HolderConjugate p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ ↑#ι - 1
x : ι → ℝ
i : ι
a✝ : i ∈ Finset.univ
⊢ HasCompactSupport (u ∘ update x i)

Tactic:
·

Goal state after:
ι : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
p : ℝ
hp : (↑#ι).HolderConjugate p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ ↑#ι - 1
x : ι → ℝ
i : ι
a✝ : i ∈ Finset.univ
⊢ ContDiff ℝ 1 (u ∘ update x i)
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: ι : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
p : ℝ
hp : (↑#ι).HolderConjugate p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ ↑#ι - 1
x : ι → ℝ
i : ι
a✝ : i ∈ Finset.univ
⊢ HasCompactSupport (u ∘ update x i)

Tactic:
·

Goal state after:
ι : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
p : ℝ
hp : (↑#ι).HolderConjugate p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ ↑#ι - 1
x : ι → ℝ
i : ι
a✝ : i ∈ Finset.univ
⊢ HasCompactSupport (u ∘ update x i)
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : f.IsPositive
h : ∃ s, Nonempty (Module.Basis (↥s) 𝕜 E)
⊢ 0 ≤ (traceAux 𝕜 ⋯.some) f

pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : f.IsPositive
h : ¬∃ s, Nonempty (Module.Basis (↥s) 𝕜 E)
⊢ 0 ≤ 0 f

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : f.IsPositive
h : ∃ s, Nonempty (Module.Basis (↥s) 𝕜 E)
⊢ 0 ≤ (traceAux 𝕜 ⋯.some) f
Module: Mathlib.Analysis.InnerProductSpace.Semisimple

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
⊢ qᗮ ∈ T.invtSubmodule

pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
⊢ Disjoint q (qᗮ ⊓ p)

pp: case refine_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
⊢ q ⊔ qᗮ ⊓ p = p

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
⊢ qᗮ ∈ T.invtSubmodule
Module: Mathlib.Analysis.InnerProductSpace.Semisimple

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
⊢ Disjoint q (qᗮ ⊓ p)

pp: case refine_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
⊢ q ⊔ qᗮ ⊓ p = p

Tactic:
·

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
⊢ Disjoint q (qᗮ ⊓ p)
Module: Mathlib.Analysis.InnerProductSpace.Semisimple

Goal state before:
pp: case refine_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
⊢ q ⊔ qᗮ ⊓ p = p

Tactic:
·

Goal state after:
case refine_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
⊢ q ⊔ qᗮ ⊓ p = p
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case h2
ι : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
p : ℝ
hp : (↑#ι).HolderConjugate p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ ↑#ι - 1
x : ι → ℝ
i : ι
a✝ : i ∈ Finset.univ
⊢ volume.restrict (Set.Iic (x i)) ≤ volume

pp: case hfg
ι : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
p : ℝ
hp : (↑#ι).HolderConjugate p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ ↑#ι - 1
x : ι → ℝ
i : ι
a✝ : i ∈ Finset.univ
y : ℝ
⊢ ‖deriv (u ∘ update x i) y‖ₑ ≤ ‖fderiv ℝ u (update x i y)‖ₑ

Tactic:
·

Goal state after:
case h2
ι : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
p : ℝ
hp : (↑#ι).HolderConjugate p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ ↑#ι - 1
x : ι → ℝ
i : ι
a✝ : i ∈ Finset.univ
⊢ volume.restrict (Set.Iic (x i)) ≤ volume
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : f.IsPositive
h : ¬∃ s, Nonempty (Module.Basis (↥s) 𝕜 E)
⊢ 0 ≤ 0 f

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : f.IsPositive
h : ¬∃ s, Nonempty (Module.Basis (↥s) 𝕜 E)
⊢ 0 ≤ 0 f
Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
hA : A.IsSymmetric
hB : B.IsSymmetric
i j : 𝕜 × 𝕜
hij : i ≠ j
v : E
x✝ : v ∈ eigenspace A i.2 ⊓ eigenspace B i.1
hv1 : v ∈ ↑(eigenspace A i.2)
hv2 : v ∈ ↑(eigenspace B i.1)
h₁ : i.1 ≠ j.1
w : E
hw1 : w ∈ ↑(eigenspace A j.2)
hw2 : w ∈ ↑(eigenspace B j.1)
⊢ inner 𝕜 w v = 0

pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
hA : A.IsSymmetric
hB : B.IsSymmetric
i j : 𝕜 × 𝕜
hij : i ≠ j
v : E
x✝ : v ∈ eigenspace A i.2 ⊓ eigenspace B i.1
hv1 : v ∈ ↑(eigenspace A i.2)
hv2 : v ∈ ↑(eigenspace B i.1)
h₂ : i.2 ≠ j.2
w : E
hw1 : w ∈ ↑(eigenspace A j.2)
hw2 : w ∈ ↑(eigenspace B j.1)
⊢ inner 𝕜 w v = 0

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
hA : A.IsSymmetric
hB : B.IsSymmetric
i j : 𝕜 × 𝕜
hij : i ≠ j
v : E
x✝ : v ∈ eigenspace A i.2 ⊓ eigenspace B i.1
hv1 : v ∈ ↑(eigenspace A i.2)
hv2 : v ∈ ↑(eigenspace B i.1)
h₁ : i.1 ≠ j.1
w : E
hw1 : w ∈ ↑(eigenspace A j.2)
hw2 : w ∈ ↑(eigenspace B j.1)
⊢ inner 𝕜 w v = 0
Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
hA : A.IsSymmetric
hB : B.IsSymmetric
i j : 𝕜 × 𝕜
hij : i ≠ j
v : E
x✝ : v ∈ eigenspace A i.2 ⊓ eigenspace B i.1
hv1 : v ∈ ↑(eigenspace A i.2)
hv2 : v ∈ ↑(eigenspace B i.1)
h₂ : i.2 ≠ j.2
w : E
hw1 : w ∈ ↑(eigenspace A j.2)
hw2 : w ∈ ↑(eigenspace B j.1)
⊢ inner 𝕜 w v = 0

Tactic:
·

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
hA : A.IsSymmetric
hB : B.IsSymmetric
i j : 𝕜 × 𝕜
hij : i ≠ j
v : E
x✝ : v ∈ eigenspace A i.2 ⊓ eigenspace B i.1
hv1 : v ∈ ↑(eigenspace A i.2)
hv2 : v ∈ ↑(eigenspace B i.1)
h₂ : i.2 ≠ j.2
w : E
hw1 : w ∈ ↑(eigenspace A j.2)
hw2 : w ∈ ↑(eigenspace B j.1)
⊢ inner 𝕜 w v = 0
Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace

Goal state before:
pp: case b
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
hT : ∀ (i : n), IsSymmetric (T i)
f g : n → 𝕜
hfg : f ≠ g
Ef : ↥(⨅ j, (T j).eigenspace (f j))
Eg : ↥(⨅ j, (T j).eigenspace (g j))
a : n
ha : f a ≠ g a
H : ∀ a_1 ∈ (T a).eigenspace (f a), ∀ a_2 ∈ (T a).eigenspace (g a), inner 𝕜 a_1 a_2 = 0
⊢ ((fun γ ↦ (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ) f) Ef ∈ (T a).eigenspace (f a)

pp: case b
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
hT : ∀ (i : n), IsSymmetric (T i)
f g : n → 𝕜
hfg : f ≠ g
Ef : ↥(⨅ j, (T j).eigenspace (f j))
Eg : ↥(⨅ j, (T j).eigenspace (g j))
a : n
ha : f a ≠ g a
H : ∀ a_1 ∈ (T a).eigenspace (f a), ∀ a_2 ∈ (T a).eigenspace (g a), inner 𝕜 a_1 a_2 = 0
⊢ ((fun γ ↦ (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ) g) Eg ∈ (T a).eigenspace (g a)

Tactic:
·

Goal state after:
case b
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
hT : ∀ (i : n), IsSymmetric (T i)
f g : n → 𝕜
hfg : f ≠ g
Ef : ↥(⨅ j, (T j).eigenspace (f j))
Eg : ↥(⨅ j, (T j).eigenspace (g j))
a : n
ha : f a ≠ g a
H : ∀ a_1 ∈ (T a).eigenspace (f a), ∀ a_2 ∈ (T a).eigenspace (g a), inner 𝕜 a_1 a_2 = 0
⊢ ((fun γ ↦ (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ) f) Ef ∈ (T a).eigenspace (f a)
Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace

Goal state before:
pp: case b
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
hT : ∀ (i : n), IsSymmetric (T i)
f g : n → 𝕜
hfg : f ≠ g
Ef : ↥(⨅ j, (T j).eigenspace (f j))
Eg : ↥(⨅ j, (T j).eigenspace (g j))
a : n
ha : f a ≠ g a
H : ∀ a_1 ∈ (T a).eigenspace (f a), ∀ a_2 ∈ (T a).eigenspace (g a), inner 𝕜 a_1 a_2 = 0
⊢ ((fun γ ↦ (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ) g) Eg ∈ (T a).eigenspace (g a)

Tactic:
·

Goal state after:
case b
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
hT : ∀ (i : n), IsSymmetric (T i)
f g : n → 𝕜
hfg : f ≠ g
Ef : ↥(⨅ j, (T j).eigenspace (f j))
Eg : ↥(⨅ j, (T j).eigenspace (g j))
a : n
ha : f a ≠ g a
H : ∀ a_1 ∈ (T a).eigenspace (f a), ∀ a_2 ∈ (T a).eigenspace (g a), inner 𝕜 a_1 a_2 = 0
⊢ ((fun γ ↦ (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ) g) Eg ∈ (T a).eigenspace (g a)
Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : DecidableEq (n → 𝕜)
hT : ∀ (i : n), IsSymmetric (T i)
hC : Pairwise (Commute on T)
⊢ (⨆ α, ⨅ j, (T j).eigenspace (α j))ᗮ = ⊥

pp: 𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : DecidableEq (n → 𝕜)
hT : ∀ (i : n), IsSymmetric (T i)
hC : Pairwise (Commute on T)
⊢ OrthogonalFamily 𝕜 (fun i ↦ ↥(⨅ j, (T j).eigenspace (i j))) fun i ↦ (⨅ j, (T j).eigenspace (i j)).subtypeₗᵢ

Tactic:
·

Goal state after:
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : DecidableEq (n → 𝕜)
hT : ∀ (i : n), IsSymmetric (T i)
hC : Pairwise (Commute on T)
⊢ (⨆ α, ⨅ j, (T j).eigenspace (α j))ᗮ = ⊥
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : RCLike 𝕜
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
x : H
h : ∀ (x : H), ‖x‖ * (‖x‖ * ↑c) ≤ ‖⟪f x, x⟫‖
hx0 : x = 0
⊢ ‖x‖ * ↑c ≤ ‖f x‖

pp: case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
x : H
h : ∀ (x : H), ‖x‖ * (‖x‖ * ↑c) ≤ ‖⟪f x, x⟫‖
hx0 : ¬x = 0
⊢ ‖x‖ * ↑c ≤ ‖f x‖

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : RCLike 𝕜
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
x : H
h : ∀ (x : H), ‖x‖ * (‖x‖ * ↑c) ≤ ‖⟪f x, x⟫‖
hx0 : x = 0
⊢ ‖x‖ * ↑c ≤ ‖f x‖
Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : DecidableEq (n → 𝕜)
hT : ∀ (i : n), IsSymmetric (T i)
hC : Pairwise (Commute on T)
⊢ OrthogonalFamily 𝕜 (fun i ↦ ↥(⨅ j, (T j).eigenspace (i j))) fun i ↦ (⨅ j, (T j).eigenspace (i j)).subtypeₗᵢ

Tactic:
·

Goal state after:
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : DecidableEq (n → 𝕜)
hT : ∀ (i : n), IsSymmetric (T i)
hC : Pairwise (Commute on T)
⊢ OrthogonalFamily 𝕜 (fun i ↦ ↥(⨅ j, (T j).eigenspace (i j))) fun i ↦ (⨅ j, (T j).eigenspace (i j)).subtypeₗᵢ
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
x : H
h : ∀ (x : H), ‖x‖ * (‖x‖ * ↑c) ≤ ‖⟪f x, x⟫‖
hx0 : ¬x = 0
⊢ ‖x‖ * ↑c ≤ ‖f x‖

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
x : H
h : ∀ (x : H), ‖x‖ * (‖x‖ * ↑c) ≤ ‖⟪f x, x⟫‖
hx0 : ¬x = 0
⊢ ‖x‖ * ↑c ≤ ‖f x‖
Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram

Goal state before:
pp: case pos
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
v : V
h : 0 < ‖v‖
⊢ C * ‖v‖ ≤ ‖(continuousLinearMapOfBilin B) v‖

pp: case neg
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
v : V
h : ¬0 < ‖v‖
⊢ C * ‖v‖ ≤ ‖(continuousLinearMapOfBilin B) v‖

Tactic:
·

Goal state after:
case pos
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
v : V
h : 0 < ‖v‖
⊢ C * ‖v‖ ≤ ‖(continuousLinearMapOfBilin B) v‖
Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram

Goal state before:
pp: case neg
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
v : V
h : ¬0 < ‖v‖
⊢ C * ‖v‖ ≤ ‖(continuousLinearMapOfBilin B) v‖

Tactic:
·

Goal state after:
case neg
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
v : V
h : ¬0 < ‖v‖
⊢ C * ‖v‖ ≤ ‖(continuousLinearMapOfBilin B) v‖
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
p : E →L[𝕜] E
hp : IsIdempotentElem p
tfae_2_iff_3 : IsStarNormal p ↔ IsSelfAdjoint p
tfae_3_iff_4 : IsSelfAdjoint p ↔ p.IsPositive
tfae_3_iff_1 : IsSelfAdjoint p ↔ (↑p).rangeᗮ = (↑p).ker
⊢ [(↑p).rangeᗮ = (↑p).ker, IsStarNormal p, IsSelfAdjoint p, p.IsPositive].TFAE

Tactic:
tfae_finish

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram

Goal state before:
pp: case a
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(↑(continuousLinearMapOfBilin B)).range
v w : V
mem_w_orthogonal : w ∈ (↑(continuousLinearMapOfBilin B)).rangeᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
⊢ C * ‖w‖ * ‖w‖ ≤ 0

pp: case a
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(↑(continuousLinearMapOfBilin B)).range
v w : V
mem_w_orthogonal : w ∈ (↑(continuousLinearMapOfBilin B)).rangeᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
⊢ 0 ≤ C * ‖w‖ * ‖w‖

Tactic:
·

Goal state after:
case a
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(↑(continuousLinearMapOfBilin B)).range
v w : V
mem_w_orthogonal : w ∈ (↑(continuousLinearMapOfBilin B)).rangeᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
⊢ C * ‖w‖ * ‖w‖ ≤ 0
Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram

Goal state before:
pp: case a
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(↑(continuousLinearMapOfBilin B)).range
v w : V
mem_w_orthogonal : w ∈ (↑(continuousLinearMapOfBilin B)).rangeᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
⊢ 0 ≤ C * ‖w‖ * ‖w‖

Tactic:
·

Goal state after:
case a
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(↑(continuousLinearMapOfBilin B)).range
v w : V
mem_w_orthogonal : w ∈ (↑(continuousLinearMapOfBilin B)).rangeᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
⊢ 0 ≤ C * ‖w‖ * ‖w‖
Module: Mathlib.Topology.Algebra.Module.LinearPMap

Goal state before:
pp: case pos
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : f.IsClosable
⊢ f ≤ f.closure

pp: case neg
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : ¬f.IsClosable
⊢ f ≤ f.closure

Tactic:
·

Goal state after:
case pos
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : f.IsClosable
⊢ f ≤ f.closure