ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{?u.24208, u_2} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : Preregular C<VAR>inst✝² : FinitaryPreExtensive C<VAR>F G : Cᵒᵖ ⥤ Type w<VAR>f : F ⟶ G<VAR>inst✝¹ : PreservesFiniteProducts F<VAR>inst✝ : PreservesFiniteProducts G<VAR>U✝ : C<VAR>y : (forget (Type w)).obj (G.obj (op U✝))<VAR>α : Type<VAR>w✝ : Finite α<VAR>Z : α → C<VAR>π : (a : α) → Z a ⟶ U✝<VAR>h : EffectiveEpiFamily Z π<VAR>h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)<VAR>x : (a : α) → F.obj (op (Z a)) := fun a => Exists.choose ⋯<VAR>x✝ : Fintype α := Fintype.ofFinite α<VAR>i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (∐ Z)) := (Types.productIso fun a => F.obj (op (Z a))).symm ≪≫ (PreservesProduct.iso F fun a => op (Z a)).symm ≪≫ F.mapIso (opCoproductIsoProduct Z).symm<VAR>this✝ : PreservesLimitsOfShape (Discrete α)ᵒᵖ G<VAR>a : α<VAR>this : f.app (op (Z a)) (x a) = G.map (π a).op y<GOAL>(f.app (op (Z a))) ((F.map (Sigma.ι Z a).op) (F.map (opCoproductIsoProduct Z).inv ((PreservesProduct.iso F fun a => op (Z a)).inv ((Types.productIso fun a => F.obj (op (Z a))).inv x)))) = (G.map (Sigma.ι Z a).op) ((G.map (Sigma.desc π).op) y)
<VAR>p : ℕ<VAR>x✝ : Fact (Nat.Prime p)<VAR>a : ℤ<GOAL>legendreSym p a = fastLegendreSym p a
<VAR>x✝ y x : ℝ<VAR>hx : 0 < x<GOAL>cosh (log x) = (x + x⁻¹) / 2
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Field α<GOAL>IsPrimePow ‖α‖
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Field α<VAR>p : ℕ<VAR>h✝ : CharP α p<GOAL>IsPrimePow ‖α‖
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Field α<VAR>p : ℕ<VAR>h✝ : CharP α p<VAR>hp : Fact (Nat.Prime p)<GOAL>IsPrimePow ‖α‖
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Field α<VAR>p : ℕ<VAR>h✝ : CharP α p<VAR>hp : Fact (Nat.Prime p)<VAR>this : Algebra (ZMod p) α := ZMod.algebra α p<VAR>b : Basis { x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) α } (ZMod p) α := IsNoetherian.finsetBasis (ZMod p) α<GOAL>IsPrimePow ‖α‖
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Field α<VAR>p : ℕ<VAR>h✝ : CharP α p<VAR>hp : Fact (Nat.Prime p)<VAR>this : Algebra (ZMod p) α := ZMod.algebra α p<VAR>b : Basis { x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) α } (ZMod p) α := IsNoetherian.finsetBasis (ZMod p) α<GOAL>IsPrimePow p
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Field α<VAR>p : ℕ<VAR>h✝ : CharP α p<VAR>hp : Fact (Nat.Prime p)<VAR>this : Algebra (ZMod p) α := ZMod.algebra α p<VAR>b : Basis { x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) α } (ZMod p) α := IsNoetherian.finsetBasis (ZMod p) α<GOAL>‖{ x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) α }‖ ≠ 0
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Field α<VAR>p : ℕ<VAR>h✝ : CharP α p<VAR>hp : Fact (Nat.Prime p)<VAR>this : Algebra (ZMod p) α := ZMod.algebra α p<VAR>b : Basis { x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) α } (ZMod p) α := IsNoetherian.finsetBasis (ZMod p) α<GOAL>FiniteDimensional.finrank (ZMod p) α ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>ι : Type u_5<VAR>inst✝ : Countable ι<VAR>f : α → ℝ≥0∞<VAR>s : ι → Set α<VAR>hd : Directed (fun x x_1 => x ⊆ x_1) s<GOAL>∫⁻ (x : α) in ⋃ i, s i, f x ∂μ = ⨆ i, ∫⁻ (x : α) in s i, f x ∂μ
<VAR>x✝¹ : Substring<VAR>h✝ : x✝¹.Valid<VAR>x✝ : Nat<VAR>w✝² w✝¹ w✝ : List Char<VAR>h : ValidFor w✝² w✝¹ w✝ x✝¹<GOAL>(x✝¹.take x✝).toString.data = List.take x✝ x✝¹.toString.data
<VAR>b✝ x y : ℝ<VAR>b : ℕ<VAR>r : ℝ<VAR>hb : 1 < b<VAR>hr✝ : 0 ≤ r<VAR>hr : 0 < r<GOAL>⌊logb (↑b) r⌋ = Int.log b r
<VAR>b✝ x y : ℝ<VAR>b : ℕ<VAR>r : ℝ<VAR>hb : 1 < b<VAR>hr✝ : 0 ≤ r<VAR>hr : 0 < r<VAR>hb1' : 1 < ↑b<GOAL>⌊logb (↑b) r⌋ = Int.log b r
<VAR>b✝ x y : ℝ<VAR>b : ℕ<VAR>r : ℝ<VAR>hb : 1 < b<VAR>hr✝ : 0 ≤ r<VAR>hr : 0 < r<VAR>hb1' : 1 < ↑b<GOAL>⌊logb (↑b) r⌋ ≤ Int.log b r
<VAR>b✝ x y : ℝ<VAR>b : ℕ<VAR>r : ℝ<VAR>hb : 1 < b<VAR>hr✝ : 0 ≤ r<VAR>hr : 0 < r<VAR>hb1' : 1 < ↑b<GOAL>Int.log b r ≤ ⌊logb (↑b) r⌋
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Fintype F<VAR>inst✝ : DecidableEq F<VAR>hF : ringChar F ≠ 2<GOAL>quadraticChar F ≠ 1
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Fintype F<VAR>inst✝ : DecidableEq F<VAR>hF : ringChar F ≠ 2<VAR>a : Fˣ<VAR>ha : (quadraticChar F) ↑a = -1<GOAL>quadraticChar F ≠ 1
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Fintype F<VAR>inst✝ : DecidableEq F<VAR>hF : ringChar F ≠ 2<VAR>a : Fˣ<VAR>ha : (quadraticChar F) ↑a = -1<VAR>hχ : quadraticChar F = 1<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>k : ℕ<GOAL>multiplicity a b < ↑k ↔ ¬a ^ k ∣ b
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>rpos : 0 < r<VAR>f : E → E := fun y => x + (r * ‖y‖⁻¹) • y<GOAL>IsPathConnected (sphere x r)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>rpos : 0 < r<VAR>f : E → E := fun y => x + (r * ‖y‖⁻¹) • y<VAR>A : ContinuousOn f {0}ᶜ<GOAL>IsPathConnected (sphere x r)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>rpos : 0 < r<VAR>f : E → E := fun y => x + (r * ‖y‖⁻¹) • y<VAR>A : ContinuousOn f {0}ᶜ<VAR>B : IsPathConnected {0}ᶜ<GOAL>IsPathConnected (sphere x r)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>rpos : 0 < r<VAR>f : E → E := fun y => x + (r * ‖y‖⁻¹) • y<VAR>A : ContinuousOn f {0}ᶜ<VAR>B : IsPathConnected {0}ᶜ<VAR>C : IsPathConnected (f '' {0}ᶜ)<GOAL>IsPathConnected (sphere x r)
<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>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ s t u : Set α<VAR>hs : MeasurableSet s<VAR>h : μ t = μ u<VAR>htu : t ⊆ u<VAR>ht_ne_top : μ u ≠ ⊤<GOAL>μ (t ∩ s) = μ (u ∩ s)
<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>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ s t u : Set α<VAR>hs : MeasurableSet s<VAR>h : μ t = μ u<VAR>htu : t ⊆ u<VAR>ht_ne_top : μ u ≠ ⊤<GOAL>μ (u ∩ s) ≤ μ (t ∩ s)
<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>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ s t u : Set α<VAR>hs : MeasurableSet s<VAR>h : μ t = μ u<VAR>htu : t ⊆ u<VAR>ht_ne_top : μ u ≠ ⊤<VAR>A : μ (u ∩ s) + μ (u \ s) ≤ μ (t ∩ s) + μ (u \ s)<GOAL>μ (u ∩ s) ≤ μ (t ∩ s)
<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>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ s t u : Set α<VAR>hs : MeasurableSet s<VAR>h : μ t = μ u<VAR>htu : t ⊆ u<VAR>ht_ne_top : μ u ≠ ⊤<VAR>A : μ (u ∩ s) + μ (u \ s) ≤ μ (t ∩ s) + μ (u \ s)<VAR>B : μ (u \ s) ≠ ⊤<GOAL>μ (u ∩ s) ≤ μ (t ∩ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : Memℒp f 1 μ<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ M, 0 ≤ M ∧ ∫⁻ (x : α), ↑‖{x | M ≤ ↑‖f x‖₊}.indicator f x‖₊ ∂μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : Memℒp f 1 μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hf_mk : Memℒp (AEStronglyMeasurable.mk f ⋯) 1 μ<GOAL>∃ M, 0 ≤ M ∧ ∫⁻ (x : α), ↑‖{x | M ≤ ↑‖f x‖₊}.indicator f x‖₊ ∂μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : Memℒp f 1 μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hf_mk : Memℒp (AEStronglyMeasurable.mk f ⋯) 1 μ<VAR>M : ℝ<VAR>hM_pos : 0 ≤ M<VAR>hfM : ∫⁻ (x : α), ↑‖{x | M ≤ ↑‖AEStronglyMeasurable.mk f ⋯ x‖₊}.indicator (AEStronglyMeasurable.mk f ⋯) x‖₊ ∂μ ≤ ENNReal.ofReal ε<GOAL>∃ M, 0 ≤ M ∧ ∫⁻ (x : α), ↑‖{x | M ≤ ↑‖f x‖₊}.indicator f x‖₊ ∂μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : Memℒp f 1 μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hf_mk : Memℒp (AEStronglyMeasurable.mk f ⋯) 1 μ<VAR>M : ℝ<VAR>hM_pos : 0 ≤ M<VAR>hfM : ∫⁻ (x : α), ↑‖{x | M ≤ ↑‖AEStronglyMeasurable.mk f ⋯ x‖₊}.indicator (AEStronglyMeasurable.mk f ⋯) x‖₊ ∂μ ≤ ENNReal.ofReal ε<GOAL>∫⁻ (x : α), ↑‖{x | M ≤ ↑‖f x‖₊}.indicator f x‖₊ ∂μ = ∫⁻ (x : α), ↑‖{x | M ≤ ↑‖AEStronglyMeasurable.mk f ⋯ x‖₊}.indicator (AEStronglyMeasurable.mk f ⋯) x‖₊ ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : Memℒp f 1 μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hf_mk : Memℒp (AEStronglyMeasurable.mk f ⋯) 1 μ<VAR>M : ℝ<VAR>hM_pos : 0 ≤ M<VAR>hfM : ∫⁻ (x : α), ↑‖{x | M ≤ ↑‖AEStronglyMeasurable.mk f ⋯ x‖₊}.indicator (AEStronglyMeasurable.mk f ⋯) x‖₊ ∂μ ≤ ENNReal.ofReal ε<GOAL>(fun x => ↑‖{x | M ≤ ↑‖f x‖₊}.indicator f x‖₊) =ᶠ[ae μ] fun x => ↑‖{x | M ≤ ↑‖AEStronglyMeasurable.mk f ⋯ x‖₊}.indicator (AEStronglyMeasurable.mk f ⋯) x‖₊
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : Memℒp f 1 μ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hf_mk : Memℒp (AEStronglyMeasurable.mk f ⋯) 1 μ<VAR>M : ℝ<VAR>hM_pos : 0 ≤ M<VAR>hfM : ∫⁻ (x : α), ↑‖{x | M ≤ ↑‖AEStronglyMeasurable.mk f ⋯ x‖₊}.indicator (AEStronglyMeasurable.mk f ⋯) x‖₊ ∂μ ≤ ENNReal.ofReal ε<VAR>x : α<VAR>hx : f x = AEStronglyMeasurable.mk f ⋯ x<GOAL>↑‖{x | M ≤ ↑‖f x‖₊}.indicator f x‖₊ = ↑‖{x | M ≤ ↑‖AEStronglyMeasurable.mk f ⋯ x‖₊}.indicator (AEStronglyMeasurable.mk f ⋯) x‖₊
<VAR>x : ℝ<GOAL>cosh x ≤ rexp (x ^ 2 / 2)
<VAR>x : ℝ<GOAL>∑' (n : ℕ), x ^ (2 * n) / ↑(2 * n)! ≤ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) (x ^ 2 / 2)
<VAR>x : ℝ<VAR>i : ℕ<GOAL>x ^ (2 * i) / ↑(2 * i)! ≤ (↑i !)⁻¹ • (x ^ 2 / 2) ^ i
<VAR>x : ℝ<VAR>i : ℕ<GOAL>(x ^ 2) ^ i / ↑(2 * i)! ≤ (x ^ 2) ^ i / (2 ^ i * ↑i !)
<VAR>x : ℝ<VAR>i : ℕ<GOAL>2 ^ i * i ! ≤ (2 * i)!
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>s I : Set (AddCircle T)<VAR>u x : AddCircle T<VAR>hu : IsOfFinAddOrder u<VAR>hs : u +ᵥ s =ᶠ[ae volume] s<VAR>hI : I =ᶠ[ae volume] ball x (T / (2 * ↑(addOrderOf u)))<VAR>G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u<GOAL>volume s = addOrderOf u • volume (s ∩ I)
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>s I : Set (AddCircle T)<VAR>u x : AddCircle T<VAR>hu : IsOfFinAddOrder u<VAR>hs : u +ᵥ s =ᶠ[ae volume] s<VAR>hI : I =ᶠ[ae volume] ball x (T / (2 * ↑(addOrderOf u)))<VAR>G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u<VAR>this : Fintype ↥G<GOAL>volume s = addOrderOf u • volume (s ∩ I)
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>s I : Set (AddCircle T)<VAR>u x : AddCircle T<VAR>hu : IsOfFinAddOrder u<VAR>hs : u +ᵥ s =ᶠ[ae volume] s<VAR>hI : I =ᶠ[ae volume] ball x (T / (2 * ↑(addOrderOf u)))<VAR>G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u<VAR>this : Fintype ↥G<VAR>hsG : ∀ (g : ↥G), g +ᵥ s =ᶠ[ae volume] s<GOAL>volume s = addOrderOf u • volume (s ∩ I)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f : α → E<VAR>p q : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : AEStronglyMeasurable f μ<VAR>hfq_lt_top : eLpNorm' f q μ < ⊤<VAR>hp_nonneg : 0 ≤ p<VAR>hpq : p ≤ q<GOAL>eLpNorm' f p μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f : α → E<VAR>p q : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : AEStronglyMeasurable f μ<VAR>hfq_lt_top : eLpNorm' f q μ < ⊤<VAR>hp_nonneg : 0 ≤ p<VAR>hpq : p ≤ q<VAR>hp_nonpos : p ≤ 0<GOAL>eLpNorm' f p μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f : α → E<VAR>p q : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : AEStronglyMeasurable f μ<VAR>hfq_lt_top : eLpNorm' f q μ < ⊤<VAR>hp_nonneg : 0 ≤ p<VAR>hpq : p ≤ q<VAR>hp_pos : 0 < p<GOAL>eLpNorm' f p μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f : α → E<VAR>p q : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : AEStronglyMeasurable f μ<VAR>hfq_lt_top : eLpNorm' f q μ < ⊤<VAR>hp_nonneg : 0 ≤ p<VAR>hpq : p ≤ q<VAR>hp_pos : 0 < p<VAR>hq_pos : 0 < q<GOAL>eLpNorm' f p μ < ⊤
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>y : ℝ<VAR>hv : ¬v = 0<VAR>e : ℝ ≃ᵐ ℝ := (Homeomorph.addRight y).symm.toMeasurableEquiv<GOAL>Measure.map (fun x => x + y) (gaussianReal μ v) = gaussianReal (μ + y) v
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>y : ℝ<VAR>hv : ¬v = 0<VAR>e : ℝ ≃ᵐ ℝ := (Homeomorph.addRight y).symm.toMeasurableEquiv<VAR>he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => 1) x) x<GOAL>Measure.map (fun x => x + y) (gaussianReal μ v) = gaussianReal (μ + y) v
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>y : ℝ<VAR>hv : ¬v = 0<VAR>e : ℝ ≃ᵐ ℝ := (Homeomorph.addRight y).symm.toMeasurableEquiv<VAR>he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => 1) x) x<VAR>s' : Set ℝ<VAR>hs' : MeasurableSet s'<GOAL>(Measure.map (⇑e.symm) (gaussianReal μ v)) s' = (gaussianReal (μ + y) v) s'
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>y : ℝ<VAR>hv : ¬v = 0<VAR>e : ℝ ≃ᵐ ℝ := (Homeomorph.addRight y).symm.toMeasurableEquiv<VAR>he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => 1) x) x<VAR>s' : Set ℝ<VAR>hs' : MeasurableSet s'<GOAL>ENNReal.ofReal (∫ (x : ℝ) in s', |1| * gaussianPDFReal μ v (e x)) = (gaussianReal (μ + y) v) s'
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>y : ℝ<VAR>hv : ¬v = 0<VAR>e : ℝ ≃ᵐ ℝ := (Homeomorph.addRight y).symm.toMeasurableEquiv<VAR>he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => 1) x) x<VAR>s' : Set ℝ<VAR>hs' : MeasurableSet s'<GOAL>ENNReal.ofReal (∫ (x : ℝ) in s', gaussianPDFReal μ v (e x)) = (gaussianReal (μ + y) v) s'
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>y : ℝ<VAR>hv : ¬v = 0<VAR>e : ℝ ≃ᵐ ℝ := (Homeomorph.addRight y).symm.toMeasurableEquiv<VAR>he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => 1) x) x<VAR>s' : Set ℝ<VAR>hs' : MeasurableSet s'<GOAL>ENNReal.ofReal (∫ (x : ℝ) in s', gaussianPDFReal μ v (e x)) = ENNReal.ofReal (∫ (x : ℝ) in s', gaussianPDFReal (μ + y) v x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>a✝ b✝ : R<VAR>s : S<VAR>inst✝⁶ : MonoidWithZero R<VAR>inst✝⁵ : MonoidWithZero S<VAR>inst✝⁴ : Zero M<VAR>inst✝³ : MulActionWithZero R M<VAR>inst✝² : MulActionWithZero R S<VAR>inst✝¹ : MulActionWithZero S M<VAR>inst✝ : IsScalarTower R S M<VAR>h : IsSMulRegular M 0<VAR>a b : M<GOAL>(fun x => 0 • x) a = (fun x => 0 • x) b
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>a✝ b✝ : R<VAR>s : S<VAR>inst✝⁶ : MonoidWithZero R<VAR>inst✝⁵ : MonoidWithZero S<VAR>inst✝⁴ : Zero M<VAR>inst✝³ : MulActionWithZero R M<VAR>inst✝² : MulActionWithZero R S<VAR>inst✝¹ : MulActionWithZero S M<VAR>inst✝ : IsScalarTower R S M<VAR>h : IsSMulRegular M 0<VAR>a b : M<GOAL>0 • a = 0 • b
<VAR>α β : Type u<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>1 ≤ ↑n
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n + a = n'<GOAL>(leftShiftAddEquiv K L n a n' hn') 0 = 0
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>A F : Cᵒᵖ ⥤ Type v<VAR>η : F ⟶ A<VAR>X : C<GOAL>unitBackward η X ∘ unitForward η X = id
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>A F : Cᵒᵖ ⥤ Type v<VAR>η : F ⟶ A<VAR>X : C<VAR>p : YonedaCollection (restrictedYonedaObj η) X<GOAL>((unitBackward η X ∘ unitForward η X) p).fst = (id p).fst
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>A F : Cᵒᵖ ⥤ Type v<VAR>η : F ⟶ A<VAR>X : C<VAR>p : YonedaCollection (restrictedYonedaObj η) X<GOAL>OverArrows.val ((restrictedYonedaObj η).map (eqToHom ⋯) (id p).snd) = OverArrows.val ((unitBackward η X ∘ unitForward η X) p).snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>ι'✝ : Type u_5<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>ι : Type u_6<VAR>ι' : Type u_7<VAR>f : ι → α<VAR>v : Filter ι<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>hv : v.HasBasis p s<GOAL>liminf f v = sSup (⋃ j, ⋂ i, Iic (f ↑i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>ι'✝ : Type u_5<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>ι : Type u_6<VAR>ι' : Type u_7<VAR>f : ι → α<VAR>v : Filter ι<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>hv : v.HasBasis p s<GOAL>sSup {a | ∃ i, p i ∧ ∀ ⦃x : ι⦄, x ∈ s i → a ≤ f x} = sSup (⋃ j, ⋂ i, Iic (f ↑i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>ι'✝ : Type u_5<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>ι : Type u_6<VAR>ι' : Type u_7<VAR>f : ι → α<VAR>v : Filter ι<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>hv : v.HasBasis p s<VAR>x : α<GOAL>x ∈ {a | ∃ i, p i ∧ ∀ ⦃x : ι⦄, x ∈ s i → a ≤ f x} ↔ x ∈ ⋃ j, ⋂ i, Iic (f ↑i)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>n : ℕ<GOAL>‖cauchyPowerSeries f c R n‖ = (2 * π)⁻¹ * ‖∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z‖
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>n : ℕ<GOAL>0 ≤ (2 * π)⁻¹
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>n : ℕ<GOAL>(2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖deriv (circleMap c R) θ • (circleMap c R θ - c)⁻¹ ^ n • (circleMap c R θ - c)⁻¹ • f (circleMap c R θ)‖ = (2 * π)⁻¹ * (|R|⁻¹ ^ n * (|R| * (|R|⁻¹ * ∫ (x : ℝ) in 0 ..2 * π, ‖f (circleMap c R x)‖)))
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>n : ℕ<GOAL>(2 * π)⁻¹ * (|R|⁻¹ ^ n * (|R| * (|R|⁻¹ * ∫ (x : ℝ) in 0 ..2 * π, ‖f (circleMap c R x)‖))) ≤ ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c R θ)‖) * |R|⁻¹ ^ n
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>n : ℕ<GOAL>(2 * π)⁻¹ * (|0|⁻¹ ^ n * (|0| * (|0|⁻¹ * ∫ (x : ℝ) in 0 ..2 * π, ‖f (circleMap c 0 x)‖))) ≤ ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c 0 θ)‖) * |0|⁻¹ ^ n
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>n : ℕ<VAR>hR : R ≠ 0<GOAL>(2 * π)⁻¹ * (|R|⁻¹ ^ n * (|R| * (|R|⁻¹ * ∫ (x : ℝ) in 0 ..2 * π, ‖f (circleMap c R x)‖))) ≤ ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * π, ‖f (circleMap c R θ)‖) * |R|⁻¹ ^ n
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq p<VAR>inst✝ : CommRing R<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>hM : M (inr ()) (inr ()) ≠ 0<VAR>i : Fin r<GOAL>(M * (listTransvecRow M).prod) (inr ()) (inl i) = 0
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq p<VAR>inst✝ : CommRing R<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>hM : M (inr ()) (inr ()) ≠ 0<VAR>i : Fin r<GOAL>∀ k ≤ r, (M * (List.take k (listTransvecRow M)).prod) (inr ()) (inl i) = if k ≤ ↑i then M (inr ()) (inl i) else 0
<VAR>𝕜 : Type u_1<VAR>X : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : PseudoEMetricSpace X<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : X → X<VAR>g l : X → E<VAR>hf : LipschitzWith 1 f<VAR>hg : UniformContinuous g<GOAL>UniformEquicontinuous (birkhoffAverage 𝕜 f g)
<VAR>𝕜 : Type u_1<VAR>X : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : PseudoEMetricSpace X<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : X → X<VAR>g l : X → E<VAR>hf : LipschitzWith 1 f<VAR>hg : UniformContinuous g<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∀ᶠ (xy : X × X) in 𝓤 X, ∀ (i : ℕ), (birkhoffAverage 𝕜 f g i xy.1, birkhoffAverage 𝕜 f g i xy.2) ∈ {p | dist p.1 p.2 ≤ ε}
<VAR>𝕜 : Type u_1<VAR>X : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : PseudoEMetricSpace X<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : X → X<VAR>g l : X → E<VAR>hf : LipschitzWith 1 f<VAR>hg : UniformContinuous g<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>δ : ℝ≥0∞<VAR>hδ₀ : 0 < δ<VAR>hδε : ∀ (x y : X), (x, y) ∈ {p | edist p.1 p.2 ≤ δ} → (g x, g y) ∈ {p | dist p.1 p.2 ≤ ε}<GOAL>∀ᶠ (xy : X × X) in 𝓤 X, ∀ (i : ℕ), (birkhoffAverage 𝕜 f g i xy.1, birkhoffAverage 𝕜 f g i xy.2) ∈ {p | dist p.1 p.2 ≤ ε}
<VAR>𝕜 : Type u_1<VAR>X : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : PseudoEMetricSpace X<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : X → X<VAR>g l : X → E<VAR>hf : LipschitzWith 1 f<VAR>hg : UniformContinuous g<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>δ : ℝ≥0∞<VAR>hδ₀ : 0 < δ<VAR>hδε : ∀ (x y : X), (x, y) ∈ {p | edist p.1 p.2 ≤ δ} → (g x, g y) ∈ {p | dist p.1 p.2 ≤ ε}<VAR>x y : X<VAR>h : edist x y < δ<VAR>n : ℕ<GOAL>(birkhoffAverage 𝕜 f g n (x, y).1, birkhoffAverage 𝕜 f g n (x, y).2) ∈ {p | dist p.1 p.2 ≤ ε}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β<VAR>s : Set (Set β)<GOAL>f ⁻¹' ⋃₀ s = ⋃ t ∈ s, f ⁻¹' t
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>x : ℝ<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hx : ∀ i ∈ s, w i ≠ 0 → z i = x<GOAL>∑ i ∈ s, w i * z i = ∑ i ∈ s, w i * x
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>x : ℝ<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hx : ∀ i ∈ s, w i ≠ 0 → z i = x<VAR>i : ι<VAR>hi : i ∈ s<GOAL>w i * z i = w i * x
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>x : ℝ<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hx : ∀ i ∈ s, w i ≠ 0 → z i = x<VAR>i : ι<VAR>hi : i ∈ s<VAR>hwi : w i = 0<GOAL>w i * z i = w i * x
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>x : ℝ<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hx : ∀ i ∈ s, w i ≠ 0 → z i = x<VAR>i : ι<VAR>hi : i ∈ s<VAR>hwi : w i ≠ 0<GOAL>w i * z i = w i * x
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>x : ℝ<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hx : ∀ i ∈ s, w i ≠ 0 → z i = x<GOAL>∑ i ∈ s, w i * x = x
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : HasPullbacks C<VAR>A : C<VAR>X✝ Y✝ : MonoOver A<VAR>k : X✝ ⟶ Y✝<VAR>g : MonoOver A<GOAL>pullback.lift (pullback.fst g.arrow X✝.arrow) (pullback.snd g.arrow X✝.arrow ≫ k.left) ⋯ ≫ pullback.snd g.arrow Y✝.arrow ≫ Y✝.arrow = pullback.snd g.arrow X✝.arrow ≫ X✝.arrow
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type ?u.18537<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsNoetherianRing R<VAR>s : Finset M<VAR>hs : Submodule.span R ↑s = ⊤<GOAL>FinitePresentation R M
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>inst✝¹ : BorelSpace E<VAR>f : β → E<VAR>μ : Measure β<VAR>fmeas : Measurable f<VAR>hf : Memℒp f p μ<VAR>s : Set E<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>hi₀ : Memℒp (fun x => y₀) p μ<VAR>n : ℕ<GOAL>Memℒp (↑(approxOn f fmeas s y₀ h₀ n)) p μ