ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : CancelCommMonoidWithZero R<VAR>inst✝⁴ : UniqueFactorizationMonoid R<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝¹ : CancelCommMonoidWithZero β<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>i : α → ℕ<VAR>p : α<VAR>hps : p ∉ s<VAR>is_prime : ∀ q ∈ insert p s, Prime q<VAR>is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'<VAR>hp : Prime p<VAR>d : α<VAR>hdprod : d ∣ ∏ p' ∈ s, p' ^ i p'<VAR>hd : Prime d<VAR>hdp : d ∣ p<VAR>q : α<VAR>q_mem : q ∈ s.val<VAR>q_mem' : q ^ i q ∈ Multiset.map (fun p' => p' ^ i p') s.val<VAR>hdq : d ∣ q ^ i q<GOAL>p ∈ s
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : CancelCommMonoidWithZero R<VAR>inst✝⁴ : UniqueFactorizationMonoid R<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝¹ : CancelCommMonoidWithZero β<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>i : α → ℕ<VAR>p : α<VAR>hps : p ∉ s<VAR>is_prime : ∀ q ∈ insert p s, Prime q<VAR>is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'<VAR>hp : Prime p<VAR>d : α<VAR>hdprod : d ∣ ∏ p' ∈ s, p' ^ i p'<VAR>hd : Prime d<VAR>hdp : d ∣ p<VAR>q : α<VAR>q_mem : q ∈ s.val<VAR>q_mem' : q ^ i q ∈ Multiset.map (fun p' => p' ^ i p') s.val<VAR>hdq : d ∣ q<GOAL>p ∈ s
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : CancelCommMonoidWithZero R<VAR>inst✝⁴ : UniqueFactorizationMonoid R<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝¹ : CancelCommMonoidWithZero β<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>i : α → ℕ<VAR>p : α<VAR>hps : p ∉ s<VAR>is_prime : ∀ q ∈ insert p s, Prime q<VAR>is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'<VAR>hp : Prime p<VAR>d : α<VAR>hdprod : d ∣ ∏ p' ∈ s, p' ^ i p'<VAR>hd : Prime d<VAR>hdp : d ∣ p<VAR>q : α<VAR>q_mem : q ∈ s.val<VAR>q_mem' : q ^ i q ∈ Multiset.map (fun p' => p' ^ i p') s.val<VAR>hdq : d ∣ q<VAR>this : p ∣ q<GOAL>p ∈ s
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : CancelCommMonoidWithZero R<VAR>inst✝⁴ : UniqueFactorizationMonoid R<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝¹ : CancelCommMonoidWithZero β<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>i : α → ℕ<VAR>p : α<VAR>hps : p ∉ s<VAR>is_prime : ∀ q ∈ insert p s, Prime q<VAR>is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'<VAR>hp : Prime p<VAR>d : α<VAR>hdprod : d ∣ ∏ p' ∈ s, p' ^ i p'<VAR>hd : Prime d<VAR>hdp : d ∣ p<VAR>q : α<VAR>q_mem : q ∈ s.val<VAR>q_mem' : q ^ i q ∈ Multiset.map (fun p' => p' ^ i p') s.val<VAR>hdq : d ∣ q<VAR>this : p ∣ q<GOAL>p ∈ s ↔ q ∈ s.val
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>hap : ↑a ≠ 0<GOAL>↑(p / 2)! ≠ 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>hap : ↑a ≠ 0<GOAL>p / 2 < p
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>hap : ↑a ≠ 0<GOAL>↑a ^ (p / 2) * ↑(p / 2)! = ↑((-1) ^ (filter (fun x => p / 2 < (↑a * ↑x).val) (Ico 1 (p / 2).succ)).card) * ↑(p / 2)!
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>G : C<GOAL>IsCodetector (op G) ↔ IsDetector G
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>c : Cardinal.{u}<VAR>α : Type u<VAR>h : ℵ₀ ≤ ⟦α⟧<GOAL>⟦α⟧ < ⟦α⟧ ^ (ord ⟦α⟧).cof
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>c : Cardinal.{u}<VAR>α : Type u<VAR>h : ℵ₀ ≤ ⟦α⟧<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>re : (#α).ord = type r<GOAL>⟦α⟧ < ⟦α⟧ ^ (ord ⟦α⟧).cof
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>c : Cardinal.{u}<VAR>α : Type u<VAR>h : ℵ₀ ≤ ⟦α⟧<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>re : (#α).ord = type r<VAR>this : (ord ⟦α⟧).IsLimit<GOAL>⟦α⟧ < ⟦α⟧ ^ (ord ⟦α⟧).cof
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>c : Cardinal.{u}<VAR>α : Type u<VAR>h : ℵ₀ ≤ ⟦α⟧<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>re : (#α).ord = type r<VAR>this : (type r).IsLimit<GOAL>#α < #α ^ (type r).cof
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>c : Cardinal.{u}<VAR>α : Type u<VAR>h : ℵ₀ ≤ ⟦α⟧<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>re : (#α).ord = type r<VAR>this : (type r).IsLimit<VAR>S : Set α<VAR>H : ∀ (a : α), ∃ b ∈ S, r a b<VAR>Se : #↑S = (type r).cof<GOAL>#α < #α ^ (type r).cof
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>c : Cardinal.{u}<VAR>α : Type u<VAR>h : ℵ₀ ≤ ⟦α⟧<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>re : (#α).ord = type r<VAR>this✝ : (type r).IsLimit<VAR>S : Set α<VAR>H : ∀ (a : α), ∃ b ∈ S, r a b<VAR>Se : #↑S = (type r).cof<VAR>this : (sum fun a => #{ x // r x ↑a }) < prod fun x => #α<GOAL>#α < #α ^ (type r).cof
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>c : Cardinal.{u}<VAR>α : Type u<VAR>h : ℵ₀ ≤ ⟦α⟧<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>re : (#α).ord = type r<VAR>this : (type r).IsLimit<VAR>S : Set α<VAR>H : ∀ (a : α), ∃ b ∈ S, r a b<VAR>Se : #↑S = (type r).cof<VAR>i : ↑S<GOAL>(fun a => #{ x // r x ↑a }) i < (fun x => #α) i
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝⁴ : Category.{v₃, u₃} E<VAR>F : C ⥤ D<VAR>inst✝³ : F.ReflectsIsomorphisms<VAR>inst✝² : F.PreservesEpimorphisms<VAR>inst✝¹ : F.PreservesMonomorphisms<VAR>inst✝ : Balanced D<VAR>X✝ Y✝ : C<VAR>f : X✝ ⟶ Y✝<VAR>x✝¹ : Mono f<VAR>x✝ : Epi f<GOAL>IsIso f
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝⁴ : Category.{v₃, u₃} E<VAR>F : C ⥤ D<VAR>inst✝³ : F.ReflectsIsomorphisms<VAR>inst✝² : F.PreservesEpimorphisms<VAR>inst✝¹ : F.PreservesMonomorphisms<VAR>inst✝ : Balanced D<VAR>X✝ Y✝ : C<VAR>f : X✝ ⟶ Y✝<VAR>x✝¹ : Mono f<VAR>x✝ : Epi f<GOAL>IsIso (F.map f)
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Zero M<VAR>s : Multiset (ι →₀ M)<VAR>x : ι<VAR>x✝ : List (ι →₀ M)<GOAL>x ∈ (map Finsupp.support (Quot.mk Setoid.r x✝)).sup ↔ ∃ f ∈ Quot.mk Setoid.r x✝, x ∈ f.support
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{v}<GOAL>Cardinal.lift.{u, v} o.cof = (lift.{u, v} o).cof
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{v}<GOAL>∀ (α : Type v) (r : α → α → Prop) [inst : IsWellOrder α r], Cardinal.lift.{u, v} (type r).cof = (lift.{u, v} (type r)).cof
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>o : Ordinal.{v}<VAR>α : Type v<VAR>r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<GOAL>Cardinal.lift.{u, v} (type r).cof = (lift.{u, v} (type r)).cof
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>o : Ordinal.{v}<VAR>α : Type v<VAR>r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<GOAL>Cardinal.lift.{u, v} (type r).cof ≤ (lift.{u, v} (type r)).cof
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>o : Ordinal.{v}<VAR>α : Type v<VAR>r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<GOAL>(lift.{u, v} (type r)).cof ≤ Cardinal.lift.{u, v} (type r).cof
<GOAL>riemannZeta 4 = ↑π ^ 4 / 90
<GOAL>riemannZeta 4 = ↑(∑' (b : ℕ), 1 / ↑b ^ 4)
<GOAL>↑π ^ 4 / 90 = ↑(π ^ 4 / 90)
<VAR>α✝ : Type u_1<VAR>inst✝¹ : MeasurableSpace α✝<VAR>μ✝ : Measure α✝<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>p q : ℝ<VAR>hp✝ : 0 ≤ p<VAR>hq✝ : 0 ≤ q<VAR>hpq : p + q = 1<VAR>hp : 0 < p<VAR>hq : 0 < q<GOAL>∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q
<VAR>α✝ : Type u_1<VAR>inst✝¹ : MeasurableSpace α✝<VAR>μ✝ : Measure α✝<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>p q : ℝ<VAR>hp✝ : 0 ≤ p<VAR>hq✝ : 0 ≤ q<VAR>hpq : p + q = 1<VAR>hp : 0 < p<VAR>hq : 0 < q<VAR>h2p : 1 < 1 / p<GOAL>∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q
<VAR>α✝ : Type u_1<VAR>inst✝¹ : MeasurableSpace α✝<VAR>μ✝ : Measure α✝<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>p q : ℝ<VAR>hp✝ : 0 ≤ p<VAR>hq✝ : 0 ≤ q<VAR>hpq : p + q = 1<VAR>hp : 0 < p<VAR>hq : 0 < q<VAR>h2p : 1 < 1 / p<VAR>h2pq : (1 / p)⁻¹ + (1 / q)⁻¹ = 1<GOAL>∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q
<VAR>α✝ : Type u_1<VAR>inst✝¹ : MeasurableSpace α✝<VAR>μ✝ : Measure α✝<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>p q : ℝ<VAR>hp✝ : 0 ≤ p<VAR>hq✝ : 0 ≤ q<VAR>hpq : p + q = 1<VAR>hp : 0 < p<VAR>hq : 0 < q<VAR>h2p : 1 < 1 / p<VAR>h2pq : (1 / p)⁻¹ + (1 / q)⁻¹ = 1<VAR>this : ∫⁻ (a : α), ((fun x => f x ^ p) * fun x => g x ^ q) a ∂μ ≤ (∫⁻ (a : α), (f a ^ p) ^ (1 / p) ∂μ) ^ (1 / (1 / p)) * (∫⁻ (a : α), (g a ^ q) ^ (1 / q) ∂μ) ^ (1 / (1 / q))<GOAL>∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤<VAR>hg : AEMeasurable g μ<VAR>hg_top : ∫⁻ (a : α), g a ^ p ∂μ ≠ ⊤<VAR>h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0<VAR>h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ⊤<GOAL>(∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤<VAR>hg : AEMeasurable g μ<VAR>hg_top : ∫⁻ (a : α), g a ^ p ∂μ ≠ ⊤<VAR>h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0<VAR>h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ⊤<VAR>hp_not_nonpos : ¬p ≤ 0<GOAL>(∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤<VAR>hg : AEMeasurable g μ<VAR>hg_top : ∫⁻ (a : α), g a ^ p ∂μ ≠ ⊤<VAR>h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0<VAR>h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ⊤<VAR>hp_not_nonpos : ¬p ≤ 0<VAR>htop_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ ⊤<GOAL>(∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤<VAR>hg : AEMeasurable g μ<VAR>hg_top : ∫⁻ (a : α), g a ^ p ∂μ ≠ ⊤<VAR>h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0<VAR>h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ⊤<VAR>hp_not_nonpos : ¬p ≤ 0<VAR>htop_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ ⊤<VAR>h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0<GOAL>(∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤<VAR>hg : AEMeasurable g μ<VAR>hg_top : ∫⁻ (a : α), g a ^ p ∂μ ≠ ⊤<VAR>h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0<VAR>h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ⊤<VAR>hp_not_nonpos : ¬p ≤ 0<VAR>htop_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ ⊤<VAR>h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0<GOAL>1 ≤ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) * ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤<VAR>hg : AEMeasurable g μ<VAR>hg_top : ∫⁻ (a : α), g a ^ p ∂μ ≠ ⊤<VAR>h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0<VAR>h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ⊤<VAR>hp_not_nonpos : ¬p ≤ 0<VAR>htop_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ ⊤<VAR>h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0<VAR>h : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤ ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) * (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / q)<GOAL>1 ≤ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) * ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤<VAR>hg : AEMeasurable g μ<VAR>hg_top : ∫⁻ (a : α), g a ^ p ∂μ ≠ ⊤<VAR>h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0<VAR>h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ⊤<VAR>hp_not_nonpos : ¬p ≤ 0<VAR>htop_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ ⊤<VAR>h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0<VAR>h : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤ ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) * (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / q)<VAR>h_one_div_q : 1 / q = 1 - 1 / p<GOAL>1 ≤ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) * ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤<VAR>hg : AEMeasurable g μ<VAR>hg_top : ∫⁻ (a : α), g a ^ p ∂μ ≠ ⊤<VAR>h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0<VAR>h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ⊤<VAR>hp_not_nonpos : ¬p ≤ 0<VAR>htop_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ ⊤<VAR>h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0<VAR>h_one_div_q : 1 / q = 1 - 1 / p<VAR>h : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤ ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) * ((∫⁻ (a : α), (f + g) a ^ p ∂μ) * (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)))<GOAL>1 ≤ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) * ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤<VAR>hg : AEMeasurable g μ<VAR>hg_top : ∫⁻ (a : α), g a ^ p ∂μ ≠ ⊤<VAR>h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0<VAR>h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ⊤<VAR>hp_not_nonpos : ¬p ≤ 0<VAR>htop_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ ⊤<VAR>h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0<VAR>h_one_div_q : 1 / q = 1 - 1 / p<VAR>h : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤ ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) * ((∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) * ∫⁻ (a : α), (f + g) a ^ p ∂μ)<GOAL>1 ≤ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) * ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤<VAR>hg : AEMeasurable g μ<VAR>hg_top : ∫⁻ (a : α), g a ^ p ∂μ ≠ ⊤<VAR>h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0<VAR>h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ⊤<VAR>hp_not_nonpos : ¬p ≤ 0<VAR>htop_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ ⊤<VAR>h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0<VAR>h_one_div_q : 1 / q = 1 - 1 / p<VAR>h : 1 * ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤ ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) * ((∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) * ∫⁻ (a : α), (f + g) a ^ p ∂μ)<GOAL>1 ≤ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) * ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>S : Type u_3<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : Semiring S<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M₂<VAR>inst✝⁹ : AddCommMonoid M₃<VAR>inst✝⁸ : AddCommMonoid M₄<VAR>inst✝⁷ : AddCommMonoid M₅<VAR>inst✝⁶ : AddCommMonoid M₆<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M₄<VAR>inst✝¹ : Module R M₅<VAR>inst✝ : Module R M₆<VAR>f : M →ₗ[R] M₂<GOAL>(inl R M M₂).coprod (inr R M M₂) = id
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c d : ℝ<GOAL>Continuous fun x => 1 + x ^ 2
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c d x : ℝ<GOAL>1 + x ^ 2 ≠ 0
<VAR>o : ONote<VAR>x✝ : NF 0<VAR>h₂ : o.NF<GOAL>(0 * o).repr = repr 0 * o.repr
<VAR>e₁ : ONote<VAR>n₁ : ℕ+<VAR>a₁ e₂ : ONote<VAR>n₂ : ℕ+<VAR>a₂ : ONote<VAR>h₁ : (e₁.oadd n₁ a₁).NF<VAR>h₂ : (e₂.oadd n₂ a₂).NF<GOAL>(e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr
<VAR>e₁ : ONote<VAR>n₁ : ℕ+<VAR>a₁ e₂ : ONote<VAR>n₂ : ℕ+<VAR>a₂ : ONote<VAR>h₁ : (e₁.oadd n₁ a₁).NF<VAR>h₂ : (e₂.oadd n₂ a₂).NF<VAR>IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr<GOAL>(e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr
<VAR>e₁ : ONote<VAR>n₁ : ℕ+<VAR>a₁ e₂ : ONote<VAR>n₂ : ℕ+<VAR>a₂ : ONote<VAR>h₁ : (e₁.oadd n₁ a₁).NF<VAR>h₂ : (e₂.oadd n₂ a₂).NF<VAR>IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr<GOAL>(Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr
<VAR>e₁ : ONote<VAR>n₁ : ℕ+<VAR>a₁ e₂ : ONote<VAR>n₂ : ℕ+<VAR>a₂ : ONote<VAR>h₁ : (e₁.oadd n₁ a₁).NF<VAR>h₂ : (e₂.oadd n₂ a₂).NF<VAR>IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr<VAR>ao : a₁.repr + ω ^ e₁.repr * ↑↑n₁ = ω ^ e₁.repr * ↑↑n₁<GOAL>(Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<GOAL>λ * S.b = λ * S.b
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>μ : R<VAR>k : ℕ<VAR>hμ : f.HasGenEigenvalue μ k<VAR>contra : f.eigenspace μ = ⊥<GOAL>(f.genEigenspace μ) k = ⊥
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>μ : R<VAR>k : ℕ<VAR>hμ : f.HasGenEigenvalue μ k<VAR>contra : Function.Injective ⇑(f - (algebraMap R (End R M)) μ)<GOAL>Function.Injective ⇑((f - (algebraMap R (End R M)) μ) ^ k)
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>μ : R<VAR>k : ℕ<VAR>hμ : f.HasGenEigenvalue μ k<VAR>contra : Function.Injective ⇑(f - (algebraMap R (End R M)) μ)<GOAL>Function.Injective (⇑(f - (algebraMap R (End R M)) μ))^[k]
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → SemilatticeSup (π i)<VAR>f : (i : ι) → π i<VAR>i : ι<VAR>a b : π i<VAR>j : ι<GOAL>update f i (a ⊔ b) j = (update f i a ⊔ update f i b) j
<VAR>ι✝ : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι✝ → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>ι : Type u_8<VAR>f : ι → M<VAR>hf : LinearIndependent R f<VAR>a✝ : Nontrivial R<GOAL>LinearIndependent (ι := { x // x ∈ range f }) R Subtype.val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>hs : MeasurableSet s<VAR>hst : s ⊆ t<VAR>hs' : μ s ≠ ⊤<VAR>ε : ℝ≥0∞<GOAL>μ (t \ s) ≤ ε ↔ μ t ≤ μ s + ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<GOAL>re ⟪x + y, x + y⟫_𝕜 = re ⟪x, x⟫_𝕜 + 2 * re ⟪x, y⟫_𝕜 + re ⟪y, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<GOAL>re (⟪x, x⟫_𝕜 + ⟪x, y⟫_𝕜 + ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜) = re ⟪x, x⟫_𝕜 + (re ⟪x, y⟫_𝕜 + re ⟪x, y⟫_𝕜) + re ⟪y, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<GOAL>re ⟪y, x⟫_𝕜 = re ⟪x, y⟫_𝕜
<VAR>z : ℍ<VAR>c d : ℝ<VAR>hd : 1 ≤ d ^ 2<VAR>H1 : (c * z.re + d) ^ 2 + (c * z.im) ^ 2 = c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2<VAR>H2 : (c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2) * (z.re ^ 2 + z.im ^ 2) - z.im ^ 2 = (c * (z.re ^ 2 + z.im ^ 2) + d * z.re) ^ 2 + (d ^ 2 - 1) * z.im ^ 2<GOAL>r1 z ≤ (c * z.re + d) ^ 2 + (c * z.im) ^ 2
<VAR>z : ℍ<VAR>c d : ℝ<VAR>hd : 1 ≤ d ^ 2<VAR>H1 : (c * z.re + d) ^ 2 + (c * z.im) ^ 2 = c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2<VAR>H2 : (c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2) * (z.re ^ 2 + z.im ^ 2) - z.im ^ 2 = (c * (z.re ^ 2 + z.im ^ 2) + d * z.re) ^ 2 + (d ^ 2 - 1) * z.im ^ 2<GOAL>0 ≤ (c * (z.re ^ 2 + z.im ^ 2) + d * z.re) ^ 2 + (d ^ 2 - 1) * z.im ^ 2
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>ι : Type u_1<VAR>l : List ι<VAR>f : ι → R[X]<VAR>n : ℕ<GOAL>(List.map f l).sum.coeff n = (List.map (fun a => (f a).coeff n) l).sum
<VAR>α : Type u_1<VAR>g : Set (Set α)<GOAL>generateFrom (generatePiSystem g) = generateFrom g
<VAR>α : Type u_1<VAR>g : Set (Set α)<GOAL>∀ t ∈ generatePiSystem g, MeasurableSet t
<VAR>α : Type u_1<VAR>g : Set (Set α)<GOAL>∀ t ∈ g, MeasurableSet t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r✝ R r : ℝ≥0<VAR>hr : ↑r < p.radius<VAR>k : ℕ<GOAL>Summable fun l => ‖p.changeOriginSeries k l‖₊ * r ^ l
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r✝ R r : ℝ≥0<VAR>hr : ↑r < p.radius<VAR>k n : ℕ<GOAL>‖p.changeOriginSeries k n‖₊ * r ^ n ≤ ∑' (y : { s // s.card = n }), ‖p (k + ⟨n, y⟩.fst)‖₊ * r ^ ⟨n, y⟩.fst
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r✝ R r : ℝ≥0<VAR>hr : ↑r < p.radius<VAR>k n : ℕ<GOAL>‖p.changeOriginSeries k n‖₊ * r ^ n ≤ (∑' (x : { s // s.card = n }), ‖p (k + n)‖₊) * r ^ n