ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>n : ℕ<VAR>hn : 2 ≤ n + 1<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>r a C : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<VAR>hC : 0 ≤ C<VAR>hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n<VAR>I : ℝ := ‖↑i.symm‖<VAR>j : ℕ<VAR>a✝ : j ∈ Ico 2 (n + 1)<GOAL>‖(↑i.symm).compContinuousMultilinearMap (∑ c ∈ {c | 1 < c.length}.toFinset, p.compAlongComposition (p.rightInv i) c)‖ ≤ I * ∑ c ∈ {c | 1 < c.length}.toFinset, C * r ^ c.length * ∏ j_1 : Fin c.length, ‖p.rightInv i (c.blocksFun j_1)‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>hn : 2 ≤ n + 1<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>r a C : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<VAR>hC : 0 ≤ C<VAR>hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n<VAR>I : ℝ := ‖↑i.symm‖<VAR>j : ℕ<VAR>a✝ : j ∈ Ico 2 (n + 1)<GOAL>‖↑i.symm‖ * ‖∑ c ∈ {c | 1 < c.length}.toFinset, p.compAlongComposition (p.rightInv i) c‖ ≤ I * ∑ c ∈ {c | 1 < c.length}.toFinset, C * r ^ c.length * ∏ j_1 : Fin c.length, ‖p.rightInv i (c.blocksFun j_1)‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>hn : 2 ≤ n + 1<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>r a C : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<VAR>hC : 0 ≤ C<VAR>hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n<VAR>I : ℝ := ‖↑i.symm‖<VAR>j : ℕ<VAR>a✝ : j ∈ Ico 2 (n + 1)<GOAL>‖∑ c ∈ {c | 1 < c.length}.toFinset, p.compAlongComposition (p.rightInv i) c‖ ≤ ∑ c ∈ {c | 1 < c.length}.toFinset, C * r ^ c.length * ∏ j_1 : Fin c.length, ‖p.rightInv i (c.blocksFun j_1)‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>hn : 2 ≤ n + 1<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>r a C : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<VAR>hC : 0 ≤ C<VAR>hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n<VAR>I : ℝ := ‖↑i.symm‖<VAR>j : ℕ<VAR>a✝ : j ∈ Ico 2 (n + 1)<GOAL>∑ i_1 ∈ {c | 1 < c.length}.toFinset, ‖p.compAlongComposition (p.rightInv i) i_1‖ ≤ ∑ c ∈ {c | 1 < c.length}.toFinset, C * r ^ c.length * ∏ j_1 : Fin c.length, ‖p.rightInv i (c.blocksFun j_1)‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>hn : 2 ≤ n + 1<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>r a C : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<VAR>hC : 0 ≤ C<VAR>hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n<VAR>I : ℝ := ‖↑i.symm‖<VAR>j : ℕ<VAR>a✝¹ : j ∈ Ico 2 (n + 1)<VAR>i✝ : Composition j<VAR>a✝ : i✝ ∈ {c | 1 < c.length}.toFinset<GOAL>‖p.compAlongComposition (p.rightInv i) i✝‖ ≤ C * r ^ i✝.length * ∏ j_1 : Fin i✝.length, ‖p.rightInv i (i✝.blocksFun j_1)‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>hn : 2 ≤ n + 1<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>r a C : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<VAR>hC : 0 ≤ C<VAR>hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n<VAR>I : ℝ := ‖↑i.symm‖<VAR>j : ℕ<VAR>a✝¹ : j ∈ Ico 2 (n + 1)<VAR>i✝ : Composition j<VAR>a✝ : i✝ ∈ {c | 1 < c.length}.toFinset<GOAL>‖p i✝.length‖ * ∏ i_1 : Fin i✝.length, ‖p.rightInv i (i✝.blocksFun i_1)‖ ≤ C * r ^ i✝.length * ∏ j_1 : Fin i✝.length, ‖p.rightInv i (i✝.blocksFun j_1)‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>hn : 2 ≤ n + 1<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>r a C : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<VAR>hC : 0 ≤ C<VAR>hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n<VAR>I : ℝ := ‖↑i.symm‖<GOAL>a * ‖↑i.symm‖ + ∑ k ∈ Ico 2 (n + 1), a ^ k * (I * ∑ c ∈ {c | 1 < c.length}.toFinset, C * r ^ c.length * ∏ j : Fin c.length, ‖p.rightInv i (c.blocksFun j)‖) = I * a + I * C * ∑ k ∈ Ico 2 (n + 1), a ^ k * ∑ c ∈ {c | 1 < c.length}.toFinset, r ^ c.length * ∏ j : Fin c.length, ‖p.rightInv i (c.blocksFun j)‖
<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>n : ℕ<VAR>hn : 2 ≤ n + 1<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>r a C : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<VAR>hC : 0 ≤ C<VAR>hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n<VAR>I : ℝ := ‖↑i.symm‖<GOAL>‖↑i.symm‖ * a + ‖↑i.symm‖ * (C * ∑ i_1 ∈ Ico 2 (n + 1), a ^ i_1 * ∑ i_2 ∈ {c | 1 < c.length}.toFinset, r ^ i_2.length * ∏ j : Fin i_2.length, ‖p.rightInv i (i_2.blocksFun j)‖) = I * a + C * (I * ∑ k ∈ Ico 2 (n + 1), a ^ k * ∑ c ∈ {c | 1 < c.length}.toFinset, r ^ c.length * ∏ j : Fin c.length, ‖p.rightInv i (c.blocksFun j)‖)
<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>n : ℕ<VAR>hn : 2 ≤ n + 1<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>r a C : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<VAR>hC : 0 ≤ C<VAR>hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n<VAR>I : ℝ := ‖↑i.symm‖<GOAL>∑ k ∈ Ico 2 (n + 1), a ^ k * ∑ c ∈ {c | 1 < c.length}.toFinset, r ^ c.length * ∏ j : Fin c.length, ‖p.rightInv i (c.blocksFun j)‖ ≤ ∑ k ∈ Ico 2 (n + 1), (r * ∑ j ∈ Ico 1 n, a ^ j * ‖p.rightInv i j‖) ^ k
<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>n : ℕ<VAR>hn : 2 ≤ n + 1<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>r a C : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<VAR>hC : 0 ≤ C<VAR>hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n<VAR>I : ℝ := ‖↑i.symm‖<GOAL>∑ k ∈ Ico 2 (n + 1), a ^ k * ∑ c ∈ {c | 1 < c.length}.toFinset, r ^ c.length * ∏ j : Fin c.length, ‖p.rightInv i (c.blocksFun j)‖ ≤ ∑ x ∈ Ico 2 (n + 1), r ^ x * (∑ j ∈ Ico 1 n, a ^ j * ‖p.rightInv i j‖) ^ x
<VAR>α : Type u_1<VAR>inst✝⁶ : MeasurableSpace α<VAR>μ : Measure α<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>F✝ : H → α → E<VAR>x₀✝ : H<VAR>bound : α → ℝ<VAR>ε : ℝ<VAR>F : 𝕜 → α → E<VAR>x₀ : 𝕜<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ<VAR>hF_int : Integrable (F x₀) μ<VAR>F' : 𝕜 → α → E<VAR>hF'_meas : AEStronglyMeasurable (F' x₀) μ<VAR>h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F' x a‖ ≤ bound a<VAR>bound_integrable : Integrable bound μ<VAR>h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, HasDerivAt (fun x => F x a) (F' x a) x<GOAL>Integrable (F' x₀) μ ∧ HasDerivAt (fun n => ∫ (a : α), F n a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀
<VAR>α : Type u_1<VAR>inst✝⁶ : MeasurableSpace α<VAR>μ : Measure α<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>F✝ : H → α → E<VAR>x₀✝ : H<VAR>bound : α → ℝ<VAR>ε : ℝ<VAR>F : 𝕜 → α → E<VAR>x₀ : 𝕜<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ<VAR>hF_int : Integrable (F x₀) μ<VAR>F' : 𝕜 → α → E<VAR>hF'_meas : AEStronglyMeasurable (F' x₀) μ<VAR>h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F' x a‖ ≤ bound a<VAR>bound_integrable : Integrable bound μ<VAR>h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, HasDerivAt (fun x => F x a) (F' x a) x<VAR>x₀_in : x₀ ∈ ball x₀ ε<GOAL>Integrable (F' x₀) μ ∧ HasDerivAt (fun n => ∫ (a : α), F n a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀
<VAR>α : Type u_1<VAR>inst✝⁶ : MeasurableSpace α<VAR>μ : Measure α<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>F✝ : H → α → E<VAR>x₀✝ : H<VAR>bound : α → ℝ<VAR>ε : ℝ<VAR>F : 𝕜 → α → E<VAR>x₀ : 𝕜<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ<VAR>hF_int : Integrable (F x₀) μ<VAR>F' : 𝕜 → α → E<VAR>hF'_meas : AEStronglyMeasurable (F' x₀) μ<VAR>h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F' x a‖ ≤ bound a<VAR>bound_integrable : Integrable bound μ<VAR>h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, HasDerivAt (fun x => F x a) (F' x a) x<VAR>x₀_in : x₀ ∈ ball x₀ ε<VAR>diff_x₀ : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun x => F x a) (F' x₀ a) x₀<GOAL>Integrable (F' x₀) μ ∧ HasDerivAt (fun n => ∫ (a : α), F n a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀
<VAR>α : Type u_1<VAR>inst✝⁶ : MeasurableSpace α<VAR>μ : Measure α<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>F✝ : H → α → E<VAR>x₀✝ : H<VAR>bound : α → ℝ<VAR>ε : ℝ<VAR>F : 𝕜 → α → E<VAR>x₀ : 𝕜<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ<VAR>hF_int : Integrable (F x₀) μ<VAR>F' : 𝕜 → α → E<VAR>hF'_meas : AEStronglyMeasurable (F' x₀) μ<VAR>h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F' x a‖ ≤ bound a<VAR>bound_integrable : Integrable bound μ<VAR>h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, HasDerivAt (fun x => F x a) (F' x a) x<VAR>x₀_in : x₀ ∈ ball x₀ ε<VAR>diff_x₀ : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun x => F x a) (F' x₀ a) x₀<VAR>this : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) (ball x₀ ε)<GOAL>Integrable (F' x₀) μ ∧ HasDerivAt (fun n => ∫ (a : α), F n a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{?u.124213, u_1} C<VAR>inst✝² : Category.{?u.124217, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S✝ : ShortComplex C<VAR>S : ShortComplex Cᵒᵖ<VAR>h : S.Splitting<GOAL>(h.s.unop ≫ S.unop.f + S.unop.g ≫ h.r.unop).op = (𝟙 S.unop.X₂).op
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{?u.124213, u_1} C<VAR>inst✝² : Category.{?u.124217, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S✝ : ShortComplex C<VAR>S : ShortComplex Cᵒᵖ<VAR>h : S.Splitting<GOAL>S.g ≫ h.s + h.r ≫ S.f = h.r ≫ S.f + S.g ≫ h.s
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>J : Type u_4<VAR>inst✝² : Category.{u_5, u_1} C<VAR>inst✝¹ : Category.{?u.7315, u_2} D<VAR>inst✝ : Category.{?u.7319, u_3} E<VAR>X Y : GradedObject J C<VAR>e : X ≅ Y<VAR>j : J<GOAL>e.inv j ≫ e.hom j = 𝟙 (Y j)
<VAR>n m : Nat<VAR>h : m < (range n).length<GOAL>(range n)[m] = m
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>v : n → α<GOAL>(diagonal v)⁻¹ = diagonal (Ring.inverse v)
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>v : n → α<GOAL>Ring.inverse (diagonal v) = diagonal (Ring.inverse v)
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : CompleteSpace E<VAR>ι : Type u_3<VAR>inst✝¹⁰ : LinearOrder ι<VAR>inst✝⁹ : LocallyFiniteOrder ι<VAR>inst✝⁸ : OrderBot ι<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : DiscreteTopology ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : BorelSpace ι<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : SecondCountableTopology E<VAR>ℱ : Filtration ι m<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>i n : ι<VAR>h : Martingale f ℱ μ<VAR>hτ : IsStoppingTime ℱ τ<VAR>hσ : IsStoppingTime ℱ σ<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<GOAL>μ[stoppedValue f τ|hσ.measurableSpace] =ᶠ[ae (μ.restrict {x | τ x ≤ σ x})] stoppedValue f τ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : CompleteSpace E<VAR>ι : Type u_3<VAR>inst✝¹⁰ : LinearOrder ι<VAR>inst✝⁹ : LocallyFiniteOrder ι<VAR>inst✝⁸ : OrderBot ι<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : DiscreteTopology ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : BorelSpace ι<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : SecondCountableTopology E<VAR>ℱ : Filtration ι m<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>i n : ι<VAR>h : Martingale f ℱ μ<VAR>hτ : IsStoppingTime ℱ τ<VAR>hσ : IsStoppingTime ℱ σ<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<GOAL>{ω | τ ω ≤ σ ω}.indicator (μ[stoppedValue f τ|hσ.measurableSpace]) =ᶠ[ae μ] {ω | τ ω ≤ σ ω}.indicator (stoppedValue f τ)
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : CompleteSpace E<VAR>ι : Type u_3<VAR>inst✝¹⁰ : LinearOrder ι<VAR>inst✝⁹ : LocallyFiniteOrder ι<VAR>inst✝⁸ : OrderBot ι<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : DiscreteTopology ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : BorelSpace ι<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : SecondCountableTopology E<VAR>ℱ : Filtration ι m<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>i n : ι<VAR>h : Martingale f ℱ μ<VAR>hτ : IsStoppingTime ℱ τ<VAR>hσ : IsStoppingTime ℱ σ<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<GOAL>μ[{ω | τ ω ≤ σ ω}.indicator (stoppedValue f τ)|hσ.measurableSpace] =ᶠ[ae μ] {ω | τ ω ≤ σ ω}.indicator (stoppedValue f τ)
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : CompleteSpace E<VAR>ι : Type u_3<VAR>inst✝¹⁰ : LinearOrder ι<VAR>inst✝⁹ : LocallyFiniteOrder ι<VAR>inst✝⁸ : OrderBot ι<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : DiscreteTopology ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : BorelSpace ι<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : SecondCountableTopology E<VAR>ℱ : Filtration ι m<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>i n : ι<VAR>h : Martingale f ℱ μ<VAR>hτ : IsStoppingTime ℱ τ<VAR>hσ : IsStoppingTime ℱ σ<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<VAR>h_int : Integrable ({ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n => f n) τ)) μ<GOAL>μ[{ω | τ ω ≤ σ ω}.indicator (stoppedValue f τ)|hσ.measurableSpace] =ᶠ[ae μ] {ω | τ ω ≤ σ ω}.indicator (stoppedValue f τ)
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : CompleteSpace E<VAR>ι : Type u_3<VAR>inst✝¹⁰ : LinearOrder ι<VAR>inst✝⁹ : LocallyFiniteOrder ι<VAR>inst✝⁸ : OrderBot ι<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : DiscreteTopology ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : BorelSpace ι<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : SecondCountableTopology E<VAR>ℱ : Filtration ι m<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>i n : ι<VAR>h : Martingale f ℱ μ<VAR>hτ : IsStoppingTime ℱ τ<VAR>hσ : IsStoppingTime ℱ σ<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<VAR>h_int : Integrable ({ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n => f n) τ)) μ<VAR>h_meas : AEStronglyMeasurable' hσ.measurableSpace ({ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n => f n) τ)) μ<GOAL>μ[{ω | τ ω ≤ σ ω}.indicator (stoppedValue f τ)|hσ.measurableSpace] =ᶠ[ae μ] {ω | τ ω ≤ σ ω}.indicator (stoppedValue f τ)
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>(o.oangle x y).cos = ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖)
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>(o.oangle x y).cos = ‖x‖ * ‖y‖ * (o.oangle x y).cos / (‖x‖ * ‖y‖)
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>d : l.Nodup<GOAL>a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : TopologicalSpace α<VAR>ι : Sort u_5<VAR>inst✝ : Finite ι<VAR>s : ι → Set α<VAR>a : α<GOAL>𝓝[⋃ i, s i] a = ⨆ i, 𝓝[s i] a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n✝ : ℕ<VAR>hm : IsPeriodicPt f m x<VAR>n : ℕ<GOAL>IsPeriodicPt f (m * n) x
<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 G<VAR>hf : Continuous ⇑f<GOAL>∃ C, 0 < C ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
<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 G<VAR>hf : Continuous ⇑f<VAR>h✝ : IsEmpty ι<GOAL>∃ C, 0 < C ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
<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 G<VAR>hf : Continuous ⇑f<VAR>h✝ : Nonempty ι<GOAL>∃ C, 0 < C ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
<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 G<VAR>hf : Continuous ⇑f<VAR>h✝ : Nonempty ι<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>hε : ∀ (m : (i : ι) → E i), ‖m - 0‖ < ε → ‖f m - f 0‖ < 1<GOAL>∃ C, 0 < C ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
<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 G<VAR>hf : Continuous ⇑f<VAR>h✝ : Nonempty ι<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>hε : ∀ (m : (i : ι) → E i), ‖m‖ < ε → ‖f m‖ < 1<GOAL>∃ C, 0 < C ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
<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 G<VAR>hf : Continuous ⇑f<VAR>h✝ : Nonempty ι<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>hε : ∀ (m : (i : ι) → E i), ‖m‖ < ε → ‖f m‖ < 1<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<GOAL>∃ C, 0 < C ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
<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 G<VAR>hf : Continuous ⇑f<VAR>h✝ : Nonempty ι<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>hε : ∀ (m : (i : ι) → E i), ‖m‖ < ε → ‖f m‖ < 1<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>this : 0 < (‖c‖ / ε) ^ Fintype.card ι<GOAL>∃ C, 0 < C ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖