ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>q : PMF (α → β)<VAR>p : PMF α<VAR>b : β<VAR>f : α → β<VAR>a : α<GOAL>(q f * if b = f a then p a else 0) = if b = f a then q f * p a else 0
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>inst✝¹ : NontriviallyNormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>c d✝ : 𝕜 → 𝕜'<VAR>c' d' : 𝕜'<VAR>hc : DifferentiableWithinAt 𝕜 c s x<VAR>d : 𝕜'<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>derivWithin (fun x => c x / d) s x = derivWithin c s x / d
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type w<VAR>K m n : Type u<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>w : m → K<VAR>v : n → K<VAR>a✝ : Nontrivial K<GOAL>(toLin' (vecMulVec w v)).rank ≤ 1
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type w<VAR>K m n : Type u<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>w : m → K<VAR>v : n → K<VAR>a✝ : Nontrivial K<GOAL>(toLin' (col (Fin 1) w) ∘ₗ toLin' (row (Fin 1) v)).rank ≤ 1
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type w<VAR>K m n : Type u<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>w : m → K<VAR>v : n → K<VAR>a✝ : Nontrivial K<GOAL>(toLin' (col (Fin 1) w)).rank ≤ 1
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type w<VAR>K m n : Type u<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>w : m → K<VAR>v : n → K<VAR>a✝ : Nontrivial K<GOAL>Module.rank K (Fin 1 → K) = 1
<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>inst✝¹ : HasColimit F<VAR>G : C ⥤ D<VAR>inst✝ : HasColimit (F ⋙ G)<VAR>c : Cocone F<VAR>j✝ : J<GOAL>ι (F ⋙ G) j✝ ≫ post F G ≫ G.map (desc F c) = ι (F ⋙ G) j✝ ≫ desc (F ⋙ G) (G.mapCocone c)
<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>inst✝¹ : HasColimit F<VAR>G : C ⥤ D<VAR>inst✝ : HasColimit (F ⋙ G)<VAR>c : Cocone F<VAR>j✝ : J<GOAL>G.map (c.ι.app j✝) = (G.mapCocone c).ι.app j✝
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x < y ^ z⁻¹ ↔ x ^ z < y
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ^ 1 < y ^ z⁻¹ ↔ x ^ z < y
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ^ (z * z⁻¹) < y ^ z⁻¹ ↔ x ^ z < y
<VAR>R S : Type u<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝⁷ : CommRing R'<VAR>inst✝⁶ : CommRing S'<VAR>f : R →+* S<VAR>inst✝⁵ : Algebra R R'<VAR>inst✝⁴ : Algebra S S'<VAR>inst✝³ : Algebra R' S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : IsScalarTower R R' S<VAR>inst✝ : IsLocalization M R'<VAR>s : Set S<VAR>x : S<VAR>hx : x ∈ Subalgebra.toSubmodule (Algebra.adjoin R' s)<GOAL>∃ t, t • x ∈ Subalgebra.toSubmodule (Algebra.adjoin R s)
<VAR>R S : Type u<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝⁷ : CommRing R'<VAR>inst✝⁶ : CommRing S'<VAR>f : R →+* S<VAR>inst✝⁵ : Algebra R R'<VAR>inst✝⁴ : Algebra S S'<VAR>inst✝³ : Algebra R' S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : IsScalarTower R R' S<VAR>inst✝ : IsLocalization M R'<VAR>s : Set S<VAR>x : S<VAR>hx : x ∈ Submodule.span R' ↑(Submonoid.closure s)<GOAL>∃ t, t • x ∈ Submodule.span R ↑(Submonoid.closure s)
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p✝ q✝ : MvPolynomial σ R<VAR>inst✝ : DecidableEq σ<VAR>p q : MvPolynomial σ R<GOAL>(p + q).degrees ≤ p.degrees ⊔ q.degrees
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p✝ q✝ : MvPolynomial σ R<VAR>inst✝ : DecidableEq σ<VAR>p q : MvPolynomial σ R<GOAL>((p + q).support.sup fun s => toMultiset s) ≤ (p.support.sup fun s => toMultiset s) ⊔ q.support.sup fun s => toMultiset s
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>P : α → Prop<VAR>r : α → α → Prop<VAR>inst✝ : IsSymm α r<VAR>h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y<GOAL>∃ f, (∀ (n : ℕ), P (f n)) ∧ Pairwise fun m n => r (f m) (f n)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>P : α → Prop<VAR>r : α → α → Prop<VAR>inst✝ : IsSymm α r<VAR>h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y<VAR>f : ℕ → α<VAR>hf : ∀ (n : ℕ), P (f n)<VAR>hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)<GOAL>∃ f, (∀ (n : ℕ), P (f n)) ∧ Pairwise fun m n => r (f m) (f n)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>P : α → Prop<VAR>r : α → α → Prop<VAR>inst✝ : IsSymm α r<VAR>h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y<VAR>f : ℕ → α<VAR>hf : ∀ (n : ℕ), P (f n)<VAR>hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)<VAR>m n : ℕ<VAR>hmn : m ≠ n<GOAL>(fun m n => r (f m) (f n)) m n
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>P : α → Prop<VAR>r : α → α → Prop<VAR>inst✝ : IsSymm α r<VAR>h✝ : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y<VAR>f : ℕ → α<VAR>hf : ∀ (n : ℕ), P (f n)<VAR>hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)<VAR>m n : ℕ<VAR>hmn : m ≠ n<VAR>h : m < n<GOAL>r (f m) (f n)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>P : α → Prop<VAR>r : α → α → Prop<VAR>inst✝ : IsSymm α r<VAR>h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y<VAR>f : ℕ → α<VAR>hf : ∀ (n : ℕ), P (f n)<VAR>hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)<VAR>m : ℕ<VAR>hmn : m ≠ m<GOAL>r (f m) (f m)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>P : α → Prop<VAR>r : α → α → Prop<VAR>inst✝ : IsSymm α r<VAR>h✝ : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y<VAR>f : ℕ → α<VAR>hf : ∀ (n : ℕ), P (f n)<VAR>hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)<VAR>m n : ℕ<VAR>hmn : m ≠ n<VAR>h : n < m<GOAL>r (f m) (f n)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ᶠ (n : ℕ) in atTop, ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>gt_zero : 0 < b (min_bi b)<GOAL>∀ᶠ (n : ℕ) in atTop, ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>gt_zero : 0 < b (min_bi b)<VAR>hlo : (fun n => ↑n / log ↑n ^ 2) =o[atTop] fun n => ↑n<GOAL>∀ᶠ (n : ℕ) in atTop, ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>gt_zero : 0 < b (min_bi b)<VAR>hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖<GOAL>∀ᶠ (n : ℕ) in atTop, ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>gt_zero : 0 < b (min_bi b)<VAR>hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖<VAR>hlo' : ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ b (min_bi b) / 2 * ‖↑x‖<GOAL>∀ᶠ (n : ℕ) in atTop, ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>gt_zero : 0 < b (min_bi b)<VAR>hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖<VAR>hlo' : ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ b (min_bi b) / 2 * ‖↑x‖<VAR>n : ℕ<VAR>hn : ‖↑n / log ↑n ^ 2‖ ≤ b (min_bi b) / 2 * ‖↑n‖<VAR>hn' : ∀ (i : α), b i * ↑n - ↑n / log ↑n ^ 2 ≤ ↑(r i n)<GOAL>∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>gt_zero : 0 < b (min_bi b)<VAR>hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖<VAR>hlo' : ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ b (min_bi b) / 2 * ‖↑x‖<VAR>n : ℕ<VAR>hn : ‖↑n / log ↑n ^ 2‖ ≤ b (min_bi b) / 2 * ‖↑n‖<VAR>hn' : ∀ (i : α), b i * ↑n - ↑n / log ↑n ^ 2 ≤ ↑(r i n)<VAR>i : α<GOAL>b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>gt_zero : 0 < b (min_bi b)<VAR>hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖<VAR>hlo' : ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ b (min_bi b) / 2 * ‖↑x‖<VAR>n : ℕ<VAR>hn' : ∀ (i : α), b i * ↑n - ↑n / log ↑n ^ 2 ≤ ↑(r i n)<VAR>i : α<VAR>hn : ‖↑n / log ↑n ^ 2‖ ≤ b (min_bi b) / 2 * ↑n<GOAL>b (min_bi b) / 2 * ↑n ≤ ↑(r i n)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>x✝ : Bornology α<VAR>s t : Set α<VAR>x : α<VAR>h : ∀ x ∈ s, IsBounded s<GOAL>IsBounded s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>x✝ : Bornology α<VAR>t : Set α<VAR>x : α<VAR>h : ∀ x ∈ ∅, IsBounded ∅<GOAL>IsBounded ∅
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>x✝¹ : Bornology α<VAR>s t : Set α<VAR>x✝ : α<VAR>h : ∀ x ∈ s, IsBounded s<VAR>x : α<VAR>hx : x ∈ s<GOAL>IsBounded s
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Indep I<GOAL>M.Basis I (M.closure I)
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Indep I<GOAL>M.Basis I {x | M.Basis I (insert x I)}
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<GOAL>∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤ ∫ (x : Ω), f n x ∂μ - ∫ (x : Ω), f 0 x ∂μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>h₁ : 0 ≤ ∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ<GOAL>∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤ ∫ (x : Ω), f n x ∂μ - ∫ (x : Ω), f 0 x ∂μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>h₁ : 0 ≤ ∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ<VAR>h₂ : ∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ = ∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ - ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ<GOAL>∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤ ∫ (x : Ω), f n x ∂μ - ∫ (x : Ω), f 0 x ∂μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>h₁ : ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤ ∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ<VAR>h₂ : ∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ = ∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ - ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ<GOAL>∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤ ∫ (x : Ω), f n x ∂μ - ∫ (x : Ω), f 0 x ∂μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>h₁ : ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤ ∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ<VAR>h₂ : ∫ (x : Ω), (∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ = ∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ - ∫ (x : Ω), (∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ<GOAL>∫ (x : Ω), (∑ k ∈ Finset.range n, (f (k + 1) - f k)) x ∂μ ≤ ∫ (x : Ω), f n x ∂μ - ∫ (x : Ω), f 0 x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : OrderTopology β<VAR>t : Set α<VAR>x : α<VAR>inst✝ : (𝓝 x).IsCountablyGenerated<VAR>htx : IsLUB t x<VAR>not_mem : x ∉ t<VAR>ht : t.Nonempty<GOAL>∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : OrderTopology β<VAR>t : Set α<VAR>x : α<VAR>inst✝ : (𝓝 x).IsCountablyGenerated<VAR>htx : IsLUB t x<VAR>not_mem : x ∉ t<VAR>ht : t.Nonempty<VAR>v : ℕ → α<VAR>hvx : Tendsto v atTop (𝓝[≤] x)<VAR>hvt : ∀ (n : ℕ), v n ∈ t<GOAL>∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : OrderTopology β<VAR>t : Set α<VAR>x : α<VAR>inst✝ : (𝓝 x).IsCountablyGenerated<VAR>htx : IsLUB t x<VAR>not_mem : x ∉ t<VAR>ht : t.Nonempty<VAR>v : ℕ → α<VAR>hvt : ∀ (n : ℕ), v n ∈ t<VAR>hvx : Tendsto v atTop (𝓝 x)<GOAL>∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : OrderTopology β<VAR>t : Set α<VAR>x : α<VAR>inst✝ : (𝓝 x).IsCountablyGenerated<VAR>htx : IsLUB t x<VAR>not_mem : x ∉ t<VAR>ht : t.Nonempty<VAR>v : ℕ → α<VAR>hvt : ∀ (n : ℕ), v n ∈ t<VAR>hvx : Tendsto v atTop (𝓝 x)<VAR>hvx' : ∀ {n : ℕ}, v n < x<GOAL>∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : OrderTopology β<VAR>t : Set α<VAR>x : α<VAR>inst✝ : (𝓝 x).IsCountablyGenerated<VAR>htx : IsLUB t x<VAR>not_mem : x ∉ t<VAR>ht : t.Nonempty<VAR>v : ℕ → α<VAR>hvt : ∀ (n : ℕ), v n ∈ t<VAR>hvx : Tendsto v atTop (𝓝 x)<VAR>hvx' : ∀ {n : ℕ}, v n < x<VAR>this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l<GOAL>∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : OrderTopology β<VAR>t : Set α<VAR>x : α<VAR>inst✝ : (𝓝 x).IsCountablyGenerated<VAR>htx : IsLUB t x<VAR>not_mem : x ∉ t<VAR>ht : t.Nonempty<VAR>v : ℕ → α<VAR>hvt : ∀ (n : ℕ), v n ∈ t<VAR>hvx : Tendsto v atTop (𝓝 x)<VAR>hvx' : ∀ {n : ℕ}, v n < x<VAR>this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l<VAR>N : ℕ → ℕ<VAR>hN : ∀ (k : ℕ), k < N k<VAR>hvN : ∀ (k : ℕ), v k < v (N k)<GOAL>∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : OrderTopology β<VAR>t : Set α<VAR>x : α<VAR>inst✝ : (𝓝 x).IsCountablyGenerated<VAR>htx : IsLUB t x<VAR>not_mem : x ∉ t<VAR>ht : t.Nonempty<VAR>v : ℕ → α<VAR>hvt : ∀ (n : ℕ), v n ∈ t<VAR>hvx : Tendsto v atTop (𝓝 x)<VAR>hvx' : ∀ {n : ℕ}, v n < x<VAR>this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l<VAR>N : ℕ → ℕ<VAR>hN : ∀ (k : ℕ), k < N k<VAR>hvN : ∀ (k : ℕ), v k < v (N k)<VAR>x✝ : ℕ<GOAL>v (N^[x✝] 0) < v (N^[x✝ + 1] 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : OrderTopology β<VAR>t : Set α<VAR>x : α<VAR>inst✝ : (𝓝 x).IsCountablyGenerated<VAR>htx : IsLUB t x<VAR>not_mem : x ∉ t<VAR>ht : t.Nonempty<VAR>v : ℕ → α<VAR>hvt : ∀ (n : ℕ), v n ∈ t<VAR>hvx : Tendsto v atTop (𝓝 x)<VAR>hvx' : ∀ {n : ℕ}, v n < x<VAR>this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l<VAR>N : ℕ → ℕ<VAR>hN : ∀ (k : ℕ), k < N k<VAR>hvN : ∀ (k : ℕ), v k < v (N k)<VAR>x✝ : ℕ<GOAL>N^[x✝] 0 < N^[x✝ + 1] 0
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>p q : α → Bool<VAR>l : List α<GOAL>filter p (filter q l) = filter q (filter p l)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>h : α ≃ᵢ β<VAR>s : Set β<GOAL>Metric.diam (⇑h ⁻¹' s) = Metric.diam s
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : NormedAddCommGroup E''<VAR>inst✝¹² : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : AddGroup G<VAR>inst✝⁴ : MeasurableAdd₂ G<VAR>inst✝³ : MeasurableNeg G<VAR>inst✝² : SFinite μ<VAR>inst✝¹ : μ.IsAddRightInvariant<VAR>inst✝ : SFinite ν<VAR>hf : Integrable f ν<VAR>hg : Integrable g μ<GOAL>Integrable (fun p => (L (f p.2)) (g (p.1 - p.2))) (μ.prod ν)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : NormedAddCommGroup E''<VAR>inst✝¹² : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : AddGroup G<VAR>inst✝⁴ : MeasurableAdd₂ G<VAR>inst✝³ : MeasurableNeg G<VAR>inst✝² : SFinite μ<VAR>inst✝¹ : μ.IsAddRightInvariant<VAR>inst✝ : SFinite ν<VAR>hf : Integrable f ν<VAR>hg : Integrable g μ<VAR>h_meas : AEStronglyMeasurable (fun p => (L (f p.2)) (g (p.1 - p.2))) (μ.prod ν)<GOAL>Integrable (fun p => (L (f p.2)) (g (p.1 - p.2))) (μ.prod ν)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : NormedAddCommGroup E''<VAR>inst✝¹² : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : AddGroup G<VAR>inst✝⁴ : MeasurableAdd₂ G<VAR>inst✝³ : MeasurableNeg G<VAR>inst✝² : SFinite μ<VAR>inst✝¹ : μ.IsAddRightInvariant<VAR>inst✝ : SFinite ν<VAR>hf : Integrable f ν<VAR>hg : Integrable g μ<VAR>h_meas : AEStronglyMeasurable (fun p => (L (f p.2)) (g (p.1 - p.2))) (μ.prod ν)<VAR>h2_meas : AEStronglyMeasurable (fun y => ∫ (x : G), ‖(L (f y)) (g (x - y))‖ ∂μ) ν<GOAL>Integrable (fun p => (L (f p.2)) (g (p.1 - p.2))) (μ.prod ν)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : NormedAddCommGroup E''<VAR>inst✝¹² : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : AddGroup G<VAR>inst✝⁴ : MeasurableAdd₂ G<VAR>inst✝³ : MeasurableNeg G<VAR>inst✝² : SFinite μ<VAR>inst✝¹ : μ.IsAddRightInvariant<VAR>inst✝ : SFinite ν<VAR>hf : Integrable f ν<VAR>hg : Integrable g μ<VAR>h_meas : AEStronglyMeasurable (fun p => (L (f p.2)) (g (p.1 - p.2))) (μ.prod ν)<VAR>h2_meas : AEStronglyMeasurable (fun y => ∫ (x : G), ‖(L (f y)) (g (x - y))‖ ∂μ) ν<GOAL>(∀ᵐ (y : G) ∂ν, Integrable (fun x => (L (f y)) (g (x - y))) μ) ∧ Integrable (fun y => ∫ (x : G), ‖(L (f y)) (g (x - y))‖ ∂μ) ν
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : NormedAddCommGroup E''<VAR>inst✝¹² : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : AddGroup G<VAR>inst✝⁴ : MeasurableAdd₂ G<VAR>inst✝³ : MeasurableNeg G<VAR>inst✝² : SFinite μ<VAR>inst✝¹ : μ.IsAddRightInvariant<VAR>inst✝ : SFinite ν<VAR>hf : Integrable f ν<VAR>hg : Integrable g μ<VAR>h_meas : AEStronglyMeasurable (fun p => (L (f p.2)) (g (p.1 - p.2))) (μ.prod ν)<VAR>h2_meas : AEStronglyMeasurable (fun y => ∫ (x : G), ‖(L (f y)) (g (x - y))‖ ∂μ) ν<GOAL>Integrable (fun y => ∫ (x : G), ‖(L (f y)) (g (x - y))‖ ∂μ) ν
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : NormedAddCommGroup E''<VAR>inst✝¹² : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : AddGroup G<VAR>inst✝⁴ : MeasurableAdd₂ G<VAR>inst✝³ : MeasurableNeg G<VAR>inst✝² : SFinite μ<VAR>inst✝¹ : μ.IsAddRightInvariant<VAR>inst✝ : SFinite ν<VAR>hf : Integrable f ν<VAR>hg : Integrable g μ<VAR>h_meas : AEStronglyMeasurable (fun p => (L (f p.2)) (g (p.1 - p.2))) (μ.prod ν)<VAR>h2_meas : AEStronglyMeasurable (fun y => ∫ (x : G), ‖(L (f y)) (g (x - y))‖ ∂μ) ν<GOAL>Integrable (fun t => ‖L‖ * ‖f t‖ * ∫ (x : G), ‖g (x - t)‖ ∂μ) ν