ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝³ : Semiring R<VAR>r : R<VAR>p : R[X]<VAR>S : Type u_2<VAR>inst✝² : AddCommMonoid S<VAR>inst✝¹ : Pow S ℕ<VAR>inst✝ : MulActionWithZero R S<VAR>x : S<GOAL>1 • x ^ 0 = 1 • x ^ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h₁ : min a b ≤ max c d<VAR>h₂ : min c d ≤ max a b<GOAL>Ico a b ∪ Ico c d = Ico (min a c) (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hab : a ≤ b<VAR>hcd : c ≤ d<VAR>h₁ : a ≤ d<VAR>h₂ : c ≤ b<GOAL>Ico a b ∪ Ico c d = Ico (min a c) (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hab : a ≤ b<VAR>hcd : d ≤ c<VAR>h₁ : a ≤ c<VAR>h₂ : d ≤ b<GOAL>Ico a b ∪ Ico c d = Ico (min a c) (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hab : b ≤ a<VAR>hcd : c ≤ d<VAR>h₁ : b ≤ d<VAR>h₂ : c ≤ a<GOAL>Ico a b ∪ Ico c d = Ico (min a c) (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hab : b ≤ a<VAR>hcd : d ≤ c<VAR>h₁ : b ≤ c<VAR>h₂ : d ≤ a<GOAL>Ico a b ∪ Ico c d = Ico (min a c) (max b d)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>x : X<VAR>s : Set X<GOAL>{x}ᶜ ∈ 𝓝ˢ s ↔ x ∉ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<GOAL>b \ a ∆ b = a ⊓ b
<VAR>n m : ℕ<VAR>p : Fin (n + 1)<VAR>i j : Fin n<VAR>a : Fin (n + 2)<VAR>h : a ≠ last (n + 1)<GOAL>a.succAbove (last n) = last (n + 1)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : Measure α<VAR>p : α → (ι → β) → Prop<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>x : α<VAR>hx : x ∈ aeSeqSet hf p<VAR>i : ι<GOAL>aeSeq hf p i x = f i x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁶ : CommRing R<VAR>M N : Matrix m m R<VAR>b : m → α<VAR>inst✝⁵ : DecidableEq m<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Invertible M<VAR>hM : M.BlockTriangular b<VAR>k : α<VAR>p : m → Prop := fun i => b i < k<VAR>q : m → Prop := fun i => ¬b i < k<GOAL>(M⁻¹.toBlock (fun i => k ≤ b i) fun i => b i < k) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁶ : CommRing R<VAR>M N : Matrix m m R<VAR>b : m → α<VAR>inst✝⁵ : DecidableEq m<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Invertible M<VAR>hM : M.BlockTriangular b<VAR>k : α<VAR>p : m → Prop := fun i => b i < k<VAR>q : m → Prop := fun i => ¬b i < k<VAR>h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0<GOAL>(M⁻¹.toBlock (fun i => k ≤ b i) fun i => b i < k) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁶ : CommRing R<VAR>M N : Matrix m m R<VAR>b : m → α<VAR>inst✝⁵ : DecidableEq m<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Invertible M<VAR>hM : M.BlockTriangular b<VAR>k : α<VAR>p : m → Prop := fun i => b i < k<VAR>q : m → Prop := fun i => ¬b i < k<VAR>h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0<VAR>h_zero : M.toBlock q p = 0<GOAL>(M⁻¹.toBlock (fun i => k ≤ b i) fun i => b i < k) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁶ : CommRing R<VAR>M N : Matrix m m R<VAR>b : m → α<VAR>inst✝⁵ : DecidableEq m<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Invertible M<VAR>hM : M.BlockTriangular b<VAR>k : α<VAR>p : m → Prop := fun i => b i < k<VAR>q : m → Prop := fun i => ¬b i < k<VAR>h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0<VAR>h_zero : M.toBlock q p = 0<VAR>h_mul_eq_zero : M⁻¹.toBlock q p * M.toBlock p p = 0<VAR>this : Invertible (M.toBlock p p)<GOAL>(M⁻¹.toBlock (fun i => k ≤ b i) fun i => b i < k) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁶ : CommRing R<VAR>M N : Matrix m m R<VAR>b : m → α<VAR>inst✝⁵ : DecidableEq m<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Invertible M<VAR>hM : M.BlockTriangular b<VAR>k : α<VAR>p : m → Prop := fun i => b i < k<VAR>q : m → Prop := fun i => ¬b i < k<VAR>h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0<VAR>h_zero : M.toBlock q p = 0<VAR>h_mul_eq_zero : M⁻¹.toBlock q p * M.toBlock p p = 0<VAR>this✝ : Invertible (M.toBlock p p)<VAR>this : (fun i => k ≤ b i) = q<GOAL>(M⁻¹.toBlock (fun i => k ≤ b i) fun i => b i < k) = 0
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x : α<VAR>s t : Set α<VAR>r : ℝ<VAR>c : α<GOAL>comap (dist c) atTop = cobounded α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>M : Type u_3<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : TopologicalSpace M<VAR>v : VectorMeasure α M<VAR>f : α → β<VAR>hf : Measurable f<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>↑(v.map f) s = ↑v (f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>M : Type u_3<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : TopologicalSpace M<VAR>v : VectorMeasure α M<VAR>f : α → β<VAR>hf : Measurable f<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>↑{ measureOf' := fun s => if MeasurableSet s then ↑v (f ⁻¹' s) else 0, empty' := ⋯, not_measurable' := ⋯, m_iUnion' := ⋯ } s = ↑v (f ⁻¹' s)
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsFiltered J<VAR>F : J ⥤ ModuleCatMax R<VAR>x : ↑(M F)<GOAL>1 • x = x
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsFiltered J<VAR>F : J ⥤ ModuleCatMax R<VAR>x : ↑(M F)<GOAL>∀ (a : (j : J) × ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙ forget AddMonCat).obj j), 1 • Quot.mk (Types.Quot.Rel ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙ forget AddMonCat)) a = Quot.mk (Types.Quot.Rel ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙ forget AddMonCat)) a
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsFiltered J<VAR>F : J ⥤ ModuleCatMax R<VAR>j : J<VAR>x : ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙ forget AddMonCat).obj j<GOAL>1 • Quot.mk (Types.Quot.Rel ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙ forget AddMonCat)) ⟨j, x⟩ = Quot.mk (Types.Quot.Rel ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙ forget AddMonCat)) ⟨j, x⟩
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsFiltered J<VAR>F : J ⥤ ModuleCatMax R<VAR>j : J<VAR>x : ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙ forget AddMonCat).obj j<GOAL>M.mk F ⟨⟨j, x⟩.fst, 1 • ⟨j, x⟩.snd⟩ = Quot.mk (Types.Quot.Rel ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙ forget AddMonCat)) ⟨j, x⟩
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E✝<VAR>inst✝¹¹ : NormedSpace ℝ E✝<VAR>hE : CompleteSpace E✝<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E✝<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E✝<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g✝ : α → E✝<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α<VAR>E : Type u_7<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : Memℒp f (ENNReal.ofReal p) μ<VAR>hg : Memℒp g (ENNReal.ofReal q) μ<GOAL>∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ ≤ (∫ (a : α), ‖f a‖ ^ p ∂μ) ^ (1 / p) * (∫ (a : α), ‖g a‖ ^ q ∂μ) ^ (1 / q)
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E✝<VAR>inst✝¹¹ : NormedSpace ℝ E✝<VAR>hE : CompleteSpace E✝<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E✝<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E✝<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g✝ : α → E✝<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α<VAR>E : Type u_7<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : Memℒp f (ENNReal.ofReal p) μ<VAR>hg : Memℒp g (ENNReal.ofReal q) μ<GOAL>(∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤ (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ).toReal ^ (1 / p) * (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ).toReal ^ (1 / q)
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E✝<VAR>inst✝¹¹ : NormedSpace ℝ E✝<VAR>hE : CompleteSpace E✝<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E✝<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E✝<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g✝ : α → E✝<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α<VAR>E : Type u_7<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : Memℒp f (ENNReal.ofReal p) μ<VAR>hg : Memℒp g (ENNReal.ofReal q) μ<GOAL>0 ≤ᶠ[ae μ] fun a => ‖g a‖ ^ q
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E✝<VAR>inst✝¹¹ : NormedSpace ℝ E✝<VAR>hE : CompleteSpace E✝<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E✝<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E✝<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g✝ : α → E✝<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α<VAR>E : Type u_7<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : Memℒp f (ENNReal.ofReal p) μ<VAR>hg : Memℒp g (ENNReal.ofReal q) μ<GOAL>AEStronglyMeasurable (fun a => ‖g a‖ ^ q) μ
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E✝<VAR>inst✝¹¹ : NormedSpace ℝ E✝<VAR>hE : CompleteSpace E✝<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E✝<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E✝<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g✝ : α → E✝<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α<VAR>E : Type u_7<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : Memℒp f (ENNReal.ofReal p) μ<VAR>hg : Memℒp g (ENNReal.ofReal q) μ<GOAL>0 ≤ᶠ[ae μ] fun a => ‖f a‖ ^ p
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E✝<VAR>inst✝¹¹ : NormedSpace ℝ E✝<VAR>hE : CompleteSpace E✝<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E✝<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E✝<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g✝ : α → E✝<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α<VAR>E : Type u_7<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : Memℒp f (ENNReal.ofReal p) μ<VAR>hg : Memℒp g (ENNReal.ofReal q) μ<GOAL>AEStronglyMeasurable (fun a => ‖f a‖ ^ p) μ
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E✝<VAR>inst✝¹¹ : NormedSpace ℝ E✝<VAR>hE : CompleteSpace E✝<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E✝<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E✝<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g✝ : α → E✝<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α<VAR>E : Type u_7<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : Memℒp f (ENNReal.ofReal p) μ<VAR>hg : Memℒp g (ENNReal.ofReal q) μ<GOAL>0 ≤ᶠ[ae μ] fun a => ‖f a‖ * ‖g a‖
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E✝<VAR>inst✝¹¹ : NormedSpace ℝ E✝<VAR>hE : CompleteSpace E✝<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E✝<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E✝<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g✝ : α → E✝<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α<VAR>E : Type u_7<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : Memℒp f (ENNReal.ofReal p) μ<VAR>hg : Memℒp g (ENNReal.ofReal q) μ<GOAL>AEStronglyMeasurable (fun a => ‖f a‖ * ‖g a‖) μ
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E✝<VAR>inst✝¹¹ : NormedSpace ℝ E✝<VAR>hE : CompleteSpace E✝<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E✝<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E✝<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g✝ : α → E✝<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α<VAR>E : Type u_7<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : Memℒp f (ENNReal.ofReal p) μ<VAR>hg : Memℒp g (ENNReal.ofReal q) μ<GOAL>(∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤ ((∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ) ^ (1 / p) * (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ) ^ (1 / q)).toReal
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E✝<VAR>inst✝¹¹ : NormedSpace ℝ E✝<VAR>hE : CompleteSpace E✝<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E✝<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E✝<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g✝ : α → E✝<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α<VAR>E : Type u_7<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : Memℒp f (ENNReal.ofReal p) μ<VAR>hg : Memℒp g (ENNReal.ofReal q) μ<VAR>h_left : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ((fun x => ↑‖f x‖₊) * fun x => ↑‖g x‖₊) a ∂μ<GOAL>(∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤ ((∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ) ^ (1 / p) * (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ) ^ (1 / q)).toReal
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E✝<VAR>inst✝¹¹ : NormedSpace ℝ E✝<VAR>hE : CompleteSpace E✝<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E✝<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E✝<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g✝ : α → E✝<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α<VAR>E : Type u_7<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : Memℒp f (ENNReal.ofReal p) μ<VAR>hg : Memℒp g (ENNReal.ofReal q) μ<VAR>h_left : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ((fun x => ↑‖f x‖₊) * fun x => ↑‖g x‖₊) a ∂μ<VAR>h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ<GOAL>(∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤ ((∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ) ^ (1 / p) * (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ) ^ (1 / q)).toReal
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E✝<VAR>inst✝¹¹ : NormedSpace ℝ E✝<VAR>hE : CompleteSpace E✝<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E✝<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E✝<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g✝ : α → E✝<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α<VAR>E : Type u_7<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : Memℒp f (ENNReal.ofReal p) μ<VAR>hg : Memℒp g (ENNReal.ofReal q) μ<VAR>h_left : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ((fun x => ↑‖f x‖₊) * fun x => ↑‖g x‖₊) a ∂μ<VAR>h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ<VAR>h_right_g : ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ↑‖g a‖₊ ^ q ∂μ<GOAL>(∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤ ((∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ) ^ (1 / p) * (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ) ^ (1 / q)).toReal
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E✝<VAR>inst✝¹¹ : NormedSpace ℝ E✝<VAR>hE : CompleteSpace E✝<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E✝<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E✝<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g✝ : α → E✝<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α<VAR>E : Type u_7<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : Memℒp f (ENNReal.ofReal p) μ<VAR>hg : Memℒp g (ENNReal.ofReal q) μ<VAR>h_left : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ((fun x => ↑‖f x‖₊) * fun x => ↑‖g x‖₊) a ∂μ<VAR>h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ<VAR>h_right_g : ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ↑‖g a‖₊ ^ q ∂μ<GOAL>(∫⁻ (a : α), ((fun x => ↑‖f x‖₊) * fun x => ↑‖g x‖₊) a ∂μ).toReal ≤ ((∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), ↑‖g a‖₊ ^ q ∂μ) ^ (1 / q)).toReal
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E✝<VAR>inst✝¹¹ : NormedSpace ℝ E✝<VAR>hE : CompleteSpace E✝<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E✝<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E✝<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g✝ : α → E✝<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α<VAR>E : Type u_7<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : Memℒp f (ENNReal.ofReal p) μ<VAR>hg : Memℒp g (ENNReal.ofReal q) μ<VAR>h_left : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ((fun x => ↑‖f x‖₊) * fun x => ↑‖g x‖₊) a ∂μ<VAR>h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ<VAR>h_right_g : ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ↑‖g a‖₊ ^ q ∂μ<GOAL>(∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), ↑‖g a‖₊ ^ q ∂μ) ^ (1 / q) ≠ ⊤
<VAR>α : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E✝<VAR>inst✝¹¹ : NormedSpace ℝ E✝<VAR>hE : CompleteSpace E✝<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E✝<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E✝<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g✝ : α → E✝<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α<VAR>E : Type u_7<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : Memℒp f (ENNReal.ofReal p) μ<VAR>hg : Memℒp g (ENNReal.ofReal q) μ<VAR>h_left : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ((fun x => ↑‖f x‖₊) * fun x => ↑‖g x‖₊) a ∂μ<VAR>h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ<VAR>h_right_g : ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ↑‖g a‖₊ ^ q ∂μ<GOAL>∫⁻ (a : α), ((fun x => ↑‖f x‖₊) * fun x => ↑‖g x‖₊) a ∂μ ≤ (∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), ↑‖g a‖₊ ^ q ∂μ) ^ (1 / q)
<VAR>s : ℂ<VAR>h2 : s ≠ 0<VAR>n : ℕ := ⌊1 - s.re⌋₊<GOAL>Gamma (s + 1) = s * Gamma s
<VAR>s : ℂ<VAR>h2 : s ≠ 0<VAR>n : ℕ := ⌊1 - s.re⌋₊<VAR>t1 : -s.re < ↑n<GOAL>Gamma (s + 1) = s * Gamma s
<VAR>s : ℂ<VAR>h2 : s ≠ 0<VAR>n : ℕ := ⌊1 - s.re⌋₊<VAR>t1 : -s.re < ↑n<VAR>t2 : -(s + 1).re < ↑n<GOAL>Gamma (s + 1) = s * Gamma s
<VAR>s : ℂ<VAR>h2 : s ≠ 0<VAR>n : ℕ := ⌊1 - s.re⌋₊<VAR>t1 : -s.re < ↑n<VAR>t2 : -(s + 1).re < ↑n<GOAL>GammaAux n (s + 1) = s * (GammaAux n (s + 1) / s)
<VAR>f g : ℂ → ℂ<VAR>s : Set ℂ<VAR>f' g' x c : ℂ<GOAL>((g x * f x ^ (g x - 1)) • ContinuousLinearMap.smulRight 1 f' + (f x ^ g x * log (f x)) • ContinuousLinearMap.smulRight 1 g') 1 = g x * f x ^ (g x - 1) * f' + f x ^ g x * log (f x) * g'
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<GOAL>Orthonormal 𝕜 fun i => single i 1