ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MetricSpace E<VAR>u : Filter ι<VAR>u.NeBot<VAR>u.IsCountablyGenerated<VAR>f : ι → α → E<VAR>g : α → E<VAR>hfg : MeasureTheory.TendstoInMeasure μ f u g<GOAL>∃ ns, ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun i => f (ns i) x) Filter.atTop (𝓝 (g x))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace E<VAR>NormedAddCommGroup E<VAR>BorelSpace E<VAR>u : Filter ι<VAR>u.NeBot<VAR>u.IsCountablyGenerated<VAR>f : ι → α → E<VAR>g : α → E<VAR>hf : ∀ (n : ι), AEMeasurable (f n) μ<VAR>h_tendsto : MeasureTheory.TendstoInMeasure μ f u g<GOAL>AEMeasurable g μ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>f : ι → α → E<VAR>g : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : ∀ (n : ι), MeasureTheory.StronglyMeasurable (f n)<VAR>hg : MeasureTheory.StronglyMeasurable g<VAR>l : Filter ι<VAR>hfg : Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) p μ) l (𝓝 0)<GOAL>MeasureTheory.TendstoInMeasure μ f l g
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>f : ι → α → E<VAR>g : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : ∀ (n : ι), MeasureTheory.AEStronglyMeasurable (f n) μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<VAR>l : Filter ι<VAR>hfg : Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) p μ) l (𝓝 0)<GOAL>MeasureTheory.TendstoInMeasure μ f l g
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>f : ι → α → E<VAR>g : α → E<VAR>l : Filter ι<VAR>hfg : Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) ⊤ μ) l (𝓝 0)<GOAL>MeasureTheory.TendstoInMeasure μ f l g
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>f : ι → α → E<VAR>g : α → E<VAR>l : Filter ι<VAR>hp_ne_zero : p ≠ 0<VAR>hf : ∀ (n : ι), MeasureTheory.AEStronglyMeasurable (f n) μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<VAR>hfg : Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) p μ) l (𝓝 0)<GOAL>MeasureTheory.TendstoInMeasure μ f l g
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>hp : Fact (1 ≤ p)<VAR>f : ι → ↥(MeasureTheory.Lp E p μ)<VAR>g : ↥(MeasureTheory.Lp E p μ)<VAR>l : Filter ι<VAR>hfg : Filter.Tendsto f l (𝓝 g)<GOAL>MeasureTheory.TendstoInMeasure μ (fun n => ↑↑(f n)) l ↑↑g
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>n : ℕ<VAR>I : BoxIntegral.Box (Fin (n + 1))<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f (BoxIntegral.Box.Icc I)<VAR>Hd : ∀ x ∈ BoxIntegral.Box.Icc I \ s, HasFDerivWithinAt f (f' x) (BoxIntegral.Box.Icc I) x<VAR>Hi : MeasureTheory.IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (Pi.single i 1) i) (BoxIntegral.Box.Icc I) MeasureTheory.volume<GOAL>∫ (x : Fin (n + 1) → ℝ) in BoxIntegral.Box.Icc I, ∑ i : Fin (n + 1), (f' x) (Pi.single i 1) i = ∑ i : Fin (n + 1), ((∫ (x : Fin n → ℝ) in BoxIntegral.Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) - ∫ (x : Fin n → ℝ) in BoxIntegral.Box.Icc (I.face i), f (i.insertNth (I.lower i) x) i)
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>n : ℕ<VAR>I : BoxIntegral.Box (Fin (n + 1))<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f (BoxIntegral.Box.Icc I)<VAR>Hd : ∀ x ∈ BoxIntegral.Box.Ioo I \ s, HasFDerivAt f (f' x) x<VAR>Hi : MeasureTheory.IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (Pi.single i 1) i) (BoxIntegral.Box.Icc I) MeasureTheory.volume<GOAL>∫ (x : Fin (n + 1) → ℝ) in BoxIntegral.Box.Icc I, ∑ i : Fin (n + 1), (f' x) (Pi.single i 1) i = ∑ i : Fin (n + 1), ((∫ (x : Fin n → ℝ) in BoxIntegral.Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) - ∫ (x : Fin n → ℝ) in BoxIntegral.Box.Icc (I.face i), f (i.insertNth (I.lower i) x) i)
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>n : ℕ<VAR>a b : Fin (n + 1) → ℝ<VAR>hle : a ≤ b<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f (Set.Icc a b)<VAR>Hd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x<VAR>Hi : MeasureTheory.IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (Pi.single i 1) i) (Set.Icc a b) MeasureTheory.volume<GOAL>∫ (x : Fin (n + 1) → ℝ) in Set.Icc a b, ∑ i : Fin (n + 1), (f' x) (Pi.single i 1) i = ∑ i : Fin (n + 1), ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (b i) x) i) - ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (a i) x) i)
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>n : ℕ<VAR>a b : Fin (n + 1) → ℝ<VAR>hle : a ≤ b<VAR>f : Fin (n + 1) → (Fin (n + 1) → ℝ) → E<VAR>f' : Fin (n + 1) → (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)<VAR>Hd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x<VAR>Hi : MeasureTheory.IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' i x) (Pi.single i 1)) (Set.Icc a b) MeasureTheory.volume<GOAL>∫ (x : Fin (n + 1) → ℝ) in Set.Icc a b, ∑ i : Fin (n + 1), (f' i x) (Pi.single i 1) = ∑ i : Fin (n + 1), ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f i (i.insertNth (b i) x)) - ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f i (i.insertNth (a i) x))
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>n : ℕ<VAR>F : Type u_1<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>PartialOrder F<VAR>MeasureTheory.MeasureSpace F<VAR>BorelSpace F<VAR>eL : F ≃L[ℝ] Fin (n + 1) → ℝ<VAR>he_ord : ∀ (x y : F), eL x ≤ eL y ↔ x ≤ y<VAR>he_vol : MeasureTheory.MeasurePreserving (⇑eL) MeasureTheory.volume MeasureTheory.volume<VAR>f : Fin (n + 1) → F → E<VAR>f' : Fin (n + 1) → F → F →L[ℝ] E<VAR>s : Set F<VAR>hs : s.Countable<VAR>a b : F<VAR>hle : a ≤ b<VAR>Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)<VAR>Hd : ∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x<VAR>DF : F → E<VAR>hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), (f' i x) (eL.symm (Pi.single i 1))<VAR>Hi : MeasureTheory.IntegrableOn DF (Set.Icc a b) MeasureTheory.volume<GOAL>∫ (x : F) in Set.Icc a b, DF x = ∑ i : Fin (n + 1), ((∫ (x : Fin n → ℝ) in Set.Icc (eL a ∘ i.succAbove) (eL b ∘ i.succAbove), f i (eL.symm (i.insertNth (eL b i) x))) - ∫ (x : Fin n → ℝ) in Set.Icc (eL a ∘ i.succAbove) (eL b ∘ i.succAbove), f i (eL.symm (i.insertNth (eL a i) x)))
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f f' : ℝ → E<VAR>a b : ℝ<VAR>hle : a ≤ b<VAR>s : Set ℝ<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f (Set.Icc a b)<VAR>Hd : ∀ x ∈ Set.Ioo a b \ s, HasDerivAt f (f' x) x<VAR>Hi : IntervalIntegrable f' MeasureTheory.volume a b<GOAL>∫ (x : ℝ) in a..b, f' x = f b - f a
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f f' : ℝ → E<VAR>a b : ℝ<VAR>s : Set ℝ<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f [[a, b]]<VAR>Hd : ∀ x ∈ Set.Ioo (min a b) (max a b) \ s, HasDerivAt f (f' x) x<VAR>Hi : IntervalIntegrable f' MeasureTheory.volume a b<GOAL>∫ (x : ℝ) in a..b, f' x = f b - f a
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f g : ℝ × ℝ → E<VAR>f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E<VAR>a b : ℝ × ℝ<VAR>hle : a ≤ b<VAR>s : Set (ℝ × ℝ)<VAR>hs : s.Countable<VAR>Hcf : ContinuousOn f (Set.Icc a b)<VAR>Hcg : ContinuousOn g (Set.Icc a b)<VAR>Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x<VAR>Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x<VAR>Hi : MeasureTheory.IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) MeasureTheory.volume<GOAL>∫ (x : ℝ × ℝ) in Set.Icc a b, (f' x) (1, 0) + (g' x) (0, 1) = (((∫ (x : ℝ) in a.1 ..b.1, g (x, b.2)) - ∫ (x : ℝ) in a.1 ..b.1, g (x, a.2)) + ∫ (y : ℝ) in a.2 ..b.2, f (b.1, y)) - ∫ (y : ℝ) in a.2 ..b.2, f (a.1, y)
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f g : ℝ × ℝ → E<VAR>f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E<VAR>a₁ a₂ b₁ b₂ : ℝ<VAR>s : Set (ℝ × ℝ)<VAR>hs : s.Countable<VAR>Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])<VAR>Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])<VAR>Hdf : ∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt f (f' x) x<VAR>Hdg : ∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt g (g' x) x<VAR>Hi : MeasureTheory.IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) MeasureTheory.volume<GOAL>∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, (f' (x, y)) (1, 0) + (g' (x, y)) (0, 1) = (((∫ (x : ℝ) in a₁..b₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) + ∫ (y : ℝ) in a₂..b₂, f (b₁, y)) - ∫ (y : ℝ) in a₂..b₂, f (a₁, y)
<VAR>α : Type u_1<GOAL>∀ {x : MeasurableSpace α} {f : α → ℝ}, (Measurable fun x => Real.exp (f x)) → Measurable f
<VAR>α : Type u_1<GOAL>∀ {x : MeasurableSpace α} {f : α → ℝ} {μ : MeasureTheory.Measure α}, AEMeasurable (fun x => Real.exp (f x)) μ → AEMeasurable f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → ℝ<VAR>hf : Measurable f<GOAL>Measurable fun x => Real.exp (f x)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → ℝ<VAR>hf : Measurable f<GOAL>Measurable fun x => Real.log (f x)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → ℝ<VAR>hf : Measurable f<GOAL>Measurable fun x => Real.cos (f x)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → ℝ<VAR>hf : Measurable f<GOAL>Measurable fun x => Real.sin (f x)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → ℝ<VAR>hf : Measurable f<GOAL>Measurable fun x => Real.cosh (f x)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → ℝ<VAR>hf : Measurable f<GOAL>Measurable fun x => Real.sinh (f x)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → ℝ<VAR>hf : Measurable f<GOAL>Measurable fun x => √(f x)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → ℂ<VAR>hf : Measurable f<GOAL>Measurable fun x => Complex.exp (f x)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → ℂ<VAR>hf : Measurable f<GOAL>Measurable fun x => Complex.cos (f x)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → ℂ<VAR>hf : Measurable f<GOAL>Measurable fun x => Complex.sin (f x)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → ℂ<VAR>hf : Measurable f<GOAL>Measurable fun x => Complex.cosh (f x)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → ℂ<VAR>hf : Measurable f<GOAL>Measurable fun x => Complex.sinh (f x)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → ℂ<VAR>hf : Measurable f<GOAL>Measurable fun x => (f x).arg
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → ℂ<VAR>hf : Measurable f<GOAL>Measurable fun x => Complex.log (f x)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace α<VAR>BorelSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>hs : MeasurableSet s<VAR>h'st : t ∈ 𝓝[s] x₀<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)<VAR>hiφ : Filter.Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)<VAR>h'iφ : ∀ᶠ (i : ι) in l, MeasureTheory.AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>hmg : MeasureTheory.IntegrableOn g s μ<VAR>hcg : Filter.Tendsto g (𝓝[s] x₀) (𝓝 a)<GOAL>∀ᶠ (i : ι) in l, MeasureTheory.IntegrableOn (fun x => φ i x • g x) s μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace α<VAR>BorelSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ : ι → α → ℝ<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hts : t ⊆ s<VAR>h'ts : t ∈ 𝓝[s] x₀<VAR>hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)<VAR>hiφ : Filter.Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)<VAR>h'iφ : ∀ᶠ (i : ι) in l, MeasureTheory.AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>hmg : MeasureTheory.IntegrableOn g s μ<VAR>hcg : Filter.Tendsto g (𝓝[s] x₀) (𝓝 0)<GOAL>Filter.Tendsto (fun i => ∫ (x : α) in s, φ i x • g x ∂μ) l (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace α<VAR>BorelSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>CompleteSpace E<VAR>hs : MeasurableSet s<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hts : t ⊆ s<VAR>h'ts : t ∈ 𝓝[s] x₀<VAR>h't : μ t ≠ ⊤<VAR>hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)<VAR>hiφ : Filter.Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)<VAR>h'iφ : ∀ᶠ (i : ι) in l, MeasureTheory.AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>hmg : MeasureTheory.IntegrableOn g s μ<VAR>hcg : Filter.Tendsto g (𝓝[s] x₀) (𝓝 a)<GOAL>Filter.Tendsto (fun i => ∫ (x : α) in s, φ i x • g x ∂μ) l (𝓝 a)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace α<VAR>BorelSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>CompleteSpace E<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>h'ts : t ∈ 𝓝 x₀<VAR>h't : μ t ≠ ⊤<VAR>hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), 0 ≤ φ i x<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l uᶜ<VAR>hiφ : Filter.Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)<VAR>h'iφ : ∀ᶠ (i : ι) in l, MeasureTheory.AEStronglyMeasurable (φ i) μ<VAR>hmg : MeasureTheory.Integrable g μ<VAR>hcg : Filter.Tendsto g (𝓝 x₀) (𝓝 a)<GOAL>Filter.Tendsto (fun i => ∫ (x : α), φ i x • g x ∂μ) l (𝓝 a)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>hm : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace α<VAR>BorelSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>g : α → E<VAR>x₀ : α<VAR>s : Set α<VAR>CompleteSpace E<VAR>TopologicalSpace.MetrizableSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>hs : IsCompact s<VAR>hμ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → 0 < μ (u ∩ s)<VAR>c : α → ℝ<VAR>hc : ContinuousOn c s<VAR>h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀<VAR>hnc : ∀ x ∈ s, 0 ≤ c x<VAR>hnc₀ : 0 < c x₀<VAR>h₀ : x₀ ∈ s<VAR>hmg : MeasureTheory.IntegrableOn g s μ<VAR>hcg : ContinuousWithinAt g s x₀<GOAL>Filter.Tendsto (fun n => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ n • g x ∂μ) Filter.atTop (𝓝 (g x₀))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>hm : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace α<VAR>BorelSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>g : α → E<VAR>x₀ : α<VAR>s : Set α<VAR>CompleteSpace E<VAR>TopologicalSpace.MetrizableSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>μ.IsOpenPosMeasure<VAR>hs : IsCompact s<VAR>c : α → ℝ<VAR>hc : ContinuousOn c s<VAR>h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀<VAR>hnc : ∀ x ∈ s, 0 ≤ c x<VAR>hnc₀ : 0 < c x₀<VAR>h₀ : x₀ ∈ closure (interior s)<VAR>hmg : MeasureTheory.IntegrableOn g s μ<VAR>hcg : ContinuousWithinAt g s x₀<GOAL>Filter.Tendsto (fun n => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ n • g x ∂μ) Filter.atTop (𝓝 (g x₀))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>hm : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace α<VAR>BorelSpace α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>g : α → E<VAR>x₀ : α<VAR>s : Set α<VAR>CompleteSpace E<VAR>TopologicalSpace.MetrizableSpace α<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>μ.IsOpenPosMeasure<VAR>hs : IsCompact s<VAR>c : α → ℝ<VAR>hc : ContinuousOn c s<VAR>h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀<VAR>hnc : ∀ x ∈ s, 0 ≤ c x<VAR>hnc₀ : 0 < c x₀<VAR>h₀ : x₀ ∈ closure (interior s)<VAR>hmg : ContinuousOn g s<GOAL>Filter.Tendsto (fun n => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ n • g x ∂μ) Filter.atTop (𝓝 (g x₀))
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>FiniteDimensional ℝ F<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>μ : MeasureTheory.Measure F<VAR>μ.IsAddHaarMeasure<VAR>φ : F → ℝ<VAR>hφ : ∀ (x : F), 0 ≤ φ x<VAR>h'φ : ∫ (x : F), φ x ∂μ = 1<VAR>h : Filter.Tendsto (fun x => ‖x‖ ^ FiniteDimensional.finrank ℝ F * φ x) (Bornology.cobounded F) (𝓝 0)<VAR>g : F → E<VAR>hg : MeasureTheory.Integrable g μ<VAR>h'g : ContinuousAt g 0<GOAL>Filter.Tendsto (fun c => ∫ (x : F), (c ^ FiniteDimensional.finrank ℝ F * φ (c • x)) • g x ∂μ) Filter.atTop (𝓝 (g 0))
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>FiniteDimensional ℝ F<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>μ : MeasureTheory.Measure F<VAR>μ.IsAddHaarMeasure<VAR>φ : F → ℝ<VAR>hφ : ∀ (x : F), 0 ≤ φ x<VAR>h'φ : ∫ (x : F), φ x ∂μ = 1<VAR>h : Filter.Tendsto (fun x => ‖x‖ ^ FiniteDimensional.finrank ℝ F * φ x) (Bornology.cobounded F) (𝓝 0)<VAR>g : F → E<VAR>x₀ : F<VAR>hg : MeasureTheory.Integrable g μ<VAR>h'g : ContinuousAt g x₀<GOAL>Filter.Tendsto (fun c => ∫ (x : F), (c ^ FiniteDimensional.finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ) Filter.atTop (𝓝 (g x₀))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>φ : ι → Set α<VAR>self : MeasureTheory.AECover μ l φ<VAR>i : ι<GOAL>MeasurableSet (φ i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>φ : ι → Set α<VAR>self : MeasureTheory.AECover μ l φ<GOAL>∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in l, x ∈ φ i
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>φ ψ : ι → Set α<VAR>hφ : MeasureTheory.AECover μ l φ<VAR>hψ : MeasureTheory.AECover μ l ψ<GOAL>MeasureTheory.AECover μ l fun i => φ i ∩ ψ i
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>φ ψ : ι → Set α<VAR>hφ : MeasureTheory.AECover μ l φ<VAR>hsub : ∀ (i : ι), φ i ⊆ ψ i<VAR>hmeas : ∀ (i : ι), MeasurableSet (ψ i)<GOAL>MeasureTheory.AECover μ l ψ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>ν : MeasureTheory.Measure α<VAR>φ : ι → Set α<VAR>hφ : MeasureTheory.AECover μ l φ<VAR>hle : ν ≪ μ<GOAL>MeasureTheory.AECover ν l φ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>ν : MeasureTheory.Measure α<VAR>φ : ι → Set α<VAR>hφ : MeasureTheory.AECover μ l φ<VAR>hle : ν ≤ μ<GOAL>MeasureTheory.AECover ν l φ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>PseudoMetricSpace α<VAR>OpensMeasurableSpace α<VAR>x : α<VAR>r : ι → ℝ<VAR>hr : Filter.Tendsto r l Filter.atTop<GOAL>MeasureTheory.AECover μ l fun i => Metric.ball x (r i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>PseudoMetricSpace α<VAR>OpensMeasurableSpace α<VAR>x : α<VAR>r : ι → ℝ<VAR>hr : Filter.Tendsto r l Filter.atTop<GOAL>MeasureTheory.AECover μ l fun i => Metric.closedBall x (r i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>Preorder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>OpensMeasurableSpace α<VAR>a : ι → α<VAR>ha : Filter.Tendsto a l Filter.atBot<GOAL>MeasureTheory.AECover μ l fun i => Set.Ici (a i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>Preorder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>OpensMeasurableSpace α<VAR>b : ι → α<VAR>hb : Filter.Tendsto b l Filter.atTop<GOAL>MeasureTheory.AECover μ l fun i => Set.Iic (b i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>Preorder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>OpensMeasurableSpace α<VAR>a b : ι → α<VAR>ha : Filter.Tendsto a l Filter.atBot<VAR>hb : Filter.Tendsto b l Filter.atTop<GOAL>MeasureTheory.AECover μ l fun i => Set.Icc (a i) (b i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>OpensMeasurableSpace α<VAR>a : ι → α<VAR>ha : Filter.Tendsto a l Filter.atBot<VAR>NoMinOrder α<GOAL>MeasureTheory.AECover μ l fun i => Set.Ioi (a i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>OpensMeasurableSpace α<VAR>b : ι → α<VAR>hb : Filter.Tendsto b l Filter.atTop<VAR>NoMaxOrder α<GOAL>MeasureTheory.AECover μ l fun i => Set.Iio (b i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>OpensMeasurableSpace α<VAR>a b : ι → α<VAR>ha : Filter.Tendsto a l Filter.atBot<VAR>hb : Filter.Tendsto b l Filter.atTop<VAR>NoMinOrder α<VAR>NoMaxOrder α<GOAL>MeasureTheory.AECover μ l fun i => Set.Ioo (a i) (b i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>OpensMeasurableSpace α<VAR>a b : ι → α<VAR>ha : Filter.Tendsto a l Filter.atBot<VAR>hb : Filter.Tendsto b l Filter.atTop<VAR>NoMinOrder α<GOAL>MeasureTheory.AECover μ l fun i => Set.Ioc (a i) (b i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>OpensMeasurableSpace α<VAR>a b : ι → α<VAR>ha : Filter.Tendsto a l Filter.atBot<VAR>hb : Filter.Tendsto b l Filter.atTop<VAR>NoMaxOrder α<GOAL>MeasureTheory.AECover μ l fun i => Set.Ico (a i) (b i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>OpensMeasurableSpace α<VAR>a : ι → α<VAR>A : α<VAR>ha : Filter.Tendsto a l (𝓝 A)<GOAL>MeasureTheory.AECover (μ.restrict (Set.Ioi A)) l fun i => Set.Ioi (a i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>OpensMeasurableSpace α<VAR>b : ι → α<VAR>B : α<VAR>hb : Filter.Tendsto b l (𝓝 B)<GOAL>MeasureTheory.AECover (μ.restrict (Set.Iio B)) l fun i => Set.Iio (b i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>OpensMeasurableSpace α<VAR>a : ι → α<VAR>A : α<VAR>ha : Filter.Tendsto a l (𝓝 A)<GOAL>MeasureTheory.AECover (μ.restrict (Set.Ioi A)) l fun i => Set.Ici (a i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>OpensMeasurableSpace α<VAR>b : ι → α<VAR>B : α<VAR>hb : Filter.Tendsto b l (𝓝 B)<GOAL>MeasureTheory.AECover (μ.restrict (Set.Iio B)) l fun i => Set.Iic (b i)