ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>s : Set (ι → ℝ)<VAR>hs : MeasurableSet s<VAR>I : Box ι<VAR>y : E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>A : μ (s ∩ Box.Icc I) ≠ ⊤<VAR>B : μ (s ∩ ↑I) ≠ ⊤<VAR>F : Set (ι → ℝ)<VAR>hFs : F ⊆ s ∩ Box.Icc I<VAR>hFc : IsClosed F<VAR>hμF : μ ((s ∩ Box.Icc I) \ F) < ↑ε<VAR>U : Set (ι → ℝ)<VAR>hsU : s ∩ Box.Icc I ⊆ U<VAR>hUo : IsOpen U<VAR>hUt : μ U < ⊤<VAR>hμU : μ (U \ (s ∩ Box.Icc I)) < ↑ε<VAR>rs : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrsU : ∀ x ∈ s ∩ Box.Icc I, closedBall x ↑(rs x) ⊆ U<VAR>rs' : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrs'F : ∀ x ∈ Box.Icc I \ s, closedBall x ↑(rs' x) ⊆ Fᶜ<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0) := s.piecewise rs rs'<GOAL>∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum (s.indicator fun x => y) μ.toBoxAdditive.toSMul π) ((μ (s ∩ ↑I)).toReal • y) ≤ ‖y‖ * ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>s : Set (ι → ℝ)<VAR>hs : MeasurableSet s<VAR>I : Box ι<VAR>y : E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>A : μ (s ∩ Box.Icc I) ≠ ⊤<VAR>B : μ (s ∩ ↑I) ≠ ⊤<VAR>F : Set (ι → ℝ)<VAR>hFs : F ⊆ s ∩ Box.Icc I<VAR>hFc : IsClosed F<VAR>hμF : μ ((s ∩ Box.Icc I) \ F) < ↑ε<VAR>U : Set (ι → ℝ)<VAR>hsU : s ∩ Box.Icc I ⊆ U<VAR>hUo : IsOpen U<VAR>hUt : μ U < ⊤<VAR>hμU : μ (U \ (s ∩ Box.Icc I)) < ↑ε<VAR>rs : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrsU : ∀ x ∈ s ∩ Box.Icc I, closedBall x ↑(rs x) ⊆ U<VAR>rs' : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrs'F : ∀ x ∈ Box.Icc I \ s, closedBall x ↑(rs' x) ⊆ Fᶜ<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0) := s.piecewise rs rs'<VAR>c : ℝ≥0<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c ((fun x => r) c) π<VAR>hπp : π.IsPartition<GOAL>dist (integralSum (s.indicator fun x => y) μ.toBoxAdditive.toSMul π) ((μ (s ∩ ↑I)).toReal • y) ≤ ‖y‖ * ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>s : Set (ι → ℝ)<VAR>hs : MeasurableSet s<VAR>I : Box ι<VAR>y : E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>A : μ (s ∩ Box.Icc I) ≠ ⊤<VAR>B : μ (s ∩ ↑I) ≠ ⊤<VAR>F : Set (ι → ℝ)<VAR>hFs : F ⊆ s ∩ Box.Icc I<VAR>hFc : IsClosed F<VAR>hμF : μ ((s ∩ Box.Icc I) \ F) < ↑ε<VAR>U : Set (ι → ℝ)<VAR>hsU : s ∩ Box.Icc I ⊆ U<VAR>hUo : IsOpen U<VAR>hUt : μ U < ⊤<VAR>hμU : μ (U \ (s ∩ Box.Icc I)) < ↑ε<VAR>rs : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrsU : ∀ x ∈ s ∩ Box.Icc I, closedBall x ↑(rs x) ⊆ U<VAR>rs' : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrs'F : ∀ x ∈ Box.Icc I \ s, closedBall x ↑(rs' x) ⊆ Fᶜ<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0) := s.piecewise rs rs'<VAR>c : ℝ≥0<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c ((fun x => r) c) π<VAR>hπp : π.IsPartition<GOAL>dist (integralSum (s.indicator fun x => y) μ.toBoxAdditive.toSMul π) ((μ (s ∩ ↑I)).toReal • y) ≤ ↑ε * ‖y‖
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>s : Set (ι → ℝ)<VAR>hs : MeasurableSet s<VAR>I : Box ι<VAR>y : E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>A : μ (s ∩ Box.Icc I) ≠ ⊤<VAR>B : μ (s ∩ ↑I) ≠ ⊤<VAR>F : Set (ι → ℝ)<VAR>hFs : F ⊆ s ∩ Box.Icc I<VAR>hFc : IsClosed F<VAR>hμF : μ ((s ∩ Box.Icc I) \ F) < ↑ε<VAR>U : Set (ι → ℝ)<VAR>hsU : s ∩ Box.Icc I ⊆ U<VAR>hUo : IsOpen U<VAR>hUt : μ U < ⊤<VAR>hμU : μ (U \ (s ∩ Box.Icc I)) < ↑ε<VAR>rs : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrsU : ∀ x ∈ s ∩ Box.Icc I, closedBall x ↑(rs x) ⊆ U<VAR>rs' : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrs'F : ∀ x ∈ Box.Icc I \ s, closedBall x ↑(rs' x) ⊆ Fᶜ<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0) := s.piecewise rs rs'<VAR>c : ℝ≥0<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c ((fun x => r) c) π<VAR>hπp : π.IsPartition<GOAL>dist (∑ J ∈ π.boxes, (μ ↑J).toReal • s.indicator (fun x => y) (π.tag J)) ((μ (s ∩ ↑I)).toReal • y) ≤ ↑ε * ‖y‖
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>s : Set (ι → ℝ)<VAR>hs : MeasurableSet s<VAR>I : Box ι<VAR>y : E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>A : μ (s ∩ Box.Icc I) ≠ ⊤<VAR>B : μ (s ∩ ↑I) ≠ ⊤<VAR>F : Set (ι → ℝ)<VAR>hFs : F ⊆ s ∩ Box.Icc I<VAR>hFc : IsClosed F<VAR>hμF : μ ((s ∩ Box.Icc I) \ F) < ↑ε<VAR>U : Set (ι → ℝ)<VAR>hsU : s ∩ Box.Icc I ⊆ U<VAR>hUo : IsOpen U<VAR>hUt : μ U < ⊤<VAR>hμU : μ (U \ (s ∩ Box.Icc I)) < ↑ε<VAR>rs : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrsU : ∀ x ∈ s ∩ Box.Icc I, closedBall x ↑(rs x) ⊆ U<VAR>rs' : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrs'F : ∀ x ∈ Box.Icc I \ s, closedBall x ↑(rs' x) ⊆ Fᶜ<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0) := s.piecewise rs rs'<VAR>c : ℝ≥0<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c ((fun x => r) c) π<VAR>hπp : π.IsPartition<GOAL>|(μ (π.filter fun i => π.tag i ∈ s).iUnion).toReal - (μ (s ∩ ↑I)).toReal| * ‖y‖ ≤ ↑ε * ‖y‖
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>s : Set (ι → ℝ)<VAR>hs : MeasurableSet s<VAR>I : Box ι<VAR>y : E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>A : μ (s ∩ Box.Icc I) ≠ ⊤<VAR>B : μ (s ∩ ↑I) ≠ ⊤<VAR>F : Set (ι → ℝ)<VAR>hFs : F ⊆ s ∩ Box.Icc I<VAR>hFc : IsClosed F<VAR>hμF : μ ((s ∩ Box.Icc I) \ F) < ↑ε<VAR>U : Set (ι → ℝ)<VAR>hsU : s ∩ Box.Icc I ⊆ U<VAR>hUo : IsOpen U<VAR>hUt : μ U < ⊤<VAR>hμU : μ (U \ (s ∩ Box.Icc I)) < ↑ε<VAR>rs : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrsU : ∀ x ∈ s ∩ Box.Icc I, closedBall x ↑(rs x) ⊆ U<VAR>rs' : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrs'F : ∀ x ∈ Box.Icc I \ s, closedBall x ↑(rs' x) ⊆ Fᶜ<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0) := s.piecewise rs rs'<VAR>c : ℝ≥0<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c ((fun x => r) c) π<VAR>hπp : π.IsPartition<VAR>t : Set (ι → ℝ) := (π.filter fun x => π.tag x ∈ s).iUnion<GOAL>|(μ t).toReal - (μ (s ∩ ↑I)).toReal| ≤ ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>s : Set (ι → ℝ)<VAR>hs : MeasurableSet s<VAR>I : Box ι<VAR>y : E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>A : μ (s ∩ Box.Icc I) ≠ ⊤<VAR>B : μ (s ∩ ↑I) ≠ ⊤<VAR>F : Set (ι → ℝ)<VAR>hFs : F ⊆ s ∩ Box.Icc I<VAR>hFc : IsClosed F<VAR>hμF : μ ((s ∩ Box.Icc I) \ F) < ↑ε<VAR>U : Set (ι → ℝ)<VAR>hsU : s ∩ Box.Icc I ⊆ U<VAR>hUo : IsOpen U<VAR>hUt : μ U < ⊤<VAR>hμU : μ (U \ (s ∩ Box.Icc I)) < ↑ε<VAR>rs : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrsU : ∀ x ∈ s ∩ Box.Icc I, closedBall x ↑(rs x) ⊆ U<VAR>rs' : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrs'F : ∀ x ∈ Box.Icc I \ s, closedBall x ↑(rs' x) ⊆ Fᶜ<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0) := s.piecewise rs rs'<VAR>c : ℝ≥0<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c ((fun x => r) c) π<VAR>hπp : π.IsPartition<VAR>t : Set (ι → ℝ) := (π.filter fun x => π.tag x ∈ s).iUnion<VAR>htU : t ⊆ U ∩ ↑I<GOAL>|(μ t).toReal - (μ (s ∩ ↑I)).toReal| ≤ ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>s : Set (ι → ℝ)<VAR>hs : MeasurableSet s<VAR>I : Box ι<VAR>y : E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>A : μ (s ∩ Box.Icc I) ≠ ⊤<VAR>B : μ (s ∩ ↑I) ≠ ⊤<VAR>F : Set (ι → ℝ)<VAR>hFs : F ⊆ s ∩ Box.Icc I<VAR>hFc : IsClosed F<VAR>hμF : μ ((s ∩ Box.Icc I) \ F) < ↑ε<VAR>U : Set (ι → ℝ)<VAR>hsU : s ∩ Box.Icc I ⊆ U<VAR>hUo : IsOpen U<VAR>hUt : μ U < ⊤<VAR>hμU : μ (U \ (s ∩ Box.Icc I)) < ↑ε<VAR>rs : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrsU : ∀ x ∈ s ∩ Box.Icc I, closedBall x ↑(rs x) ⊆ U<VAR>rs' : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrs'F : ∀ x ∈ Box.Icc I \ s, closedBall x ↑(rs' x) ⊆ Fᶜ<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0) := s.piecewise rs rs'<VAR>c : ℝ≥0<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c ((fun x => r) c) π<VAR>hπp : π.IsPartition<VAR>t : Set (ι → ℝ) := (π.filter fun x => π.tag x ∈ s).iUnion<VAR>htU : t ⊆ U ∩ ↑I<GOAL>(μ t).toReal - (μ (s ∩ ↑I)).toReal ≤ ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>s : Set (ι → ℝ)<VAR>hs : MeasurableSet s<VAR>I : Box ι<VAR>y : E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>A : μ (s ∩ Box.Icc I) ≠ ⊤<VAR>B : μ (s ∩ ↑I) ≠ ⊤<VAR>F : Set (ι → ℝ)<VAR>hFs : F ⊆ s ∩ Box.Icc I<VAR>hFc : IsClosed F<VAR>hμF : μ ((s ∩ Box.Icc I) \ F) < ↑ε<VAR>U : Set (ι → ℝ)<VAR>hsU : s ∩ Box.Icc I ⊆ U<VAR>hUo : IsOpen U<VAR>hUt : μ U < ⊤<VAR>hμU : μ (U \ (s ∩ Box.Icc I)) < ↑ε<VAR>rs : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrsU : ∀ x ∈ s ∩ Box.Icc I, closedBall x ↑(rs x) ⊆ U<VAR>rs' : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrs'F : ∀ x ∈ Box.Icc I \ s, closedBall x ↑(rs' x) ⊆ Fᶜ<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0) := s.piecewise rs rs'<VAR>c : ℝ≥0<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c ((fun x => r) c) π<VAR>hπp : π.IsPartition<VAR>t : Set (ι → ℝ) := (π.filter fun x => π.tag x ∈ s).iUnion<VAR>htU : t ⊆ U ∩ ↑I<GOAL>(μ (s ∩ ↑I)).toReal - (μ t).toReal ≤ ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r✝ : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>u : δ → δ → Prop<VAR>r : α → α → Prop<VAR>b : β<VAR>h : ¬s b b<GOAL>∀ {a b_1 : α}, Prod.Lex r s ({ toFun := fun a => (a, b), inj' := ⋯ } a) ({ toFun := fun a => (a, b), inj' := ⋯ } b_1) ↔ r a b_1
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>hf₁ : f.ker = ⊥<VAR>hf₂ : N₂ ≤ f.range<GOAL>comap f ⁅I, N₂⁆ = ⁅I, comap f N₂⁆
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>hf₁ : f.ker = ⊥<VAR>hf₂ : N₂ ≤ f.range<GOAL>comap f ⁅I, map f (comap f N₂)⁆ = ⁅I, comap f N₂⁆
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s : Set α<VAR>h : s.Finite<VAR>val✝ : Fintype ↑s<GOAL>∃ s', ↑s' = s
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedAddCommGroup E''<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x✝ x' : G<VAR>y y' : E<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>inst✝² : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹ : AddGroup G<VAR>inst✝ : TopologicalSpace G<VAR>hcg : HasCompactSupport g<VAR>hg : Continuous g<VAR>x t : G<VAR>s u : Set G<VAR>hx : x ∈ s<VAR>hu : -tsupport g + s ⊆ u<GOAL>‖(L (f t)) (g (x - t))‖ ≤ u.indicator (fun t => ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖) t
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedAddCommGroup E''<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x✝ x' : G<VAR>y y' : E<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>inst✝² : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹ : AddGroup G<VAR>inst✝ : TopologicalSpace G<VAR>hcg : HasCompactSupport g<VAR>hg : Continuous g<VAR>x t : G<VAR>s u : Set G<VAR>hx : x ∈ s<VAR>hu : -tsupport g + s ⊆ u<VAR>i : G<GOAL>‖g i‖ ≤ ⨆ i, ‖g i‖
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MulAction G α<VAR>inst✝² : MulAction G β<VAR>inst✝¹ : SMul α β<VAR>inst✝ : IsScalarTower G α β<VAR>a : α<VAR>b : β<GOAL>stabilizer G a ≤ stabilizer G (a • b)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MulAction G α<VAR>inst✝² : MulAction G β<VAR>inst✝¹ : SMul α β<VAR>inst✝ : IsScalarTower G α β<VAR>a : α<VAR>b : β<GOAL>∀ ⦃x : G⦄, x • a = a → (x • a) • b = a • b
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>v0 : R<VAR>v : Fin n → R<VAR>i✝ j✝ : Fin (n + 1)<VAR>i j : Fin n<GOAL>vandermonde (Fin.cons v0 v) i.succ j.succ = Fin.cons (fun j => v0 ^ ↑j) (fun i => Fin.cons 1 fun j => v i * vandermonde v i j) i.succ j.succ
<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>S : Type u_7<VAR>F : Filter R<VAR>inst✝² : LinearOrder R<VAR>inst✝¹ : LinearOrder S<VAR>f : R → S<VAR>f_incr : Monotone f<VAR>inst✝ : F.NeBot<VAR>cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F<GOAL>IsCoboundedUnder (fun x x_1 => x ≤ x_1) F f
<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>S : Type u_7<VAR>F : Filter R<VAR>inst✝² : LinearOrder R<VAR>inst✝¹ : LinearOrder S<VAR>f : R → S<VAR>f_incr : Monotone f<VAR>inst✝ : F.NeBot<VAR>cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F<VAR>l : R<VAR>hl : ∃ᶠ (x : R) in F, l ≤ x<GOAL>IsCoboundedUnder (fun x x_1 => x ≤ x_1) F f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : CountablyGenerated α<GOAL>Measurable (mapNatBool α)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : CountablyGenerated α<GOAL>∀ (a : ℕ), Measurable fun x => mapNatBool α x a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : CountablyGenerated α<VAR>n : ℕ<GOAL>MeasurableSet ((fun x => mapNatBool α x n) ⁻¹' {true})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : CountablyGenerated α<VAR>n : ℕ<GOAL>MeasurableSet (natGeneratingSequence α n)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f : Filter α<VAR>p q : α → Prop<GOAL>(∃ᶠ (x : α) in f, p x → q x) ↔ (∀ᶠ (x : α) in f, p x) → ∃ᶠ (x : α) in f, q x
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>‖x‖₊ = univ.sup fun w => ⟨(normAtPlace w) x, ⋯⟩
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<VAR>this : univ = image (fun w => ↑w) univ ∪ image (fun w => ↑w) univ<GOAL>‖x‖₊ = univ.sup fun w => ⟨(normAtPlace w) x, ⋯⟩
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<VAR>this : univ = image (fun w => ↑w) univ ∪ image (fun w => ↑w) univ<GOAL>max (univ.sup fun b => ‖x.1 b‖₊) (univ.sup fun b => ‖x.2 b‖₊) = max (univ.sup ((fun w => ⟨(normAtPlace w) x, ⋯⟩) ∘ fun w => ↑w)) (univ.sup ((fun w => ⟨(normAtPlace w) x, ⋯⟩) ∘ fun w => ↑w))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>hf : Continuous f<GOAL>SpecializingMap f ↔ ∀ (x : X), IsClosed (f '' closure {x})
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x✝ y z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>hf : Continuous f<VAR>h : SpecializingMap f<VAR>x : X<GOAL>IsClosed (f '' closure {x})
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x✝ y z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>hf : Continuous f<VAR>h : SpecializingMap f<VAR>x : X<GOAL>IsClosed (closure {f x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : LinearOrderedField 𝕜<VAR>t : Finset (α × β × γ)<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>x : α × β × γ<VAR>ε : 𝕜<VAR>inst✝⁶ : DecidableEq α<VAR>inst✝⁵ : DecidableEq β<VAR>inst✝⁴ : DecidableEq γ<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>inst✝¹ : Fintype γ<VAR>inst✝ : NoAccidental t<GOAL>(graph t).cliqueSet 3 = ⇑toTriangle '' ↑t
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : IsEmpty α<VAR>s : Finset α<GOAL>∏ i ∈ s, f i = 1
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝ : E<VAR>s✝ t : Set E<VAR>L L₁ L₂ : Filter E<VAR>iso : E ≃L[𝕜] F<VAR>f : G → E<VAR>s : Set G<VAR>x : G<VAR>f' : G →L[𝕜] F<GOAL>HasFDerivWithinAt (⇑iso ∘ f) f' s x ↔ HasFDerivWithinAt f ((↑iso.symm).comp f') s x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x : P<VAR>v : V<VAR>r₁ r₂ : R<VAR>hr₁ : 0 ≤ r₁<VAR>hr₂ : 0 ≤ r₂<GOAL>Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x : P<VAR>v : V<VAR>r₁ r₂ : R<VAR>hr₁ : 0 ≤ r₁<VAR>hr₂ : 0 ≤ r₂<VAR>h : r₁ ≤ r₂<GOAL>Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x : P<VAR>v : V<VAR>r₁ r₂ : R<VAR>hr₁ : 0 ≤ r₁<VAR>hr₂ : 0 ≤ r₂<VAR>h : r₂ ≤ r₁<GOAL>Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)
<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>hp0_lt : 0 < p<VAR>hpq : p ≤ q<VAR>μ : Measure α<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hf : AEStronglyMeasurable f μ<GOAL>eLpNorm' f p μ ≤ eLpNorm' f q μ
<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>hp0_lt : 0 < p<VAR>hpq : p ≤ q<VAR>μ : Measure α<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hf : AEStronglyMeasurable f μ<VAR>h_le_μ : eLpNorm' f p μ ≤ eLpNorm' f q μ * μ Set.univ ^ (1 / p - 1 / q)<GOAL>eLpNorm' f p μ ≤ eLpNorm' f q μ
<VAR>G✝ : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁴ : TopologicalSpace G✝<VAR>inst✝³ : Group G✝<VAR>inst✝² : TopologicalGroup G✝<VAR>inst✝¹ : TopologicalSpace α<VAR>f : α → G✝<VAR>s : Set α<VAR>x✝ : α<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>t t' : TopologicalSpace G<VAR>tg : TopologicalGroup G<VAR>tg' : TopologicalGroup G<VAR>h : 𝓝 1 = 𝓝 1<VAR>x : G<GOAL>𝓝 x = 𝓝 x
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(μ.withDensity 0) s = 0 s
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>a : Associates α<VAR>ha : a ≠ 0<VAR>b : Associates α<VAR>hb : b ≠ 0<VAR>p : Associates α<VAR>hp : Irreducible p<GOAL>p.count (a * b).factors = p.count a.factors + p.count b.factors
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>b : Associates α<VAR>hb : b ≠ 0<VAR>p : Associates α<VAR>hp : Irreducible p<VAR>a0 : α<VAR>nza : a0 ≠ 0<VAR>ha : Associates.mk a0 ≠ 0<GOAL>p.count (Associates.mk a0 * b).factors = p.count (Associates.mk a0).factors + p.count b.factors
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>p : Associates α<VAR>hp : Irreducible p<VAR>a0 : α<VAR>nza : a0 ≠ 0<VAR>ha : Associates.mk a0 ≠ 0<VAR>b0 : α<VAR>nzb : b0 ≠ 0<VAR>hb : Associates.mk b0 ≠ 0<GOAL>p.count (Associates.mk a0 * Associates.mk b0).factors = p.count (Associates.mk a0).factors + p.count (Associates.mk b0).factors
<VAR>α β : Type u<VAR>c : Cardinal.{u}<GOAL>lift.{v, u} c < ℵ₀ ↔ c < ℵ₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : Type u_4<VAR>A : Type u_5<VAR>B : Type u_6<VAR>inst✝¹ : DivisionMonoid G<VAR>inst✝ : MulAction G A<VAR>f : A → B<GOAL>(fun x => f (1⁻¹ • x)) = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : Type u_4<VAR>A : Type u_5<VAR>B : Type u_6<VAR>inst✝¹ : DivisionMonoid G<VAR>inst✝ : MulAction G A<VAR>x y : G<VAR>f : A → B<GOAL>(fun a => f ((x * y)⁻¹ • a)) = fun a => f (y⁻¹ • x⁻¹ • a)
<VAR>E : Type u_1<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T1Space E<VAR>s t : Set E<VAR>x : E<VAR>hx : gauge t x ≠ 0<GOAL>gauge t (gaugeRescale s t x) = gauge s x
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : NormedSpace ℝ V<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>inst✝ : SecondCountableTopology V<VAR>μ : Measure V<VAR>hf : Integrable f μ<VAR>hf' : Integrable (fun v => ‖v‖ * ‖f v‖) μ<VAR>w : W<VAR>F : W → V → E := fun w' v => 𝐞 (-(L v) w') • f v<VAR>F' : W → V → W →L[ℝ] E := fun w' v => 𝐞 (-(L v) w') • fourierSMulRight L f v<VAR>B : V → ℝ := fun v => 2 * π * ‖L‖ * ‖v‖ * ‖f v‖<GOAL>HasFDerivAt (fourierIntegral 𝐞 μ L.toLinearMap₂ f) (fourierIntegral 𝐞 μ L.toLinearMap₂ (fourierSMulRight L f) w) w
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : NormedSpace ℝ V<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>inst✝ : SecondCountableTopology V<VAR>μ : Measure V<VAR>hf : Integrable f μ<VAR>hf' : Integrable (fun v => ‖v‖ * ‖f v‖) μ<VAR>w : W<VAR>F : W → V → E := fun w' v => 𝐞 (-(L v) w') • f v<VAR>F' : W → V → W →L[ℝ] E := fun w' v => 𝐞 (-(L v) w') • fourierSMulRight L f v<VAR>B : V → ℝ := fun v => 2 * π * ‖L‖ * ‖v‖ * ‖f v‖<VAR>h0 : ∀ (w' : W), Integrable (F w') μ<GOAL>HasFDerivAt (fourierIntegral 𝐞 μ L.toLinearMap₂ f) (fourierIntegral 𝐞 μ L.toLinearMap₂ (fourierSMulRight L f) w) w