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>p : ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<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>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>h : ε < ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε.toReal / 3<VAR>hdivp : 0 ≤ 1 / p.toReal<VAR>hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)<VAR>δ₁ : ℝ<VAR>hδ₁ : 0 < δ₁<VAR>heLpNorm₁ : ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>δ₂ : ℝ<VAR>hδ₂ : 0 < δ₂<VAR>heLpNorm₂ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>t : Set α<VAR>htm : MeasurableSet t<VAR>ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)<VAR>ht₂ : TendstoUniformlyOn f g atTop tᶜ<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>p : ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<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>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>h : ε < ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε.toReal / 3<VAR>hdivp : 0 ≤ 1 / p.toReal<VAR>hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)<VAR>δ₁ : ℝ<VAR>hδ₁ : 0 < δ₁<VAR>heLpNorm₁ : ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>δ₂ : ℝ<VAR>hδ₂ : 0 < δ₂<VAR>heLpNorm₂ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>t : Set α<VAR>htm : MeasurableSet t<VAR>ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)<VAR>ht₂ : ∀ ε > 0, ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ tᶜ, dist (g x) (f n 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>p : ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<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>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>h : ε < ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε.toReal / 3<VAR>hdivp : 0 ≤ 1 / p.toReal<VAR>hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)<VAR>δ₁ : ℝ<VAR>hδ₁ : 0 < δ₁<VAR>heLpNorm₁ : ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>δ₂ : ℝ<VAR>hδ₂ : 0 < δ₂<VAR>heLpNorm₂ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>t : Set α<VAR>htm : MeasurableSet t<VAR>ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)<VAR>ht₂ : ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ tᶜ, dist (g x) (f n x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))<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>p : ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<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>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>h : ε < ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε.toReal / 3<VAR>hdivp : 0 ≤ 1 / p.toReal<VAR>hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)<VAR>δ₁ : ℝ<VAR>hδ₁ : 0 < δ₁<VAR>heLpNorm₁ : ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>δ₂ : ℝ<VAR>hδ₂ : 0 < δ₂<VAR>heLpNorm₂ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>t : Set α<VAR>htm : MeasurableSet t<VAR>ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)<VAR>ht₂ : ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ tᶜ, dist (g x) (f n x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))<VAR>N : ℕ<VAR>hN : ∀ b ≥ N, ∀ x ∈ tᶜ, dist (g x) (f b x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))<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>p : ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<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>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>h : ε < ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε.toReal / 3<VAR>hdivp : 0 ≤ 1 / p.toReal<VAR>hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)<VAR>δ₁ : ℝ<VAR>hδ₁ : 0 < δ₁<VAR>heLpNorm₁ : ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>δ₂ : ℝ<VAR>hδ₂ : 0 < δ₂<VAR>heLpNorm₂ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>t : Set α<VAR>htm : MeasurableSet t<VAR>ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)<VAR>N : ℕ<VAR>hN : ∀ b ≥ N, ∀ x ∈ tᶜ, dist (g x) (f b x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))<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>p : ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<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>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>h : ε < ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε.toReal / 3<VAR>hdivp : 0 ≤ 1 / p.toReal<VAR>hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)<VAR>δ₁ : ℝ<VAR>hδ₁ : 0 < δ₁<VAR>heLpNorm₁ : ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>δ₂ : ℝ<VAR>hδ₂ : 0 < δ₂<VAR>heLpNorm₂ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>t : Set α<VAR>htm : MeasurableSet t<VAR>ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)<VAR>N : ℕ<VAR>hN : ∀ b ≥ N, ∀ x ∈ tᶜ, dist (g x) (f b x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))<VAR>n : ℕ<VAR>hn : n ≥ N<GOAL>eLpNorm (t.indicator (f n - g) + tᶜ.indicator (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>p : ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<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>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>h : ε < ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε.toReal / 3<VAR>hdivp : 0 ≤ 1 / p.toReal<VAR>hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)<VAR>δ₁ : ℝ<VAR>hδ₁ : 0 < δ₁<VAR>heLpNorm₁ : ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>δ₂ : ℝ<VAR>hδ₂ : 0 < δ₂<VAR>heLpNorm₂ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>t : Set α<VAR>htm : MeasurableSet t<VAR>ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)<VAR>N : ℕ<VAR>hN : ∀ b ≥ N, ∀ x ∈ tᶜ, dist (g x) (f b x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))<VAR>n : ℕ<VAR>hn : n ≥ N<GOAL>eLpNorm (t.indicator (f n - g)) p μ + eLpNorm (tᶜ.indicator (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>p : ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<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>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>h : ε < ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε.toReal / 3<VAR>hdivp : 0 ≤ 1 / p.toReal<VAR>hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)<VAR>δ₁ : ℝ<VAR>hδ₁ : 0 < δ₁<VAR>heLpNorm₁ : ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>δ₂ : ℝ<VAR>hδ₂ : 0 < δ₂<VAR>heLpNorm₂ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>t : Set α<VAR>htm : MeasurableSet t<VAR>ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)<VAR>N : ℕ<VAR>hN : ∀ b ≥ N, ∀ x ∈ tᶜ, dist (g x) (f b x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))<VAR>n : ℕ<VAR>hn : n ≥ N<GOAL>eLpNorm (t.indicator (f n) + -t.indicator g) p μ + eLpNorm (tᶜ.indicator (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>p : ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<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>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>h : ε < ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε.toReal / 3<VAR>hdivp : 0 ≤ 1 / p.toReal<VAR>hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)<VAR>δ₁ : ℝ<VAR>hδ₁ : 0 < δ₁<VAR>heLpNorm₁ : ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>δ₂ : ℝ<VAR>hδ₂ : 0 < δ₂<VAR>heLpNorm₂ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>t : Set α<VAR>htm : MeasurableSet t<VAR>ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)<VAR>N : ℕ<VAR>hN : ∀ b ≥ N, ∀ x ∈ tᶜ, dist (g x) (f b x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))<VAR>n : ℕ<VAR>hn : n ≥ N<GOAL>eLpNorm (t.indicator (f n)) p μ + eLpNorm (-t.indicator g) p μ + eLpNorm (tᶜ.indicator (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>p : ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<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>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>h : ε < ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε.toReal / 3<VAR>hdivp : 0 ≤ 1 / p.toReal<VAR>hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)<VAR>δ₁ : ℝ<VAR>hδ₁ : 0 < δ₁<VAR>heLpNorm₁ : ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>δ₂ : ℝ<VAR>hδ₂ : 0 < δ₂<VAR>heLpNorm₂ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>t : Set α<VAR>htm : MeasurableSet t<VAR>ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)<VAR>N : ℕ<VAR>hN : ∀ b ≥ N, ∀ x ∈ tᶜ, dist (g x) (f b x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))<VAR>n : ℕ<VAR>hn : n ≥ N<VAR>hnf : eLpNorm (t.indicator (f n)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<GOAL>eLpNorm (t.indicator (f n)) p μ + eLpNorm (-t.indicator g) p μ + eLpNorm (tᶜ.indicator (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>p : ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<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>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>h : ε < ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε.toReal / 3<VAR>hdivp : 0 ≤ 1 / p.toReal<VAR>hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)<VAR>δ₁ : ℝ<VAR>hδ₁ : 0 < δ₁<VAR>heLpNorm₁ : ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>δ₂ : ℝ<VAR>hδ₂ : 0 < δ₂<VAR>heLpNorm₂ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>t : Set α<VAR>htm : MeasurableSet t<VAR>ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)<VAR>N : ℕ<VAR>hN : ∀ b ≥ N, ∀ x ∈ tᶜ, dist (g x) (f b x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))<VAR>n : ℕ<VAR>hn : n ≥ N<VAR>hnf : eLpNorm (t.indicator (f n)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>hng : eLpNorm (t.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<GOAL>eLpNorm (t.indicator (f n)) p μ + eLpNorm (-t.indicator g) p μ + eLpNorm (tᶜ.indicator (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>p : ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<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>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>h : ε < ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε.toReal / 3<VAR>hdivp : 0 ≤ 1 / p.toReal<VAR>hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)<VAR>δ₁ : ℝ<VAR>hδ₁ : 0 < δ₁<VAR>heLpNorm₁ : ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>δ₂ : ℝ<VAR>hδ₂ : 0 < δ₂<VAR>heLpNorm₂ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>t : Set α<VAR>htm : MeasurableSet t<VAR>ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)<VAR>N : ℕ<VAR>hN : ∀ b ≥ N, ∀ x ∈ tᶜ, dist (g x) (f b x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))<VAR>n : ℕ<VAR>hn : n ≥ N<VAR>hnf : eLpNorm (t.indicator (f n)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>hng : eLpNorm (t.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>hlt : eLpNorm (tᶜ.indicator (f n - g)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<GOAL>eLpNorm (t.indicator (f n)) p μ + eLpNorm (-t.indicator g) p μ + eLpNorm (tᶜ.indicator (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>p : ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<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>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>h : ε < ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε.toReal / 3<VAR>hdivp : 0 ≤ 1 / p.toReal<VAR>hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)<VAR>δ₁ : ℝ<VAR>hδ₁ : 0 < δ₁<VAR>heLpNorm₁ : ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>δ₂ : ℝ<VAR>hδ₂ : 0 < δ₂<VAR>heLpNorm₂ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>t : Set α<VAR>htm : MeasurableSet t<VAR>ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)<VAR>N : ℕ<VAR>hN : ∀ b ≥ N, ∀ x ∈ tᶜ, dist (g x) (f b x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))<VAR>n : ℕ<VAR>hn : n ≥ N<VAR>hnf : eLpNorm (t.indicator (f n)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>hng : eLpNorm (t.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>hlt : eLpNorm (tᶜ.indicator (f n - g)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>this : ENNReal.ofReal (ε.toReal / 3) = ε / 3<GOAL>eLpNorm (t.indicator (f n)) p μ + eLpNorm (-t.indicator g) p μ + eLpNorm (tᶜ.indicator (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>p : ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<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>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>h : ε < ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε.toReal / 3<VAR>hdivp : 0 ≤ 1 / p.toReal<VAR>hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)<VAR>δ₁ : ℝ<VAR>hδ₁ : 0 < δ₁<VAR>heLpNorm₁ : ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>δ₂ : ℝ<VAR>hδ₂ : 0 < δ₂<VAR>heLpNorm₂ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>t : Set α<VAR>htm : MeasurableSet t<VAR>ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)<VAR>N : ℕ<VAR>hN : ∀ b ≥ N, ∀ x ∈ tᶜ, dist (g x) (f b x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))<VAR>n : ℕ<VAR>hn : n ≥ N<VAR>hnf : eLpNorm (t.indicator (f n)) p μ ≤ ε / 3<VAR>hng : eLpNorm (t.indicator g) p μ ≤ ε / 3<VAR>hlt : eLpNorm (tᶜ.indicator (f n - g)) p μ ≤ ε / 3<VAR>this : ENNReal.ofReal (ε.toReal / 3) = ε / 3<GOAL>eLpNorm (t.indicator (f n)) p μ + eLpNorm (-t.indicator g) p μ + eLpNorm (tᶜ.indicator (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>p : ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<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>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>h : ε < ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε.toReal / 3<VAR>hdivp : 0 ≤ 1 / p.toReal<VAR>hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)<VAR>δ₁ : ℝ<VAR>hδ₁ : 0 < δ₁<VAR>heLpNorm₁ : ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>δ₂ : ℝ<VAR>hδ₂ : 0 < δ₂<VAR>heLpNorm₂ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)<VAR>t : Set α<VAR>htm : MeasurableSet t<VAR>ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)<VAR>N : ℕ<VAR>hN : ∀ b ≥ N, ∀ x ∈ tᶜ, dist (g x) (f b x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))<VAR>n : ℕ<VAR>hn : n ≥ N<VAR>hnf : eLpNorm (t.indicator (f n)) p μ ≤ ε / 3<VAR>hng : eLpNorm (t.indicator g) p μ ≤ ε / 3<VAR>hlt : eLpNorm (tᶜ.indicator (f n - g)) p μ ≤ ε / 3<VAR>this : ENNReal.ofReal (ε.toReal / 3) = ε / 3<GOAL>eLpNorm (t.indicator (f n)) p μ + eLpNorm (t.indicator g) p μ + eLpNorm (tᶜ.indicator (f n - g)) p μ ≤ ε / 3 + ε / 3 + ε / 3
<VAR>α : Type u_1<VAR>inst✝² : Zero α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : DecidableRel fun x x_1 => x < x_1<VAR>a : α<GOAL>sign a = 1 ↔ 0 < a
<VAR>α : Type u_1<VAR>inst✝² : Zero α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : DecidableRel fun x x_1 => x < x_1<VAR>a : α<VAR>h : sign a = 1<GOAL>0 < a
<VAR>α : Type u_1<VAR>inst✝² : Zero α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : DecidableRel fun x x_1 => x < x_1<VAR>a : α<VAR>h : sign a = 1<VAR>hn : ¬0 < a<GOAL>False
<VAR>α : Type u_1<VAR>inst✝² : Zero α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : DecidableRel fun x x_1 => x < x_1<VAR>a : α<VAR>h : (if a < 0 then -1 else 0) = 1<VAR>hn : ¬0 < a<GOAL>False
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>n : ℕ<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁴ : Fintype ι<VAR>inst✝¹³ : Fintype ι'<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁹ : (i : ι) → NormedAddCommGroup (E₁ i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁷ : (i : ι') → NormedAddCommGroup (E' i)<VAR>inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁵ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>inst✝⁴ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei i.succ) G<VAR>m : (i : Fin n.succ) → Ei i<GOAL>‖f‖ * (‖m 0‖ * ∏ i : Fin n, ‖tail m i‖) = ‖f‖ * ∏ i : Fin n.succ, ‖m i‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>n : ℕ<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁴ : Fintype ι<VAR>inst✝¹³ : Fintype ι'<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁹ : (i : ι) → NormedAddCommGroup (E₁ i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁷ : (i : ι') → NormedAddCommGroup (E' i)<VAR>inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁵ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>inst✝⁴ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei i.succ) G<VAR>m : (i : Fin n.succ) → Ei i<GOAL>‖f‖ * (‖m 0‖ * ∏ i : Fin n, ‖tail m i‖) = ‖f‖ * (‖m 0‖ * ∏ i : Fin n, ‖m i.succ‖)
<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>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>inst✝ : CompleteSpace F<GOAL>Measurable (fderiv 𝕜 f)
<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>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>inst✝ : CompleteSpace F<VAR>s : Set (E →L[𝕜] F)<VAR>hs : IsClosed s<GOAL>MeasurableSet (fderiv 𝕜 f ⁻¹' s)
<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>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>inst✝ : CompleteSpace F<VAR>s : Set (E →L[𝕜] F)<VAR>hs : IsClosed s<VAR>this : fderiv 𝕜 f ⁻¹' s = {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s} ∪ {x | ¬DifferentiableAt 𝕜 f x} ∩ {_x | 0 ∈ s}<GOAL>MeasurableSet (fderiv 𝕜 f ⁻¹' s)
<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>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>inst✝ : CompleteSpace F<VAR>s : Set (E →L[𝕜] F)<VAR>hs : IsClosed s<VAR>this : fderiv 𝕜 f ⁻¹' s = {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s} ∪ {x | ¬DifferentiableAt 𝕜 f x} ∩ {_x | 0 ∈ s}<GOAL>MeasurableSet ({x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s} ∪ {x | ¬DifferentiableAt 𝕜 f x} ∩ {_x | 0 ∈ s})
<VAR>a b : ℕ+<VAR>h : a < b<GOAL>↑(a + (b - a)) = ↑b
<VAR>a b : ℕ+<VAR>h : a < b<GOAL>↑a + (↑b - ↑a) = ↑b