ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hfinε : ε ≠ ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε / 3<VAR>Eg : Set α<VAR>hmEg : MeasurableSet Eg<VAR>hμEg : μ Eg < ⊤<VAR>hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3<VAR>Ef : Set α<VAR>hmEf : MeasurableSet Ef<VAR>hμEf : μ Ef < ⊤<VAR>hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3<VAR>hmE : MeasurableSet (Ef ∪ Eg)<VAR>hfmE : μ (Ef ∪ Eg) < ⊤<GOAL>∃ N, ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hfinε : ε ≠ ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε / 3<VAR>Eg : Set α<VAR>hmEg : MeasurableSet Eg<VAR>hμEg : μ Eg < ⊤<VAR>hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3<VAR>Ef : Set α<VAR>hmEf : MeasurableSet Ef<VAR>hμEf : μ Ef < ⊤<VAR>hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3<VAR>E : Set α := Ef ∪ Eg<VAR>hmE : MeasurableSet E<VAR>hfmE : μ E < ⊤<GOAL>∃ N, ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hfinε : ε ≠ ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε / 3<VAR>Eg : Set α<VAR>hmEg : MeasurableSet Eg<VAR>hμEg : μ Eg < ⊤<VAR>hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3<VAR>Ef : Set α<VAR>hmEf : MeasurableSet Ef<VAR>hμEf : μ Ef < ⊤<VAR>hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3<VAR>E : Set α := Ef ∪ Eg<VAR>hmE : MeasurableSet E<VAR>hfmE : μ E < ⊤<VAR>hgE' : Memℒp g p (μ.restrict E)<GOAL>∃ N, ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hfinε : ε ≠ ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε / 3<VAR>Eg : Set α<VAR>hmEg : MeasurableSet Eg<VAR>hμEg : μ Eg < ⊤<VAR>hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3<VAR>Ef : Set α<VAR>hmEf : MeasurableSet Ef<VAR>hμEf : μ Ef < ⊤<VAR>hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3<VAR>E : Set α := Ef ∪ Eg<VAR>hmE : MeasurableSet E<VAR>hfmE : μ E < ⊤<VAR>hgE' : Memℒp g p (μ.restrict E)<VAR>huiE : UnifIntegrable f p (μ.restrict E)<GOAL>∃ N, ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hfinε : ε ≠ ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε / 3<VAR>Eg : Set α<VAR>hmEg : MeasurableSet Eg<VAR>hμEg : μ Eg < ⊤<VAR>hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3<VAR>Ef : Set α<VAR>hmEf : MeasurableSet Ef<VAR>hμEf : μ Ef < ⊤<VAR>hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3<VAR>E : Set α := Ef ∪ Eg<VAR>hmE : MeasurableSet E<VAR>hfmE : μ E < ⊤<VAR>hgE' : Memℒp g p (μ.restrict E)<VAR>huiE : UnifIntegrable f p (μ.restrict E)<VAR>hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun n => f n x) atTop (𝓝 (g x))<GOAL>∃ N, ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hfinε : ε ≠ ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε / 3<VAR>Eg : Set α<VAR>hmEg : MeasurableSet Eg<VAR>hμEg : μ Eg < ⊤<VAR>hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3<VAR>Ef : Set α<VAR>hmEf : MeasurableSet Ef<VAR>hμEf : μ Ef < ⊤<VAR>hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3<VAR>E : Set α := Ef ∪ Eg<VAR>hmE : MeasurableSet E<VAR>hfmE : μ E < ⊤<VAR>hgE' : Memℒp g p (μ.restrict E)<VAR>huiE : UnifIntegrable f p (μ.restrict E)<VAR>hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ffmE : Fact (μ E < ⊤)<GOAL>∃ N, ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hfinε : ε ≠ ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε / 3<VAR>Eg : Set α<VAR>hmEg : MeasurableSet Eg<VAR>hμEg : μ Eg < ⊤<VAR>hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3<VAR>Ef : Set α<VAR>hmEf : MeasurableSet Ef<VAR>hμEf : μ Ef < ⊤<VAR>hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3<VAR>E : Set α := Ef ∪ Eg<VAR>hmE : MeasurableSet E<VAR>hfmE : μ E < ⊤<VAR>hgE' : Memℒp g p (μ.restrict E)<VAR>huiE : UnifIntegrable f p (μ.restrict E)<VAR>hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ffmE : Fact (μ E < ⊤)<VAR>hInner : Tendsto (fun n => eLpNorm (f n - g) p (μ.restrict E)) atTop (𝓝 0)<GOAL>∃ N, ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hfinε : ε ≠ ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε / 3<VAR>Eg : Set α<VAR>hmEg : MeasurableSet Eg<VAR>hμEg : μ Eg < ⊤<VAR>hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3<VAR>Ef : Set α<VAR>hmEf : MeasurableSet Ef<VAR>hμEf : μ Ef < ⊤<VAR>hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3<VAR>E : Set α := Ef ∪ Eg<VAR>hmE : MeasurableSet E<VAR>hfmE : μ E < ⊤<VAR>hgE' : Memℒp g p (μ.restrict E)<VAR>huiE : UnifIntegrable f p (μ.restrict E)<VAR>hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ffmE : Fact (μ E < ⊤)<VAR>hInner : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε<GOAL>∃ N, ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hfinε : ε ≠ ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε / 3<VAR>Eg : Set α<VAR>hmEg : MeasurableSet Eg<VAR>hμEg : μ Eg < ⊤<VAR>hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3<VAR>Ef : Set α<VAR>hmEf : MeasurableSet Ef<VAR>hμEf : μ Ef < ⊤<VAR>hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3<VAR>E : Set α := Ef ∪ Eg<VAR>hmE : MeasurableSet E<VAR>hfmE : μ E < ⊤<VAR>hgE' : Memℒp g p (μ.restrict E)<VAR>huiE : UnifIntegrable f p (μ.restrict E)<VAR>hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ffmE : Fact (μ E < ⊤)<VAR>hInner : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε<VAR>N : ℕ<VAR>hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3<GOAL>∃ N, ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hfinε : ε ≠ ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε / 3<VAR>Eg : Set α<VAR>hmEg : MeasurableSet Eg<VAR>hμEg : μ Eg < ⊤<VAR>hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3<VAR>Ef : Set α<VAR>hmEf : MeasurableSet Ef<VAR>hμEf : μ Ef < ⊤<VAR>hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3<VAR>E : Set α := Ef ∪ Eg<VAR>hmE : MeasurableSet E<VAR>hfmE : μ E < ⊤<VAR>hgE' : Memℒp g p (μ.restrict E)<VAR>huiE : UnifIntegrable f p (μ.restrict E)<VAR>hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ffmE : Fact (μ E < ⊤)<VAR>hInner : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε<VAR>N : ℕ<VAR>hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3<GOAL>∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hfinε : ε ≠ ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε / 3<VAR>Eg : Set α<VAR>hmEg : MeasurableSet Eg<VAR>hμEg : μ Eg < ⊤<VAR>hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3<VAR>Ef : Set α<VAR>hmEf : MeasurableSet Ef<VAR>hμEf : μ Ef < ⊤<VAR>hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3<VAR>E : Set α := Ef ∪ Eg<VAR>hmE : MeasurableSet E<VAR>hfmE : μ E < ⊤<VAR>hgE' : Memℒp g p (μ.restrict E)<VAR>huiE : UnifIntegrable f p (μ.restrict E)<VAR>hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ffmE : Fact (μ E < ⊤)<VAR>hInner : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε<VAR>N : ℕ<VAR>hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3<VAR>n : ℕ<VAR>hn : n ≥ N<GOAL>eLpNorm (f n - g) p μ ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hfinε : ε ≠ ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε / 3<VAR>Eg : Set α<VAR>hmEg : MeasurableSet Eg<VAR>hμEg : μ Eg < ⊤<VAR>hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3<VAR>Ef : Set α<VAR>hmEf : MeasurableSet Ef<VAR>hμEf : μ Ef < ⊤<VAR>hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3<VAR>E : Set α := Ef ∪ Eg<VAR>hmE : MeasurableSet E<VAR>hfmE : μ E < ⊤<VAR>hgE' : Memℒp g p (μ.restrict E)<VAR>huiE : UnifIntegrable f p (μ.restrict E)<VAR>hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ffmE : Fact (μ E < ⊤)<VAR>hInner : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε<VAR>N : ℕ<VAR>hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3<VAR>n : ℕ<VAR>hn : n ≥ N<VAR>hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ<GOAL>eLpNorm (f n - g) p μ ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hfinε : ε ≠ ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε / 3<VAR>Eg : Set α<VAR>hmEg : MeasurableSet Eg<VAR>hμEg : μ Eg < ⊤<VAR>hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3<VAR>Ef : Set α<VAR>hmEf : MeasurableSet Ef<VAR>hμEf : μ Ef < ⊤<VAR>hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3<VAR>E : Set α := Ef ∪ Eg<VAR>hmE : MeasurableSet E<VAR>hfmE : μ E < ⊤<VAR>hgE' : Memℒp g p (μ.restrict E)<VAR>huiE : UnifIntegrable f p (μ.restrict E)<VAR>hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ffmE : Fact (μ E < ⊤)<VAR>hInner : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε<VAR>N : ℕ<VAR>hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3<VAR>n : ℕ<VAR>hn : n ≥ N<VAR>hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ<VAR>hfngEε : eLpNorm (E.indicator (f n - g)) p μ ≤ ε / 3<GOAL>eLpNorm (f n - g) p μ ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hfinε : ε ≠ ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε / 3<VAR>Eg : Set α<VAR>hmEg : MeasurableSet Eg<VAR>hμEg : μ Eg < ⊤<VAR>hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3<VAR>Ef : Set α<VAR>hmEf : MeasurableSet Ef<VAR>hμEf : μ Ef < ⊤<VAR>hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3<VAR>E : Set α := Ef ∪ Eg<VAR>hmE : MeasurableSet E<VAR>hfmE : μ E < ⊤<VAR>hgE' : Memℒp g p (μ.restrict E)<VAR>huiE : UnifIntegrable f p (μ.restrict E)<VAR>hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ffmE : Fact (μ E < ⊤)<VAR>hInner : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε<VAR>N : ℕ<VAR>hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3<VAR>n : ℕ<VAR>hn : n ≥ N<VAR>hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ<VAR>hfngEε : eLpNorm (E.indicator (f n - g)) p μ ≤ ε / 3<VAR>hmgEc : AEStronglyMeasurable (Eᶜ.indicator g) μ<GOAL>eLpNorm (f n - g) p μ ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hfinε : ε ≠ ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε / 3<VAR>Eg : Set α<VAR>hmEg : MeasurableSet Eg<VAR>hμEg : μ Eg < ⊤<VAR>hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3<VAR>Ef : Set α<VAR>hmEf : MeasurableSet Ef<VAR>hμEf : μ Ef < ⊤<VAR>hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3<VAR>E : Set α := Ef ∪ Eg<VAR>hmE : MeasurableSet E<VAR>hfmE : μ E < ⊤<VAR>hgE' : Memℒp g p (μ.restrict E)<VAR>huiE : UnifIntegrable f p (μ.restrict E)<VAR>hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ffmE : Fact (μ E < ⊤)<VAR>hInner : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε<VAR>N : ℕ<VAR>hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3<VAR>n : ℕ<VAR>hn : n ≥ N<VAR>hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ<VAR>hfngEε : eLpNorm (E.indicator (f n - g)) p μ ≤ ε / 3<VAR>hmgEc : AEStronglyMeasurable (Eᶜ.indicator g) μ<VAR>hgEcε : eLpNorm (Eᶜ.indicator g) p μ ≤ ε / 3<GOAL>eLpNorm (f n - g) p μ ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hfinε : ε ≠ ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε / 3<VAR>Eg : Set α<VAR>hmEg : MeasurableSet Eg<VAR>hμEg : μ Eg < ⊤<VAR>hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3<VAR>Ef : Set α<VAR>hmEf : MeasurableSet Ef<VAR>hμEf : μ Ef < ⊤<VAR>hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3<VAR>E : Set α := Ef ∪ Eg<VAR>hmE : MeasurableSet E<VAR>hfmE : μ E < ⊤<VAR>hgE' : Memℒp g p (μ.restrict E)<VAR>huiE : UnifIntegrable f p (μ.restrict E)<VAR>hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ffmE : Fact (μ E < ⊤)<VAR>hInner : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε<VAR>N : ℕ<VAR>hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3<VAR>n : ℕ<VAR>hn : n ≥ N<VAR>hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ<VAR>hfngEε : eLpNorm (E.indicator (f n - g)) p μ ≤ ε / 3<VAR>hmgEc : AEStronglyMeasurable (Eᶜ.indicator g) μ<VAR>hgEcε : eLpNorm (Eᶜ.indicator g) p μ ≤ ε / 3<VAR>hmfnEc : AEStronglyMeasurable (Eᶜ.indicator (f n)) μ<GOAL>eLpNorm (f n - g) p μ ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hfinε : ε ≠ ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε / 3<VAR>Eg : Set α<VAR>hmEg : MeasurableSet Eg<VAR>hμEg : μ Eg < ⊤<VAR>hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3<VAR>Ef : Set α<VAR>hmEf : MeasurableSet Ef<VAR>hμEf : μ Ef < ⊤<VAR>hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3<VAR>E : Set α := Ef ∪ Eg<VAR>hmE : MeasurableSet E<VAR>hfmE : μ E < ⊤<VAR>hgE' : Memℒp g p (μ.restrict E)<VAR>huiE : UnifIntegrable f p (μ.restrict E)<VAR>hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ffmE : Fact (μ E < ⊤)<VAR>hInner : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε<VAR>N : ℕ<VAR>hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3<VAR>n : ℕ<VAR>hn : n ≥ N<VAR>hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ<VAR>hfngEε : eLpNorm (E.indicator (f n - g)) p μ ≤ ε / 3<VAR>hmgEc : AEStronglyMeasurable (Eᶜ.indicator g) μ<VAR>hgEcε : eLpNorm (Eᶜ.indicator g) p μ ≤ ε / 3<VAR>hmfnEc : AEStronglyMeasurable (Eᶜ.indicator (f n)) μ<VAR>hfnEcε : eLpNorm (Eᶜ.indicator (f n)) p μ ≤ ε / 3<GOAL>eLpNorm (f n - g) p μ ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hfinε : ε ≠ ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε / 3<VAR>Eg : Set α<VAR>hmEg : MeasurableSet Eg<VAR>hμEg : μ Eg < ⊤<VAR>hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3<VAR>Ef : Set α<VAR>hmEf : MeasurableSet Ef<VAR>hμEf : μ Ef < ⊤<VAR>hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3<VAR>E : Set α := Ef ∪ Eg<VAR>hmE : MeasurableSet E<VAR>hfmE : μ E < ⊤<VAR>hgE' : Memℒp g p (μ.restrict E)<VAR>huiE : UnifIntegrable f p (μ.restrict E)<VAR>hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ffmE : Fact (μ E < ⊤)<VAR>hInner : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε<VAR>N : ℕ<VAR>hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3<VAR>n : ℕ<VAR>hn : n ≥ N<VAR>hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ<VAR>hfngEε : eLpNorm (E.indicator (f n - g)) p μ ≤ ε / 3<VAR>hmgEc : AEStronglyMeasurable (Eᶜ.indicator g) μ<VAR>hgEcε : eLpNorm (Eᶜ.indicator g) p μ ≤ ε / 3<VAR>hmfnEc : AEStronglyMeasurable (Eᶜ.indicator (f n)) μ<VAR>hfnEcε : eLpNorm (Eᶜ.indicator (f n)) p μ ≤ ε / 3<VAR>hmfngEc : AEStronglyMeasurable (Eᶜ.indicator (f n - g)) μ<GOAL>eLpNorm (f n - g) p μ ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hfinε : ε ≠ ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε / 3<VAR>Eg : Set α<VAR>hmEg : MeasurableSet Eg<VAR>hμEg : μ Eg < ⊤<VAR>hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3<VAR>Ef : Set α<VAR>hmEf : MeasurableSet Ef<VAR>hμEf : μ Ef < ⊤<VAR>hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3<VAR>E : Set α := Ef ∪ Eg<VAR>hmE : MeasurableSet E<VAR>hfmE : μ E < ⊤<VAR>hgE' : Memℒp g p (μ.restrict E)<VAR>huiE : UnifIntegrable f p (μ.restrict E)<VAR>hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ffmE : Fact (μ E < ⊤)<VAR>hInner : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε<VAR>N : ℕ<VAR>hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3<VAR>n : ℕ<VAR>hn : n ≥ N<VAR>hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ<VAR>hfngEε : eLpNorm (E.indicator (f n - g)) p μ ≤ ε / 3<VAR>hmgEc : AEStronglyMeasurable (Eᶜ.indicator g) μ<VAR>hgEcε : eLpNorm (Eᶜ.indicator g) p μ ≤ ε / 3<VAR>hmfnEc : AEStronglyMeasurable (Eᶜ.indicator (f n)) μ<VAR>hfnEcε : eLpNorm (Eᶜ.indicator (f n)) p μ ≤ ε / 3<VAR>hmfngEc : AEStronglyMeasurable (Eᶜ.indicator (f n - g)) μ<VAR>hfngEcε : eLpNorm (Eᶜ.indicator (f n - g)) p μ ≤ ε / 3 + ε / 3<GOAL>eLpNorm (f n - g) p μ ≤ ε
<VAR>x y : ℝ<GOAL>sinh (2 * x) = 2 * sinh x * cosh x
<VAR>x y : ℝ<GOAL>↑(sinh (2 * x)) = ↑(2 * sinh x * cosh x)