ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f✝ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f f' : ℝ → E<VAR>hcont : ContinuousOn g (Icc a b)<VAR>hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x<VAR>g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x<VAR>hab : a < b<GOAL>IntegrableOn g' (Ioc a b) volume
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f✝ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f f' : ℝ → E<VAR>hcont : ContinuousOn g (Icc a b)<VAR>hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x<VAR>g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x<VAR>hab : a < b<GOAL>IntegrableOn g' (Ioo a b) volume
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f✝ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f f' : ℝ → E<VAR>hcont : ContinuousOn g (Icc a b)<VAR>hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x<VAR>g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x<VAR>hab : a < b<VAR>meas_g' : AEMeasurable g' (volume.restrict (Ioo a b))<GOAL>IntegrableOn g' (Ioo a b) volume
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f✝ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f f' : ℝ → E<VAR>hcont : ContinuousOn g (Icc a b)<VAR>hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x<VAR>g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x<VAR>hab : a < b<VAR>meas_g' : AEMeasurable g' (volume.restrict (Ioo a b))<GOAL>∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊ ≤ ENNReal.ofReal (g b - g a)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f✝ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f f' : ℝ → E<VAR>hcont : ContinuousOn g (Icc a b)<VAR>hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x<VAR>g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x<VAR>hab : a < b<VAR>meas_g' : AEMeasurable g' (volume.restrict (Ioo a b))<VAR>H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊<GOAL>False
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f✝¹ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f✝ f' : ℝ → E<VAR>hcont : ContinuousOn g (Icc a b)<VAR>hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x<VAR>g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x<VAR>hab : a < b<VAR>meas_g' : AEMeasurable g' (volume.restrict (Ioo a b))<VAR>H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊<VAR>f : SimpleFunc ℝ ℝ≥0<VAR>fle : ∀ (x : ℝ), ↑f x ≤ ‖g' x‖₊<VAR>fint : ∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x) < ⊤<VAR>hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)<GOAL>False
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F✝ : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f✝¹ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f✝ f' : ℝ → E<VAR>hcont : ContinuousOn g (Icc a b)<VAR>hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x<VAR>g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x<VAR>hab : a < b<VAR>meas_g' : AEMeasurable g' (volume.restrict (Ioo a b))<VAR>H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊<VAR>f : SimpleFunc ℝ ℝ≥0<VAR>fle : ∀ (x : ℝ), ↑f x ≤ ‖g' x‖₊<VAR>fint : ∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x) < ⊤<VAR>hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)<VAR>F : ℝ → ℝ := NNReal.toReal ∘ ↑f<GOAL>False
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F✝ : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f✝¹ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f✝ f' : ℝ → E<VAR>hcont : ContinuousOn g (Icc a b)<VAR>hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x<VAR>g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x<VAR>hab : a < b<VAR>meas_g' : AEMeasurable g' (volume.restrict (Ioo a b))<VAR>H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊<VAR>f : SimpleFunc ℝ ℝ≥0<VAR>fle : ∀ (x : ℝ), ↑f x ≤ ‖g' x‖₊<VAR>fint : ∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x) < ⊤<VAR>hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)<VAR>F : ℝ → ℝ := NNReal.toReal ∘ ↑f<VAR>intF : IntegrableOn F (Ioo a b) volume<GOAL>False
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F✝ : Type u_4<VAR>A✝ : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f✝¹ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f✝ f' : ℝ → E<VAR>hcont : ContinuousOn g (Icc a b)<VAR>hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x<VAR>g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x<VAR>hab : a < b<VAR>meas_g' : AEMeasurable g' (volume.restrict (Ioo a b))<VAR>H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊<VAR>f : SimpleFunc ℝ ℝ≥0<VAR>fle : ∀ (x : ℝ), ↑f x ≤ ‖g' x‖₊<VAR>fint : ∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x) < ⊤<VAR>hf : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x)<VAR>F : ℝ → ℝ := NNReal.toReal ∘ ↑f<VAR>intF : IntegrableOn F (Ioo a b) volume<VAR>A : ∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x) = ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)<GOAL>False
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F✝ : Type u_4<VAR>A✝ : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f✝¹ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f✝ f' : ℝ → E<VAR>hcont : ContinuousOn g (Icc a b)<VAR>hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x<VAR>g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x<VAR>hab : a < b<VAR>meas_g' : AEMeasurable g' (volume.restrict (Ioo a b))<VAR>H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊<VAR>f : SimpleFunc ℝ ℝ≥0<VAR>fle : ∀ (x : ℝ), ↑f x ≤ ‖g' x‖₊<VAR>fint : ∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x) < ⊤<VAR>F : ℝ → ℝ := NNReal.toReal ∘ ↑f<VAR>hf : ENNReal.ofReal (g b - g a) < ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)<VAR>intF : IntegrableOn F (Ioo a b) volume<VAR>A : ∫⁻ (x : ℝ) in Ioo a b, ↑(↑f x) = ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)<VAR>B : ∫ (x : ℝ) in Ioo a b, F x ≤ g b - g a<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>M✝ N✝ M : Matroid α<VAR>N : Matroid β<VAR>I X : Set (α ⊕ β)<GOAL>(M.sum N).Basis I X ↔ M.Basis (Sum.inl ⁻¹' I) (Sum.inl ⁻¹' X) ∧ N.Basis (Sum.inr ⁻¹' I) (Sum.inr ⁻¹' X)
<VAR>α : Type u<VAR>β : Type v<VAR>M✝ N✝ M : Matroid α<VAR>N : Matroid β<VAR>I X : Set (α ⊕ β)<GOAL>M.Basis ((fun a => a.down) '' (Sigma.mk false ⁻¹' ((fun s => Sum.elim (fun x => ⟨false, x⟩) (fun x => ⟨true, x⟩) s) '' ((fun a => Sum.map (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) a) '' I)))) ((fun a => a.down) '' (Sigma.mk false ⁻¹' ((fun s => Sum.elim (fun x => ⟨false, x⟩) (fun x => ⟨true, x⟩) s) '' ((fun a => Sum.map (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) a) '' X)))) ∧ N.Basis ((fun a => a.down) '' (Sigma.mk true ⁻¹' ((fun s => Sum.elim (fun x => ⟨false, x⟩) (fun x => ⟨true, x⟩) s) '' ((fun a => Sum.map (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) a) '' I)))) ((fun a => a.down) '' (Sigma.mk true ⁻¹' ((fun s => Sum.elim (fun x => ⟨false, x⟩) (fun x => ⟨true, x⟩) s) '' ((fun a => Sum.map (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) a) '' X)))) ↔ M.Basis (Sum.inl ⁻¹' I) (Sum.inl ⁻¹' X) ∧ N.Basis (Sum.inr ⁻¹' I) (Sum.inr ⁻¹' X)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDF f κ ν<VAR>a : α<GOAL>∀ᵐ (b : β) ∂ν a, Tendsto (f (a, b)) atTop (𝓝 1)
<VAR>A : Type u_1<VAR>inst✝⁶ : NonUnitalRing A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Module ℝ A<VAR>inst✝² : IsScalarTower ℝ A A<VAR>inst✝¹ : SMulCommClass ℝ A A<VAR>inst✝ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>a : A<VAR>ha₁ : IsSelfAdjoint a<VAR>ha₂ : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal<GOAL>∃ x, IsSelfAdjoint x ∧ QuasispectrumRestricts x ⇑ContinuousMap.realToNNReal ∧ x * x = a
<VAR>A : Type u_1<VAR>inst✝⁶ : NonUnitalRing A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Module ℝ A<VAR>inst✝² : IsScalarTower ℝ A A<VAR>inst✝¹ : SMulCommClass ℝ A A<VAR>inst✝ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>a : A<VAR>ha₁ : IsSelfAdjoint a<VAR>ha₂ : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal<GOAL>QuasispectrumRestricts (cfcₙ Real.sqrt a) ⇑ContinuousMap.realToNNReal ∧ cfcₙ Real.sqrt a * cfcₙ Real.sqrt a = a
<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>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hf : HasStrictFDerivAt f f' x<VAR>hg : HasStrictFDerivAt g g' x<GOAL>HasStrictFDerivAt (fun x => f x - g x) (f' - g') x
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω<VAR>hf : Adapted ℱ f<VAR>hint : ∀ (n : ℕ), Integrable (f n) μ<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R<GOAL>∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop atTop ↔ Tendsto (fun n => predictablePart f ℱ μ n ω) atTop atTop
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω<VAR>hf : Adapted ℱ f<VAR>hint : ∀ (n : ℕ), Integrable (f n) μ<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R<VAR>h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop<GOAL>∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop atTop ↔ Tendsto (fun n => predictablePart f ℱ μ n ω) atTop atTop
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω<VAR>hf : Adapted ℱ f<VAR>hint : ∀ (n : ℕ), Integrable (f n) μ<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R<VAR>h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop<VAR>h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot<GOAL>∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop atTop ↔ Tendsto (fun n => predictablePart f ℱ μ n ω) atTop atTop
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω<VAR>hf : Adapted ℱ f<VAR>hint : ∀ (n : ℕ), Integrable (f n) μ<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R<VAR>h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop<VAR>h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot<VAR>h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω<GOAL>∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop atTop ↔ Tendsto (fun n => predictablePart f ℱ μ n ω) atTop atTop
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω✝ : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω<VAR>hf : Adapted ℱ f<VAR>hint : ∀ (n : ℕ), Integrable (f n) μ<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R<VAR>h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop<VAR>h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot<VAR>h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω<VAR>ω : Ω<VAR>hω₁ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop<VAR>hω₂ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot<VAR>hω₃ : ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω<VAR>hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω<GOAL>Tendsto (fun n => f n ω) atTop atTop ↔ Tendsto (fun n => predictablePart f ℱ μ n ω) atTop atTop
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>f : X → Y<VAR>g : Z → W<VAR>hf : IsOpenMap f<VAR>hg : IsOpenMap g<GOAL>IsOpenMap fun p => (f p.1, g p.2)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>f : X → Y<VAR>g : Z → W<VAR>hf : IsOpenMap f<VAR>hg : IsOpenMap g<GOAL>∀ (x : X × Z), 𝓝 (f x.1, g x.2) ≤ map (fun p => (f p.1, g p.2)) (𝓝 x)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>f : X → Y<VAR>g : Z → W<VAR>hf : IsOpenMap f<VAR>hg : IsOpenMap g<VAR>a : X<VAR>b : Z<GOAL>𝓝 (f (a, b).1, g (a, b).2) ≤ map (fun p => (f p.1, g p.2)) (𝓝 (a, b))
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>f : X → Y<VAR>g : Z → W<VAR>hf : IsOpenMap f<VAR>hg : IsOpenMap g<VAR>a : X<VAR>b : Z<GOAL>𝓝 (f (a, b).1) ×ˢ 𝓝 (g (a, b).2) ≤ map f (𝓝 a) ×ˢ map g (𝓝 b)
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)<VAR>i : ι<GOAL>biprod.inr.f i ≫ biprod.snd.f i = 𝟙 (L.X i)
<VAR>m✝ n✝ : ℕ<VAR>b : Bool<VAR>m n k : ℕ<VAR>h : k + 1 ≤ n + 1<GOAL>shiftLeft' b m (n + 1 - (k + 1)) = shiftLeft' b m (n + 1) >>> (k + 1)
<VAR>m✝ n✝ : ℕ<VAR>b : Bool<VAR>m n k : ℕ<VAR>h : k + 1 ≤ n + 1<GOAL>shiftLeft' b m (n - k) = bit b (shiftLeft' b m n) >>> 1 >>> k
<VAR>m✝ n✝ : ℕ<VAR>b : Bool<VAR>m n k : ℕ<VAR>h : k + 1 ≤ n + 1<GOAL>shiftLeft' b m n >>> k = (bit b (shiftLeft' b m n) / 2) >>> k
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>hf : StronglyMeasurable f<VAR>hfg : Integrable (f * g) μ<VAR>hg : Integrable g μ<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<GOAL>μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>hf : StronglyMeasurable f<VAR>hfg : Integrable (f * g) μ<VAR>hg : Integrable g μ<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<VAR>sets : ℕ → Set α<VAR>sets_prop : ∀ (n : ℕ), MeasurableSet (sets n) ∧ μ (sets n) < ⊤ ∧ ∀ x ∈ sets n, ‖f x‖ ≤ ↑n<VAR>h_univ : ⋃ i, sets i = Set.univ<GOAL>μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>hf : StronglyMeasurable f<VAR>hfg : Integrable (f * g) μ<VAR>hg : Integrable g μ<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<VAR>sets : ℕ → Set α<VAR>h_univ : ⋃ i, sets i = Set.univ<VAR>sets_prop : (∀ (x : ℕ), MeasurableSet (sets x)) ∧ (∀ (x : ℕ), μ (sets x) < ⊤) ∧ ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ ↑x<GOAL>μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>hf : StronglyMeasurable f<VAR>hfg : Integrable (f * g) μ<VAR>hg : Integrable g μ<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<VAR>sets : ℕ → Set α<VAR>h_univ : ⋃ i, sets i = Set.univ<VAR>h_meas : ∀ (x : ℕ), MeasurableSet (sets x)<VAR>h_finite : ∀ (x : ℕ), μ (sets x) < ⊤<VAR>h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ ↑x<GOAL>μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>hf : StronglyMeasurable f<VAR>hfg : Integrable (f * g) μ<VAR>hg : Integrable g μ<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<VAR>sets : ℕ → Set α<VAR>h_univ : ⋃ i, sets i = Set.univ<VAR>h_meas : ∀ (x : ℕ), MeasurableSet (sets x)<VAR>h_finite : ∀ (x : ℕ), μ (sets x) < ⊤<VAR>h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ ↑x<GOAL>∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, x ∈ sets n → (μ[f * g|m]) x = f x * (μ[g|m]) x
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>hf : StronglyMeasurable f<VAR>hfg : Integrable (f * g) μ<VAR>hg : Integrable g μ<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<VAR>sets : ℕ → Set α<VAR>h_univ : ⋃ i, sets i = Set.univ<VAR>h_meas : ∀ (x : ℕ), MeasurableSet (sets x)<VAR>h_finite : ∀ (x : ℕ), μ (sets x) < ⊤<VAR>h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ ↑x<VAR>n : ℕ<GOAL>∀ᵐ (x : α) ∂μ.restrict (sets n), (μ[f * g|m]) x = f x * (μ[g|m]) x
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>hf : StronglyMeasurable f<VAR>hfg : Integrable (f * g) μ<VAR>hg : Integrable g μ<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<VAR>sets : ℕ → Set α<VAR>h_univ : ⋃ i, sets i = Set.univ<VAR>h_meas : ∀ (x : ℕ), MeasurableSet (sets x)<VAR>h_finite : ∀ (x : ℕ), μ (sets x) < ⊤<VAR>h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ ↑x<VAR>n : ℕ<GOAL>μ.restrict (sets n)[f * g|m] =ᶠ[ae (μ.restrict (sets n))] f * μ.restrict (sets n)[g|m]
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>hf : StronglyMeasurable f<VAR>hfg : Integrable (f * g) μ<VAR>hg : Integrable g μ<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<VAR>sets : ℕ → Set α<VAR>h_univ : ⋃ i, sets i = Set.univ<VAR>h_meas : ∀ (x : ℕ), MeasurableSet (sets x)<VAR>h_finite : ∀ (x : ℕ), μ (sets x) < ⊤<VAR>h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ ↑x<VAR>n : ℕ<GOAL>μ.restrict (sets n)[(sets n).indicator f * g|m] =ᶠ[ae (μ.restrict (sets n))] (sets n).indicator f * μ.restrict (sets n)[g|m]
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>hf : StronglyMeasurable f<VAR>hfg : Integrable (f * g) μ<VAR>hg : Integrable g μ<VAR>hm : m ≤ m0<VAR>hμm this✝ : SigmaFinite (μ.trim hm)<VAR>sets : ℕ → Set α<VAR>h_univ : ⋃ i, sets i = Set.univ<VAR>h_meas : ∀ (x : ℕ), MeasurableSet (sets x)<VAR>h_finite : ∀ (x : ℕ), μ (sets x) < ⊤<VAR>h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ ↑x<VAR>n : ℕ<VAR>this : IsFiniteMeasure (μ.restrict (sets n))<GOAL>μ.restrict (sets n)[(sets n).indicator f * g|m] =ᶠ[ae (μ.restrict (sets n))] (sets n).indicator f * μ.restrict (sets n)[g|m]
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>hf : StronglyMeasurable f<VAR>hfg : Integrable (f * g) μ<VAR>hg : Integrable g μ<VAR>hm : m ≤ m0<VAR>hμm this✝ : SigmaFinite (μ.trim hm)<VAR>sets : ℕ → Set α<VAR>h_univ : ⋃ i, sets i = Set.univ<VAR>h_meas : ∀ (x : ℕ), MeasurableSet (sets x)<VAR>h_finite : ∀ (x : ℕ), μ (sets x) < ⊤<VAR>h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ ↑x<VAR>n : ℕ<VAR>this : IsFiniteMeasure (μ.restrict (sets n))<GOAL>∀ᵐ (x : α) ∂μ.restrict (sets n), ‖(sets n).indicator f x‖ ≤ ↑n
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>hf : StronglyMeasurable f<VAR>hfg : Integrable (f * g) μ<VAR>hg : Integrable g μ<VAR>hm : m ≤ m0<VAR>hμm this✝ : SigmaFinite (μ.trim hm)<VAR>sets : ℕ → Set α<VAR>h_univ : ⋃ i, sets i = Set.univ<VAR>h_meas : ∀ (x : ℕ), MeasurableSet (sets x)<VAR>h_finite : ∀ (x : ℕ), μ (sets x) < ⊤<VAR>h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ ↑x<VAR>n : ℕ<VAR>this : IsFiniteMeasure (μ.restrict (sets n))<VAR>x : α<GOAL>‖(sets n).indicator f x‖ ≤ ↑n
<VAR>a x✝ y✝ : ℂ<VAR>x y : ℝ<GOAL>angle (cexp (↑x * I)) (cexp (↑y * I)) = |toIocMod Real.two_pi_pos (-π) (x - y)|
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>a : α<VAR>l : List α<VAR>h : l ≠ []<VAR>ainl : a ∈ l<GOAL>a ∈ cycle l h
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>a : α<VAR>l : List α<VAR>h : l ≠ []<VAR>ainl : a ∈ l<GOAL>a ∈ l ++ₛ cycle l h
<VAR>J : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>F✝ : J ⥤ C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>F : J ⥤ C<VAR>inst✝¹ : HasLimit F<VAR>G : C ⥤ D<VAR>inst✝ : HasLimit (F ⋙ G)<VAR>c : Cone F<VAR>j✝ : J<GOAL>(G.map (lift F c) ≫ post F G) ≫ π (F ⋙ G) j✝ = lift (F ⋙ G) (G.mapCone c) ≫ π (F ⋙ G) j✝
<VAR>J : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>F✝ : J ⥤ C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>F : J ⥤ C<VAR>inst✝¹ : HasLimit F<VAR>G : C ⥤ D<VAR>inst✝ : HasLimit (F ⋙ G)<VAR>c : Cone F<VAR>j✝ : J<GOAL>G.map (c.π.app j✝) = (G.mapCone c).π.app j✝
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set α<VAR>t : Set β<VAR>s_ae_univ : μ sᶜ = 0<VAR>t_ae_univ : ν tᶜ = 0<GOAL>(μ.prod ν) (s ×ˢ t)ᶜ = 0
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set α<VAR>t : Set β<VAR>s_ae_univ : μ sᶜ = 0<VAR>t_ae_univ : ν tᶜ = 0<GOAL>(μ.prod ν) (sᶜ ×ˢ univ) = 0 ∧ (μ.prod ν) (univ ×ˢ tᶜ) = 0
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x - a) ⁻¹' Icc b c = Icc (b + a) (c + a)
<VAR>α β : Type u<VAR>c : Cardinal.{?u.235675}<VAR>x : α<GOAL>#α = 2 ↔ ∃! y, y ≠ x
<VAR>α β : Type u<VAR>c : Cardinal.{?u.235675}<VAR>x : α<GOAL>(∃ x y, x ≠ y ∧ {x, y} = univ) ↔ ∃! y, y ≠ x
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s t✝ : Set G<VAR>hs : IsOpen s<VAR>t : Set G<GOAL>s / closure t = s / t
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝³ : SeminormedGroup E<VAR>inst✝² : SeminormedGroup F<VAR>inst✝¹ : SeminormedGroup G<VAR>s✝ : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>inst✝ : FunLike 𝓕 E F<VAR>f : ι → κ → G<VAR>s : Set κ<VAR>l : Filter ι<GOAL>TendstoUniformlyOn f 1 l s ↔ ∀ ε > 0, ∀ᶠ (i : ι) in l, ∀ x ∈ s, ‖f i x‖ < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>a : ℝ≥0∞<GOAL>ContinuousOn ((fun p => p.1 - p.2) ∘ fun x => (a, x)) {x | x ≠ ⊤}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>a : ℝ≥0∞<GOAL>MapsTo (fun y => (a, y)) {x | x ≠ ⊤} {p | p ≠ (⊤, ⊤)}