ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ inst✝ : CommSemiring R<VAR>n : ℕ<VAR>φ ψ : MvPolynomial σ R<VAR>h : ∀ d ∈ φ.support, (weight 1) d ≠ n<GOAL>(homogeneousComponent n) φ = 0
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>inst✝³ : DivisionSemiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : CharZero R<VAR>f : α → α<VAR>x : α<VAR>h : IsFixedPt f x<VAR>g : α → M<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>birkhoffAverage R f g n x = g x
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>inst✝³ : DivisionSemiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : CharZero R<VAR>f : α → α<VAR>x : α<VAR>h : IsFixedPt f x<VAR>g : α → M<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>↑n ≠ 0
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p q : R[X]<GOAL>gcd (p * q).eraseLead.content p.leadingCoeff = gcd (p.eraseLead * q).content p.leadingCoeff
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p q : R[X]<GOAL>gcd p.leadingCoeff (p * q).eraseLead.content = gcd p.leadingCoeff (p.eraseLead * q).content
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p q : R[X]<GOAL>C p.leadingCoeff ∣ (p * q).eraseLead - p.eraseLead * q
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p q : R[X]<GOAL>C p.leadingCoeff ∣ C p.leadingCoeff * (X ^ p.natDegree * q) - C p.leadingCoeff * (C q.leadingCoeff * X ^ (p * q).natDegree)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>angle (r • x) y = angle x y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>hs : NullMeasurableSet s μ<VAR>hfi : Integrable f μ<GOAL>∫ (x : X) in s, f x ∂μ + ∫ (x : X) in sᶜ, f x ∂μ = ∫ (x : X), f x ∂μ
<VAR>n m : ℕ<VAR>a : Fin (n + 1)<VAR>ha : a.castSucc ≠ 0<GOAL>a.castSucc.pred ha < a
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)<VAR>C : ℝ<VAR>H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i), ‖(f m₁) m₂‖ ≤ (C * ∏ i : ι, ‖m₁ i‖) * ∏ i : ι', ‖m₂ i‖<GOAL>‖{ toFun := fun m => (f m).mkContinuous (C * ∏ i : ι, ‖m i‖) ⋯, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous (max C 0) ⋯‖ ≤ max C 0
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End K V<VAR>μ : K<VAR>h : f.HasEigenvalue μ<GOAL>(minpoly K f).IsRoot μ
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End K V<VAR>μ : K<VAR>h : f.HasEigenvalue μ<VAR>w : V<VAR>H : w ∈ f.eigenspace μ<VAR>ne0 : w ≠ 0<GOAL>(minpoly K f).IsRoot μ
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End K V<VAR>μ : K<VAR>h : f.HasEigenvalue μ<VAR>w : V<VAR>H : w ∈ f.eigenspace μ<VAR>ne0 : w ≠ 0<GOAL>eval μ (minpoly K f) • w = 0
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<VAR>r : α ⊗ α ⟹ repeat n Prop<VAR>i : Fin2 n<VAR>x : Subtype_ r i<GOAL>(toSubtype' r ⊚ ofSubtype' r) i x = id i x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>hI : M.Indep I<VAR>f : α ↪ β<GOAL>(M.mapEmbedding f).Indep (⇑f '' I)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>f✝ g✝ : X✝ ⟶ Y✝<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>t : Fork f g<VAR>ht : IsLimit t<VAR>Z : C<VAR>k : Z ⟶ t.pt<GOAL>(k ≫ t.ι) ≫ f = (k ≫ t.ι) ≫ g
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r✝ : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>o o' : Ordinal.{u}<VAR>ho : o < type r<VAR>ho' : o' < type r<GOAL>¬r (enum r o' ho') (enum r o ho) ↔ o ≤ o'
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>A B X X' Y Y' Z : C<VAR>inst✝¹ : HasFiniteProducts C<VAR>inst✝ : Exponentiable A<VAR>I : C<VAR>t : IsInitial I<GOAL>prod.snd ≫ t.to (A ⨯ I) = 𝟙 (A ⨯ I)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>A B X X' Y Y' Z : C<VAR>inst✝¹ : HasFiniteProducts C<VAR>inst✝ : Exponentiable A<VAR>I : C<VAR>t : IsInitial I<VAR>this : prod.snd = uncurry (t.to (A ⟹ I))<GOAL>prod.snd ≫ t.to (A ⨯ I) = 𝟙 (A ⨯ I)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>A B X X' Y Y' Z : C<VAR>inst✝¹ : HasFiniteProducts C<VAR>inst✝ : Exponentiable A<VAR>I : C<VAR>t : IsInitial I<VAR>this : prod.snd = uncurry (t.to (A ⟹ I))<GOAL>t.to (A ⟹ I) ≫ (exp A).map (t.to (A ⨯ I)) = curry (𝟙 (A ⨯ I))
<VAR>α : Type u_1<VAR>inst✝³ : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝² : Ring β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>inst✝ : IsComplete β abv<VAR>f g : CauSeq β abv<GOAL>(const abv (f.lim + g.lim) - (f + g)).LimZero
<VAR>α : Type u_1<VAR>inst✝³ : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝² : Ring β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>inst✝ : IsComplete β abv<VAR>f g : CauSeq β abv<GOAL>(const abv f.lim - f + (const abv g.lim - g)).LimZero
<VAR>α : Type u_1<VAR>inst✝ : MonoidWithZero α<VAR>x y : α<VAR>nonzero : ¬(x = 0 ∧ y = 0)<VAR>H : ∀ (z : α), ¬IsUnit z → z ≠ 0 → z ∣ x → ¬z ∣ y<VAR>hx : 0 ∣ x<VAR>hy : 0 ∣ y<VAR>h : ¬IsUnit 0<GOAL>False
<VAR>n m : ℕ<VAR>h : Ico n m = []<GOAL>m - n = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>s : Set α<VAR>l : Filter α<GOAL>s =ᶠ[l] univ ↔ s ∈ l
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R✝ : ℝ<VAR>z✝ w : ℂ<VAR>R r : ℝ<VAR>hr : r < R<VAR>hr' : 0 ≤ r<VAR>z : ℂ<GOAL>∃ x, ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])), abs (circleTransformBoundingFunction R z ↑y) ≤ abs (circleTransformBoundingFunction R z ↑x)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R✝ : ℝ<VAR>z✝ w : ℂ<VAR>R r : ℝ<VAR>hr : r < R<VAR>hr' : 0 ≤ r<VAR>z : ℂ<VAR>cts : ContinuousOn (⇑abs ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ)<GOAL>∃ x, ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])), abs (circleTransformBoundingFunction R z ↑y) ≤ abs (circleTransformBoundingFunction R z ↑x)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R✝ : ℝ<VAR>z✝ w : ℂ<VAR>R r : ℝ<VAR>hr : r < R<VAR>hr' : 0 ≤ r<VAR>z : ℂ<VAR>cts : ContinuousOn (⇑abs ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ)<VAR>comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]])<GOAL>∃ x, ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])), abs (circleTransformBoundingFunction R z ↑y) ≤ abs (circleTransformBoundingFunction R z ↑x)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R✝ : ℝ<VAR>z✝ w : ℂ<VAR>R r : ℝ<VAR>hr : r < R<VAR>hr' : 0 ≤ r<VAR>z : ℂ<VAR>cts : ContinuousOn (⇑abs ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ)<VAR>comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]])<VAR>none : (closedBall z r ×ˢ [[0, 2 * π]]).Nonempty<GOAL>∃ x, ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])), abs (circleTransformBoundingFunction R z ↑y) ≤ abs (circleTransformBoundingFunction R z ↑x)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R✝ : ℝ<VAR>z✝ w : ℂ<VAR>R r : ℝ<VAR>hr : r < R<VAR>hr' : 0 ≤ r<VAR>z : ℂ<VAR>cts : ContinuousOn (⇑abs ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ)<VAR>comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]])<VAR>none : (closedBall z r ×ˢ [[0, 2 * π]]).Nonempty<VAR>this : ∃ x ∈ closedBall z r ×ˢ [[0, 2 * π]], IsMaxOn (⇑abs ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ [[0, 2 * π]]) x<GOAL>∃ x, ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])), abs (circleTransformBoundingFunction R z ↑y) ≤ abs (circleTransformBoundingFunction R z ↑x)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>γ : Type w<VAR>inst✝ : EMetricSpace γ<VAR>s : Set γ<GOAL>0 < diam s ↔ s.Nontrivial
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>s : Set α<VAR>t : Set β<VAR>h : NullMeasurableSet (s ×ˢ t) (μ.prod ν)<VAR>ht : ν t ≠ 0<GOAL>NullMeasurableSet s μ
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>s : Set α<VAR>t : Set β<VAR>h : NullMeasurableSet (s ×ˢ t) (μ.prod ν)<VAR>ht : ν t ≠ 0<GOAL>NullMeasurableSet (t ×ˢ s) (ν.prod μ)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>s : Set α<VAR>t : Set β<VAR>h : NullMeasurableSet (s ×ˢ t) (μ.prod ν)<VAR>ht : ν t ≠ 0<GOAL>NullMeasurableSet (Prod.swap ⁻¹' s ×ˢ t) (ν.prod μ)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p : ι → P<VAR>i : ι<VAR>his : i ∈ s<VAR>hwi : w i = 1<VAR>hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0<GOAL>(affineCombination k s p) w = p i
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p : ι → P<VAR>i : ι<VAR>his : i ∈ s<VAR>hwi : w i = 1<VAR>hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0<VAR>h1 : ∑ i ∈ s, w i = 1<GOAL>(affineCombination k s p) w = p i
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p : ι → P<VAR>i : ι<VAR>his : i ∈ s<VAR>hwi : w i = 1<VAR>hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0<VAR>h1 : ∑ i ∈ s, w i = 1<GOAL>∑ i_1 ∈ s, w i_1 • (p i_1 -ᵥ p i) +ᵥ p i = p i
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p : ι → P<VAR>i : ι<VAR>his : i ∈ s<VAR>hwi : w i = 1<VAR>hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0<VAR>h1 : ∑ i ∈ s, w i = 1<GOAL>∑ i_1 ∈ s, w i_1 • (p i_1 -ᵥ p i) = 0
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p : ι → P<VAR>i : ι<VAR>his : i ∈ s<VAR>hwi : w i = 1<VAR>hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0<VAR>h1 : ∑ i ∈ s, w i = 1<GOAL>∀ x ∈ s, w x • (p x -ᵥ p i) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝¹ : CompleteLattice α<VAR>f✝ g s t : ι → α<VAR>a✝ b : α<VAR>inst✝ : Nonempty ι<VAR>f : ι → α<VAR>a : α<GOAL>(⨅ x, f x) ⊓ a = ⨅ x, f x ⊓ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>c : ComplexMeasure α<VAR>inst✝ : c.HaveLebesgueDecomposition μ<GOAL>c.singularPart μ + μ.withDensityᵥ (c.rnDeriv μ) = c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>c : ComplexMeasure α<VAR>inst✝ : c.HaveLebesgueDecomposition μ<GOAL>c.singularPart μ + μ.withDensityᵥ (c.rnDeriv μ) = (re c).toComplexMeasure (im c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>c : ComplexMeasure α<VAR>inst✝ : c.HaveLebesgueDecomposition μ<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>↑(c.singularPart μ + μ.withDensityᵥ (c.rnDeriv μ)) i = ↑((re c).toComplexMeasure (im c)) i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>c : ComplexMeasure α<VAR>inst✝ : c.HaveLebesgueDecomposition μ<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>↑(c.singularPart μ) i + ↑(μ.withDensityᵥ (c.rnDeriv μ)) i = { re := ↑(re c) i, im := ↑(im c) i }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>c : ComplexMeasure α<VAR>inst✝ : c.HaveLebesgueDecomposition μ<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>(↑(c.singularPart μ) i + ↑(μ.withDensityᵥ (c.rnDeriv μ)) i).re = { re := ↑(re c) i, im := ↑(im c) i }.re
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>c : ComplexMeasure α<VAR>inst✝ : c.HaveLebesgueDecomposition μ<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>(↑(c.singularPart μ) i + ↑(μ.withDensityᵥ (c.rnDeriv μ)) i).im = { re := ↑(re c) i, im := ↑(im c) i }.im
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>c : E<VAR>inst✝ : NeZero μ<VAR>hp_zero : p ≠ 0<GOAL>‖(Lp.const p μ) c‖ = ‖c‖ * (μ Set.univ).toReal ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>c : E<VAR>inst✝ : NeZero μ<VAR>hp_zero : p ≠ 0<VAR>this : μ ≠ 0<GOAL>‖(Lp.const p μ) c‖ = ‖c‖ * (μ Set.univ).toReal ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>c : E<VAR>inst✝ : NeZero μ<VAR>hp_zero : p ≠ 0<VAR>this : μ ≠ 0<GOAL>(↑‖c‖₊ * μ Set.univ ^ (1 / p.toReal)).toReal = ‖c‖ * (μ Set.univ).toReal ^ (1 / p.toReal)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>p : X → Prop<VAR>s : Set X<VAR>x : ↑s<GOAL>map Subtype.val (𝓝 x) = 𝓝[s] ↑x
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>h : ContfracLegendre.Ass ξ u v<GOAL>0 < fract ξ
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>h : ContfracLegendre.Ass ξ u v<VAR>hv₀ : 0 < ↑v<GOAL>0 < fract ξ
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>h : ContfracLegendre.Ass ξ u v<VAR>hv₀ hv₁ : 0 < ↑v<VAR>hv₂ : 0 < 2 * ↑v - 1<GOAL>0 < fract ξ
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>hv₀ hv₁ : 0 < ↑v<VAR>hv₂ : 0 < 2 * ↑v - 1<VAR>hcop : IsCoprime u v<VAR>left✝ : v = 1 → -(1 / 2) < ξ - ↑u<VAR>h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹<GOAL>0 < fract ξ
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>hv₀ hv₁ : 0 < ↑v<VAR>hv₂ : 0 < 2 * ↑v - 1<VAR>hcop : IsCoprime u v<VAR>left✝ : v = 1 → -(1 / 2) < ξ - ↑u<VAR>h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹<VAR>hf : ξ = ↑⌊ξ⌋<GOAL>False
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>hv₀ hv₁ : 0 < ↑v<VAR>hv₂ : 0 < 2 * ↑v - 1<VAR>hcop : IsCoprime u v<VAR>left✝ : v = 1 → -(1 / 2) < ξ - ↑u<VAR>h : |↑⌊ξ⌋ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹<VAR>hf : ξ = ↑⌊ξ⌋<GOAL>False
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>hv₀ hv₁ : 0 < ↑v<VAR>hv₂ : 0 < 2 * ↑v - 1<VAR>hcop : IsCoprime u v<VAR>left✝ : v = 1 → -(1 / 2) < ξ - ↑u<VAR>h : |↑⌊ξ⌋ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹<VAR>hf : ξ = ↑⌊ξ⌋<VAR>H : 2 * ↑v - 1 < 1<GOAL>False
<VAR>G : Type uG<VAR>E' : Type uE'<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>g : G → E'<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>μ : Measure G<VAR>inst✝⁹ : NormedSpace ℝ E'<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedSpace ℝ G<VAR>inst✝⁶ : HasContDiffBump G<VAR>inst✝⁵ : CompleteSpace E'<VAR>φ✝ : ContDiffBump 0<VAR>x₀ : G<VAR>inst✝⁴ : BorelSpace G<VAR>inst✝³ : IsLocallyFiniteMeasure μ<VAR>inst✝² : μ.IsOpenPosMeasure<VAR>inst✝¹ : FiniteDimensional ℝ G<VAR>inst✝ : μ.IsAddLeftInvariant<VAR>ι : Type u_1<VAR>φ : ι → ContDiffBump 0<VAR>l : Filter ι<VAR>K : ℝ<VAR>hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)<VAR>h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn<VAR>hg : LocallyIntegrable g μ<VAR>this : μ.IsAddHaarMeasure<GOAL>∀ᵐ (x₀ : G) ∂μ, Tendsto (fun i => ((φ i).normed μ ⋆[lsmul ℝ ℝ, μ] g) x₀) l (𝓝 (g x₀))
<VAR>G : Type uG<VAR>E' : Type uE'<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>g : G → E'<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>μ : Measure G<VAR>inst✝⁹ : NormedSpace ℝ E'<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedSpace ℝ G<VAR>inst✝⁶ : HasContDiffBump G<VAR>inst✝⁵ : CompleteSpace E'<VAR>φ✝ : ContDiffBump 0<VAR>x₀✝ : G<VAR>inst✝⁴ : BorelSpace G<VAR>inst✝³ : IsLocallyFiniteMeasure μ<VAR>inst✝² : μ.IsOpenPosMeasure<VAR>inst✝¹ : FiniteDimensional ℝ G<VAR>inst✝ : μ.IsAddLeftInvariant<VAR>ι : Type u_1<VAR>φ : ι → ContDiffBump 0<VAR>l : Filter ι<VAR>K : ℝ<VAR>hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)<VAR>h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn<VAR>hg : LocallyIntegrable g μ<VAR>this : μ.IsAddHaarMeasure<VAR>x₀ : G<VAR>h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ((Besicovitch.vitaliFamily μ).filterAt x₀) (𝓝 0)<GOAL>Tendsto (fun i => ((φ i).normed μ ⋆[lsmul ℝ ℝ, μ] g) x₀) l (𝓝 (g x₀))
<VAR>G : Type uG<VAR>E' : Type uE'<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>g : G → E'<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>μ : Measure G<VAR>inst✝⁹ : NormedSpace ℝ E'<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedSpace ℝ G<VAR>inst✝⁶ : HasContDiffBump G<VAR>inst✝⁵ : CompleteSpace E'<VAR>φ✝ : ContDiffBump 0<VAR>x₀✝ : G<VAR>inst✝⁴ : BorelSpace G<VAR>inst✝³ : IsLocallyFiniteMeasure μ<VAR>inst✝² : μ.IsOpenPosMeasure<VAR>inst✝¹ : FiniteDimensional ℝ G<VAR>inst✝ : μ.IsAddLeftInvariant<VAR>ι : Type u_1<VAR>φ : ι → ContDiffBump 0<VAR>l : Filter ι<VAR>K : ℝ<VAR>hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)<VAR>h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn<VAR>hg : LocallyIntegrable g μ<VAR>this : μ.IsAddHaarMeasure<VAR>x₀ : G<VAR>h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ((Besicovitch.vitaliFamily μ).filterAt x₀) (𝓝 0)<GOAL>Tendsto (fun i => ∫ (t : G), (φ i).normed μ (x₀ - t) • g t ∂μ) l (𝓝 (g x₀))
<VAR>G : Type uG<VAR>E' : Type uE'<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>g : G → E'<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>μ : Measure G<VAR>inst✝⁹ : NormedSpace ℝ E'<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedSpace ℝ G<VAR>inst✝⁶ : HasContDiffBump G<VAR>inst✝⁵ : CompleteSpace E'<VAR>φ✝ : ContDiffBump 0<VAR>x₀✝ : G<VAR>inst✝⁴ : BorelSpace G<VAR>inst✝³ : IsLocallyFiniteMeasure μ<VAR>inst✝² : μ.IsOpenPosMeasure<VAR>inst✝¹ : FiniteDimensional ℝ G<VAR>inst✝ : μ.IsAddLeftInvariant<VAR>ι : Type u_1<VAR>φ : ι → ContDiffBump 0<VAR>l : Filter ι<VAR>K : ℝ<VAR>hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)<VAR>h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn<VAR>hg : LocallyIntegrable g μ<VAR>this : μ.IsAddHaarMeasure<VAR>x₀ : G<VAR>h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ((Besicovitch.vitaliFamily μ).filterAt x₀) (𝓝 0)<VAR>hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[>] 0)<GOAL>Tendsto (fun i => ∫ (t : G), (φ i).normed μ (x₀ - t) • g t ∂μ) l (𝓝 (g x₀))
<VAR>G : Type uG<VAR>E' : Type uE'<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>g : G → E'<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>μ : Measure G<VAR>inst✝⁹ : NormedSpace ℝ E'<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedSpace ℝ G<VAR>inst✝⁶ : HasContDiffBump G<VAR>inst✝⁵ : CompleteSpace E'<VAR>φ✝ : ContDiffBump 0<VAR>x₀✝ : G<VAR>inst✝⁴ : BorelSpace G<VAR>inst✝³ : IsLocallyFiniteMeasure μ<VAR>inst✝² : μ.IsOpenPosMeasure<VAR>inst✝¹ : FiniteDimensional ℝ G<VAR>inst✝ : μ.IsAddLeftInvariant<VAR>ι : Type u_1<VAR>φ : ι → ContDiffBump 0<VAR>l : Filter ι<VAR>K : ℝ<VAR>hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)<VAR>h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn<VAR>hg : LocallyIntegrable g μ<VAR>this✝ : μ.IsAddHaarMeasure<VAR>x₀ : G<VAR>h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ((Besicovitch.vitaliFamily μ).filterAt x₀) (𝓝 0)<VAR>hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[>] 0)<VAR>this : Tendsto (((fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ∘ fun r => closedBall x₀ r) ∘ fun i => (φ i).rOut) l (𝓝 0)<GOAL>Tendsto (fun i => ∫ (t : G), (φ i).normed μ (x₀ - t) • g t ∂μ) l (𝓝 (g x₀))
<VAR>G : Type uG<VAR>E' : Type uE'<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>g : G → E'<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>μ : Measure G<VAR>inst✝⁹ : NormedSpace ℝ E'<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedSpace ℝ G<VAR>inst✝⁶ : HasContDiffBump G<VAR>inst✝⁵ : CompleteSpace E'<VAR>φ✝ : ContDiffBump 0<VAR>x₀✝ : G<VAR>inst✝⁴ : BorelSpace G<VAR>inst✝³ : IsLocallyFiniteMeasure μ<VAR>inst✝² : μ.IsOpenPosMeasure<VAR>inst✝¹ : FiniteDimensional ℝ G<VAR>inst✝ : μ.IsAddLeftInvariant<VAR>ι : Type u_1<VAR>φ : ι → ContDiffBump 0<VAR>l : Filter ι<VAR>K : ℝ<VAR>hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)<VAR>h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn<VAR>hg : LocallyIntegrable g μ<VAR>this✝ : μ.IsAddHaarMeasure<VAR>x₀ : G<VAR>h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ((Besicovitch.vitaliFamily μ).filterAt x₀) (𝓝 0)<VAR>hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[>] 0)<VAR>this : Tendsto (fun x => ⨍ (y : G) in closedBall x₀ (φ x).rOut, ‖g y - g x₀‖ ∂μ) l (𝓝 0)<GOAL>Tendsto (fun i => ∫ (t : G), (φ i).normed μ (x₀ - t) • g t ∂μ) l (𝓝 (g x₀))
<VAR>G : Type uG<VAR>E' : Type uE'<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>g : G → E'<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>μ : Measure G<VAR>inst✝⁹ : NormedSpace ℝ E'<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedSpace ℝ G<VAR>inst✝⁶ : HasContDiffBump G<VAR>inst✝⁵ : CompleteSpace E'<VAR>φ✝ : ContDiffBump 0<VAR>x₀✝ : G<VAR>inst✝⁴ : BorelSpace G<VAR>inst✝³ : IsLocallyFiniteMeasure μ<VAR>inst✝² : μ.IsOpenPosMeasure<VAR>inst✝¹ : FiniteDimensional ℝ G<VAR>inst✝ : μ.IsAddLeftInvariant<VAR>ι : Type u_1<VAR>φ : ι → ContDiffBump 0<VAR>l : Filter ι<VAR>K : ℝ<VAR>hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)<VAR>h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn<VAR>hg : LocallyIntegrable g μ<VAR>this✝ : μ.IsAddHaarMeasure<VAR>x₀ : G<VAR>h₀ : Tendsto (fun a => ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ((Besicovitch.vitaliFamily μ).filterAt x₀) (𝓝 0)<VAR>hφ' : Tendsto (fun i => (φ i).rOut) l (𝓝[>] 0)<VAR>this : Tendsto (fun x => ⨍ (y : G) in closedBall x₀ (φ x).rOut, ‖g y - g x₀‖ ∂μ) l (𝓝 0)<GOAL>∀ᶠ (i : ι) in l, IntegrableOn g (closedBall x₀ (φ i).rOut) μ