Loogle!

Result

Found 292 declarations mentioning Filter.EventuallyLE. Of these, only the first 200 are shown.

• Filter.EventuallyLE 📋 Mathlib.Order.Filter.Defs
  {α : Type u_1} {β : Type u_2} [LE β] (l : Filter α) (f g : α → β) : Prop
• Filter.EventuallyLE.refl 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [Preorder β] (l : Filter α) (f : α → β) : f ≤ᶠ[l] f
• Filter.EventuallyLE.rfl 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {f : α → β} : f ≤ᶠ[l] f
• Filter.EventuallyEq.ge 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {f g : α → β} (h : f =ᶠ[l] g) : g ≤ᶠ[l] f
• Filter.EventuallyEq.le 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {f g : α → β} (h : f =ᶠ[l] g) : f ≤ᶠ[l] g
• Filter.EventuallyLE.of_le 📋 Mathlib.Order.Filter.Basic
  {α : Type u_1} {β : Type u_2} [LE β] {l : Filter α} {f g : α → β} (h : f ≤ g) : f ≤ᶠ[l] g
• LE.le.eventuallyLE 📋 Mathlib.Order.Filter.Basic
  {α : Type u_1} {β : Type u_2} [LE β] {l : Filter α} {f g : α → β} (h : f ≤ g) : f ≤ᶠ[l] g
• Filter.EventuallyEq.trans_le 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {f g h : α → β} (H₁ : f =ᶠ[l] g) (H₂ : g ≤ᶠ[l] h) : f ≤ᶠ[l] h
• Filter.EventuallyLE.trans_eq 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {f g h : α → β} (H₁ : f ≤ᶠ[l] g) (H₂ : g =ᶠ[l] h) : f ≤ᶠ[l] h
• Filter.EventuallyLE.antisymm 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [PartialOrder β] {l : Filter α} {f g : α → β} (h₁ : f ≤ᶠ[l] g) (h₂ : g ≤ᶠ[l] f) : f =ᶠ[l] g
• Filter.eventuallyLE_iff_all_subsets 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [LE β] {f g : α → β} {l : Filter α} : f ≤ᶠ[l] g ↔ ∀ (s : Set α), ∀ᶠ (x : α) in l, x ∈ s → f x ≤ g x
• Filter.EventuallyLE.ge_iff_eq 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [PartialOrder β] {l : Filter α} {f g : α → β} (h : f ≤ᶠ[l] g) : g ≤ᶠ[l] f ↔ f =ᶠ[l] g
• Filter.EventuallyLE.ge_iff_eq' 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [PartialOrder β] {l : Filter α} {f g : α → β} (h : g ≤ᶠ[l] f) : f ≤ᶠ[l] g ↔ f =ᶠ[l] g
• Filter.EventuallyLE.trans 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {f g h : α → β} (H₁ : f ≤ᶠ[l] g) (H₂ : g ≤ᶠ[l] h) : f ≤ᶠ[l] h
• Filter.eventuallyLE_antisymm_iff 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [PartialOrder β] {l : Filter α} {f g : α → β} : f =ᶠ[l] g ↔ f ≤ᶠ[l] g ∧ g ≤ᶠ[l] f
• Filter.EventuallyLE.congr 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [LE β] {l : Filter α} {f f' g g' : α → β} (H : f ≤ᶠ[l] g) (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') : f' ≤ᶠ[l] g'
• Filter.eventuallyLE_congr 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [LE β] {l : Filter α} {f f' g g' : α → β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') : f ≤ᶠ[l] g ↔ f' ≤ᶠ[l] g'
• Filter.instTransForallEventuallyEqEventuallyLE 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [Preorder β] {l : Filter α} : Trans (fun x1 x2 => x1 =ᶠ[l] x2) (fun x1 x2 => x1 ≤ᶠ[l] x2) fun x1 x2 => x1 ≤ᶠ[l] x2
• Filter.instTransForallEventuallyLEEventuallyEq 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [Preorder β] {l : Filter α} : Trans (fun x1 x2 => x1 ≤ᶠ[l] x2) (fun x1 x2 => x1 =ᶠ[l] x2) fun x1 x2 => x1 ≤ᶠ[l] x2
• Filter.EventuallyLE.inf_le_of_left_le 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [SemilatticeInf β] {l : Filter α} {f g h : α → β} (hf : f ≤ᶠ[l] h) : f ⊓ g ≤ᶠ[l] h
• Filter.EventuallyLE.inf_le_of_right_le 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [SemilatticeInf β] {l : Filter α} {f g h : α → β} (hg : g ≤ᶠ[l] h) : f ⊓ g ≤ᶠ[l] h
• Filter.EventuallyLE.le_sup_of_le_left 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [SemilatticeSup β] {l : Filter α} {f g h : α → β} (hf : h ≤ᶠ[l] f) : h ≤ᶠ[l] f ⊔ g
• Filter.EventuallyLE.le_sup_of_le_right 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [SemilatticeSup β] {l : Filter α} {f g h : α → β} (hg : h ≤ᶠ[l] g) : h ≤ᶠ[l] f ⊔ g
• Filter.instTransForallEventuallyLE 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [Preorder β] {l : Filter α} : Trans (fun x1 x2 => x1 ≤ᶠ[l] x2) (fun x1 x2 => x1 ≤ᶠ[l] x2) fun x1 x2 => x1 ≤ᶠ[l] x2
• Filter.EventuallyLE.le_inf 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [SemilatticeInf β] {l : Filter α} {f g h : α → β} (hf : h ≤ᶠ[l] f) (hg : h ≤ᶠ[l] g) : h ≤ᶠ[l] f ⊓ g
• Filter.EventuallyLE.sup_le 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [SemilatticeSup β] {l : Filter α} {f g h : α → β} (hf : f ≤ᶠ[l] h) (hg : g ≤ᶠ[l] h) : f ⊔ g ≤ᶠ[l] h
• Filter.EventuallyLE.inf 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [SemilatticeInf β] {l : Filter α} {f₁ f₂ g₁ g₂ : α → β} (hf : f₂ ≤ᶠ[l] f₁) (hg : g₂ ≤ᶠ[l] g₁) : f₂ ⊓ g₂ ≤ᶠ[l] f₁ ⊓ g₁
• Filter.EventuallyLE.sup 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [SemilatticeSup β] {l : Filter α} {f₁ f₂ g₁ g₂ : α → β} (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) : f₁ ⊔ g₁ ≤ᶠ[l] f₂ ⊔ g₂
• Filter.eventuallyLE_bind 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE γ] {f : Filter α} {m : α → Filter β} {g₁ g₂ : β → γ} : g₁ ≤ᶠ[f.bind m] g₂ ↔ ∀ᶠ (x : α) in f, g₁ ≤ᶠ[m x] g₂
• Filter.eventuallyLE_map 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {m : α → β} [LE γ] {f₁ f₂ : β → γ} : f₁ ≤ᶠ[Filter.map m f] f₂ ↔ f₁ ∘ m ≤ᶠ[f] f₂ ∘ m
• Filter.bind_mono 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f₁ f₂ : Filter α} {g₁ g₂ : α → Filter β} (hf : f₁ ≤ f₂) (hg : g₁ ≤ᶠ[f₁] g₂) : f₁.bind g₁ ≤ f₂.bind g₂
• Filter.tendsto_atBot_mono' 📋 Mathlib.Order.Filter.AtTopBot.Tendsto
  {α : Type u_3} {β : Type u_4} [Preorder β] (l : Filter α) ⦃f₁ f₂ : α → β⦄ (h : f₂ ≤ᶠ[l] f₁) (h₁ : Filter.Tendsto f₁ l Filter.atBot) : Filter.Tendsto f₂ l Filter.atBot
• Filter.tendsto_atTop_mono' 📋 Mathlib.Order.Filter.AtTopBot.Tendsto
  {α : Type u_3} {β : Type u_4} [Preorder β] (l : Filter α) ⦃f₁ f₂ : α → β⦄ (h : f₁ ≤ᶠ[l] f₂) (h₁ : Filter.Tendsto f₁ l Filter.atTop) : Filter.Tendsto f₂ l Filter.atTop
• Filter.EventuallyLE.isMaxFilter 📋 Mathlib.Order.Filter.Extr
  {α : Type u_1} {β : Type u_2} [Preorder β] {f g : α → β} {a : α} {l : Filter α} (hle : g ≤ᶠ[l] f) (hfga : f a = g a) (h : IsMaxFilter f l a) : IsMaxFilter g l a
• Filter.EventuallyLE.isMinFilter 📋 Mathlib.Order.Filter.Extr
  {α : Type u_1} {β : Type u_2} [Preorder β] {f g : α → β} {a : α} {l : Filter α} (hle : f ≤ᶠ[l] g) (hfga : f a = g a) (h : IsMinFilter f l a) : IsMinFilter g l a
• Filter.EventuallyLE.prodMap 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_6} [LE γ] [LE δ] {la : Filter α} {fa ga : α → γ} (ha : fa ≤ᶠ[la] ga) {lb : Filter β} {fb gb : β → δ} (hb : fb ≤ᶠ[lb] gb) : Prod.map fa fb ≤ᶠ[la ×ˢ lb] Prod.map ga gb
• Filter.EventuallyLE.eventuallyLE_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} [LE α] {f g : X → α} (h : f ≤ᶠ[nhds x] g) : ∀ᶠ (y : X) in nhds x, f ≤ᶠ[nhds y] g
• eventually_eventuallyLE_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} [LE α] {f g : X → α} : (∀ᶠ (y : X) in nhds x, f ≤ᶠ[nhds y] g) ↔ f ≤ᶠ[nhds x] g
• Filter.EventuallyLE.prodMap_nhds 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {α : Type u_5} {β : Type u_6} [LE α] [LE β] {f₁ f₂ : X → α} {g₁ g₂ : Y → β} {x : X} {y : Y} (hf : f₁ ≤ᶠ[nhds x] f₂) (hg : g₁ ≤ᶠ[nhds y] g₂) : Prod.map f₁ g₁ ≤ᶠ[nhds (x, y)] Prod.map f₂ g₂
• le_of_tendsto_of_tendsto 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {f g : β → α} {b : Filter β} {a₁ a₂ : α} [hb : b.NeBot] (hf : Filter.Tendsto f b (nhds a₁)) (hg : Filter.Tendsto g b (nhds a₂)) (h : f ≤ᶠ[b] g) : a₁ ≤ a₂
• tendsto_le_of_eventuallyLE 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {f g : β → α} {b : Filter β} {a₁ a₂ : α} [hb : b.NeBot] (hf : Filter.Tendsto f b (nhds a₁)) (hg : Filter.Tendsto g b (nhds a₂)) (h : f ≤ᶠ[b] g) : a₁ ≤ a₂
• Filter.Tendsto.atBot_add_eventuallyLE_zero 📋 Mathlib.Order.Filter.AtTopBot.Monoid
  {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [Preorder M] [IsOrderedAddMonoid M] {l : Filter α} {f g : α → M} (hf : Filter.Tendsto f l Filter.atBot) (hg : g ≤ᶠ[l] 0) : Filter.Tendsto (fun x => f x + g x) l Filter.atBot
• Filter.Tendsto.atBot_mul_eventuallyLE_one 📋 Mathlib.Order.Filter.AtTopBot.Monoid
  {α : Type u_1} {M : Type u_2} [CommMonoid M] [Preorder M] [IsOrderedMonoid M] {l : Filter α} {f g : α → M} (hf : Filter.Tendsto f l Filter.atBot) (hg : g ≤ᶠ[l] 1) : Filter.Tendsto (fun x => f x * g x) l Filter.atBot
• Filter.Tendsto.atTop_add_zero_eventuallyLE 📋 Mathlib.Order.Filter.AtTopBot.Monoid
  {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [Preorder M] [IsOrderedAddMonoid M] {l : Filter α} {f g : α → M} (hf : Filter.Tendsto f l Filter.atTop) (hg : 0 ≤ᶠ[l] g) : Filter.Tendsto (fun x => f x + g x) l Filter.atTop
• Filter.Tendsto.atTop_mul_one_eventuallyLE 📋 Mathlib.Order.Filter.AtTopBot.Monoid
  {α : Type u_1} {M : Type u_2} [CommMonoid M] [Preorder M] [IsOrderedMonoid M] {l : Filter α} {f g : α → M} (hf : Filter.Tendsto f l Filter.atTop) (hg : 1 ≤ᶠ[l] g) : Filter.Tendsto (fun x => f x * g x) l Filter.atTop
• Filter.Tendsto.eventuallyLE_one_mul_atBot 📋 Mathlib.Order.Filter.AtTopBot.Monoid
  {α : Type u_1} {M : Type u_2} [CommMonoid M] [Preorder M] [IsOrderedMonoid M] {l : Filter α} {f g : α → M} (hf : f ≤ᶠ[l] 1) (hg : Filter.Tendsto g l Filter.atBot) : Filter.Tendsto (fun x => f x * g x) l Filter.atBot
• Filter.Tendsto.eventuallyLE_zero_add_atBot 📋 Mathlib.Order.Filter.AtTopBot.Monoid
  {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [Preorder M] [IsOrderedAddMonoid M] {l : Filter α} {f g : α → M} (hf : f ≤ᶠ[l] 0) (hg : Filter.Tendsto g l Filter.atBot) : Filter.Tendsto (fun x => f x + g x) l Filter.atBot
• Filter.Tendsto.one_eventuallyLE_mul_atTop 📋 Mathlib.Order.Filter.AtTopBot.Monoid
  {α : Type u_1} {M : Type u_2} [CommMonoid M] [Preorder M] [IsOrderedMonoid M] {l : Filter α} {f g : α → M} (hf : 1 ≤ᶠ[l] f) (hg : Filter.Tendsto g l Filter.atTop) : Filter.Tendsto (fun x => f x * g x) l Filter.atTop
• Filter.Tendsto.zero_eventuallyLE_add_atTop 📋 Mathlib.Order.Filter.AtTopBot.Monoid
  {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [Preorder M] [IsOrderedAddMonoid M] {l : Filter α} {f g : α → M} (hf : 0 ≤ᶠ[l] f) (hg : Filter.Tendsto g l Filter.atTop) : Filter.Tendsto (fun x => f x + g x) l Filter.atTop
• Filter.EventuallyLE.isLocalMax 📋 Mathlib.Topology.Order.LocalExtr
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder β] {f g : α → β} {a : α} (hle : g ≤ᶠ[nhds a] f) (hfga : f a = g a) (h : IsLocalMax f a) : IsLocalMax g a
• Filter.EventuallyLE.isLocalMin 📋 Mathlib.Topology.Order.LocalExtr
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder β] {f g : α → β} {a : α} (hle : f ≤ᶠ[nhds a] g) (hfga : f a = g a) (h : IsLocalMin f a) : IsLocalMin g a
• Filter.EventuallyLE.isLocalMaxOn 📋 Mathlib.Topology.Order.LocalExtr
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder β] {s : Set α} {f g : α → β} {a : α} (hle : g ≤ᶠ[nhdsWithin a s] f) (hfga : f a = g a) (h : IsLocalMaxOn f s a) : IsLocalMaxOn g s a
• Filter.EventuallyLE.isLocalMinOn 📋 Mathlib.Topology.Order.LocalExtr
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder β] {s : Set α} {f g : α → β} {a : α} (hle : f ≤ᶠ[nhdsWithin a s] g) (hfga : f a = g a) (h : IsLocalMinOn f s a) : IsLocalMinOn g s a
• tendsto_nhds_bot_mono 📋 Mathlib.Topology.Order.Basic
  {α : Type u} {β : Type v} [TopologicalSpace β] [Preorder β] [OrderBot β] [OrderTopology β] {l : Filter α} {f g : α → β} (hf : Filter.Tendsto f l (nhds ⊥)) (hg : g ≤ᶠ[l] f) : Filter.Tendsto g l (nhds ⊥)
• tendsto_nhds_top_mono 📋 Mathlib.Topology.Order.Basic
  {α : Type u} {β : Type v} [TopologicalSpace β] [Preorder β] [OrderTop β] [OrderTopology β] {l : Filter α} {f g : α → β} (hf : Filter.Tendsto f l (nhds ⊤)) (hg : f ≤ᶠ[l] g) : Filter.Tendsto g l (nhds ⊤)
• intermediate_value_univ₂_eventually₁ 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] [PreconnectedSpace X] {a : X} {l : Filter X} [l.NeBot] {f g : X → α} (hf : Continuous f) (hg : Continuous g) (ha : f a ≤ g a) (he : g ≤ᶠ[l] f) : ∃ x, f x = g x
• intermediate_value_univ₂_eventually₂ 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] [PreconnectedSpace X] {l₁ l₂ : Filter X} [l₁.NeBot] [l₂.NeBot] {f g : X → α} (hf : Continuous f) (hg : Continuous g) (he₁ : f ≤ᶠ[l₁] g) (he₂ : g ≤ᶠ[l₂] f) : ∃ x, f x = g x
• IsPreconnected.intermediate_value₂_eventually₁ 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {a : X} {l : Filter X} (ha : a ∈ s) [l.NeBot] (hl : l ≤ Filter.principal s) {f g : X → α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) (ha' : f a ≤ g a) (he : g ≤ᶠ[l] f) : ∃ x ∈ s, f x = g x
• IsPreconnected.intermediate_value₂_eventually₂ 📋 Mathlib.Topology.Order.IntermediateValue
  {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {l₁ l₂ : Filter X} [l₁.NeBot] [l₂.NeBot] (hl₁ : l₁ ≤ Filter.principal s) (hl₂ : l₂ ≤ Filter.principal s) {f g : X → α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) (he₁ : f ≤ᶠ[l₁] g) (he₂ : g ≤ᶠ[l₂] f) : ∃ x ∈ s, f x = g x
• Filter.IsBoundedUnder.mono_ge 📋 Mathlib.Order.Filter.IsBounded
  {α : Type u_1} {β : Type u_2} [Preorder β] {l : Filter α} {u v : α → β} (hu : Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) l u) (hv : u ≤ᶠ[l] v) : Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) l v
• Filter.IsBoundedUnder.mono_le 📋 Mathlib.Order.Filter.IsBounded
  {α : Type u_1} {β : Type u_2} [Preorder β] {l : Filter α} {u v : α → β} (hu : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l u) (hv : v ≤ᶠ[l] u) : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l v
• Filter.isBoundedUnder_le_mul_of_nonneg 📋 Mathlib.Order.Filter.IsBounded
  {α : Type u_1} {ι : Type u_4} [Preorder α] [Mul α] [Zero α] [PosMulMono α] [MulPosMono α] {f : Filter ι} {u v : ι → α} (h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x) (h₂ : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) (h₃ : 0 ≤ᶠ[f] v) (h₄ : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (u * v)
• Filter.isCoboundedUnder_ge_mul_of_nonneg 📋 Mathlib.Order.Filter.IsBounded
  {α : Type u_1} {ι : Type u_4} [LinearOrder α] [Mul α] [Zero α] [PosMulMono α] [MulPosMono α] {f : Filter ι} [f.NeBot] {u v : ι → α} (h₁ : 0 ≤ᶠ[f] u) (h₂ : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) (h₃ : 0 ≤ᶠ[f] v) (h₄ : Filter.IsCoboundedUnder (fun x1 x2 => x2 ≤ x1) f v) : Filter.IsCoboundedUnder (fun x1 x2 => x2 ≤ x1) f (u * v)
• Filter.limsup_le_limsup 📋 Mathlib.Order.LiminfLimsup
  {β : Type u_2} {α : Type u_6} [ConditionallyCompleteLattice β] {f : Filter α} {u v : α → β} (h : u ≤ᶠ[f] v) (hu : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) (hv : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v := by isBoundedDefault) : Filter.limsup u f ≤ Filter.limsup v f
• EReal.le_limsup_mul 📋 Mathlib.Topology.Instances.EReal.Lemmas
  {α : Type u_3} {f : Filter α} {u v : α → EReal} (hu : ∃ᶠ (x : α) in f, 0 ≤ u x) (hv : 0 ≤ᶠ[f] v) : Filter.limsup u f * Filter.liminf v f ≤ Filter.limsup (u * v) f
• EReal.le_liminf_mul 📋 Mathlib.Topology.Instances.EReal.Lemmas
  {α : Type u_3} {f : Filter α} {u v : α → EReal} (hu : 0 ≤ᶠ[f] u) (hv : 0 ≤ᶠ[f] v) : Filter.liminf u f * Filter.liminf v f ≤ Filter.liminf (u * v) f
• EReal.limsup_mul_le 📋 Mathlib.Topology.Instances.EReal.Lemmas
  {α : Type u_3} {f : Filter α} {u v : α → EReal} (hu : ∃ᶠ (x : α) in f, 0 ≤ u x) (hv : 0 ≤ᶠ[f] v) (h₁ : Filter.limsup u f ≠ 0 ∨ Filter.limsup v f ≠ ⊤) (h₂ : Filter.limsup u f ≠ ⊤ ∨ Filter.limsup v f ≠ 0) : Filter.limsup (u * v) f ≤ Filter.limsup u f * Filter.limsup v f
• EReal.liminf_mul_le 📋 Mathlib.Topology.Instances.EReal.Lemmas
  {α : Type u_3} {f : Filter α} {u v : α → EReal} [f.NeBot] (hu : 0 ≤ᶠ[f] u) (hv : 0 ≤ᶠ[f] v) (h₁ : Filter.limsup u f ≠ 0 ∨ Filter.liminf v f ≠ ⊤) (h₂ : Filter.limsup u f ≠ ⊤ ∨ Filter.liminf v f ≠ 0) : Filter.liminf (u * v) f ≤ Filter.limsup u f * Filter.liminf v f
• MeasureTheory.ae_le_of_ae_lt 📋 Mathlib.MeasureTheory.OuterMeasure.AE
  {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {β : Type u_4} [Preorder β] {f g : α → β} (h : ∀ᵐ (x : α) ∂μ, f x < g x) : f ≤ᵐ[μ] g
• MeasureTheory.one_le_div_ae 📋 Mathlib.MeasureTheory.Measure.Restrict
  {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_6} [Group β] [LE β] [MulRightMono β] (f g : α → β) : 1 ≤ᵐ[μ] g / f ↔ f ≤ᵐ[μ] g
• MeasureTheory.sub_nonneg_ae 📋 Mathlib.MeasureTheory.Measure.Restrict
  {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_6} [AddGroup β] [LE β] [AddRightMono β] (f g : α → β) : 0 ≤ᵐ[μ] g - f ↔ f ≤ᵐ[μ] g
• MeasureTheory.ae_le_of_ae_le_trim 📋 Mathlib.MeasureTheory.Measure.Trim
  {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_3} [LE E] {hm : m ≤ m0} {f₁ f₂ : α → E} (h12 : f₁ ≤ᵐ[μ.trim hm] f₂) : f₁ ≤ᵐ[μ] f₂
• MeasureTheory.StronglyMeasurable.ae_le_trim_of_stronglyMeasurable 📋 Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
  {α : Type u_1} {E : Type u_5} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → E} [TopologicalSpace E] [Preorder E] [OrderClosedTopology E] [TopologicalSpace.PseudoMetrizableSpace E] (hm : m ≤ m₀) (hf : MeasureTheory.StronglyMeasurable f) (hg : MeasureTheory.StronglyMeasurable g) (hfg : f ≤ᵐ[μ] g) : f ≤ᵐ[μ.trim hm] g
• MeasureTheory.StronglyMeasurable.ae_le_trim_iff 📋 Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
  {α : Type u_1} {E : Type u_5} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → E} [TopologicalSpace E] [Preorder E] [OrderClosedTopology E] [TopologicalSpace.PseudoMetrizableSpace E] (hm : m ≤ m₀) (hf : MeasureTheory.StronglyMeasurable f) (hg : MeasureTheory.StronglyMeasurable g) : f ≤ᵐ[μ.trim hm] g ↔ f ≤ᵐ[μ] g
• MeasureTheory.ae_eq_of_ae_le_of_lintegral_le 📋 Mathlib.MeasureTheory.Integral.Lebesgue.Markov
  {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} (hfg : f ≤ᵐ[μ] g) (hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤) (hg : AEMeasurable g μ) (hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ) : f =ᵐ[μ] g
• MeasureTheory.lintegral_strict_mono_of_ae_le_of_frequently_ae_lt 📋 Mathlib.MeasureTheory.Integral.Lebesgue.Markov
  {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} (hg : AEMeasurable g μ) (hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤) (h_le : f ≤ᵐ[μ] g) (h : ∃ᵐ (x : α) ∂μ, f x ≠ g x) : ∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ
• MeasureTheory.lintegral_add_mul_meas_add_le_le_lintegral 📋 Mathlib.MeasureTheory.Integral.Lebesgue.Markov
  {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} (hle : f ≤ᵐ[μ] g) (hg : AEMeasurable g μ) (ε : ENNReal) : ∫⁻ (a : α), f a ∂μ + ε * μ {x | f x + ε ≤ g x} ≤ ∫⁻ (a : α), g a ∂μ
• MeasureTheory.lintegral_strict_mono_of_ae_le_of_ae_lt_on 📋 Mathlib.MeasureTheory.Integral.Lebesgue.Markov
  {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} (hg : AEMeasurable g μ) (hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤) (h_le : f ≤ᵐ[μ] g) {s : Set α} (hμs : μ s ≠ 0) (h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x < g x) : ∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ
• MeasureTheory.lintegral_sub 📋 Mathlib.MeasureTheory.Integral.Lebesgue.Sub
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ENNReal} (hg : Measurable g) (hg_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤) (h_le : g ≤ᵐ[μ] f) : ∫⁻ (a : α), f a - g a ∂μ = ∫⁻ (a : α), f a ∂μ - ∫⁻ (a : α), g a ∂μ
• MeasureTheory.lintegral_sub' 📋 Mathlib.MeasureTheory.Integral.Lebesgue.Sub
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ENNReal} (hg : AEMeasurable g μ) (hg_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤) (h_le : g ≤ᵐ[μ] f) : ∫⁻ (a : α), f a - g a ∂μ = ∫⁻ (a : α), f a ∂μ - ∫⁻ (a : α), g a ∂μ
• MeasureTheory.lintegral_iInf_ae 📋 Mathlib.MeasureTheory.Integral.Lebesgue.Sub
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} (h_meas : ∀ (n : ℕ), Measurable (f n)) (h_mono : ∀ (n : ℕ), f n.succ ≤ᵐ[μ] f n) (h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤) : ∫⁻ (a : α), ⨅ n, f n a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ
• MeasureTheory.limsup_lintegral_le 📋 Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} (g : α → ENNReal) (hf_meas : ∀ (n : ℕ), Measurable (f n)) (h_bound : ∀ (n : ℕ), f n ≤ᵐ[μ] g) (h_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤) : Filter.limsup (fun n => ∫⁻ (a : α), f n a ∂μ) Filter.atTop ≤ ∫⁻ (a : α), Filter.limsup (fun n => f n a) Filter.atTop ∂μ
• MeasureTheory.tendsto_lintegral_of_dominated_convergence 📋 Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {F : ℕ → α → ENNReal} {f : α → ENNReal} (bound : α → ENNReal) (hF_meas : ∀ (n : ℕ), Measurable (F n)) (h_bound : ∀ (n : ℕ), F n ≤ᵐ[μ] bound) (h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (nhds (f a))) : Filter.Tendsto (fun n => ∫⁻ (a : α), F n a ∂μ) Filter.atTop (nhds (∫⁻ (a : α), f a ∂μ))
• MeasureTheory.tendsto_lintegral_of_dominated_convergence' 📋 Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {F : ℕ → α → ENNReal} {f : α → ENNReal} (bound : α → ENNReal) (hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ) (h_bound : ∀ (n : ℕ), F n ≤ᵐ[μ] bound) (h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤) (h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (nhds (f a))) : Filter.Tendsto (fun n => ∫⁻ (a : α), F n a ∂μ) Filter.atTop (nhds (∫⁻ (a : α), f a ∂μ))
• MeasureTheory.lintegral_enorm_of_ae_nonneg 📋 Mathlib.MeasureTheory.Integral.Lebesgue.Norm
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ} (h_nonneg : 0 ≤ᵐ[μ] f) : ∫⁻ (x : α), ‖f x‖ₑ ∂μ = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ
• MeasureTheory.withDensity_mono 📋 Mathlib.MeasureTheory.Measure.WithDensity
  {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} (hfg : f ≤ᵐ[μ] g) : μ.withDensity f ≤ μ.withDensity g
• MeasureTheory.hasFiniteIntegral_iff_ofReal 📋 Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
  {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (h : 0 ≤ᵐ[μ] f) : MeasureTheory.HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ < ⊤
• Asymptotics.IsBigO.of_norm_eventuallyLE 📋 Mathlib.Analysis.Asymptotics.Defs
  {α : Type u_1} {E : Type u_2} {f : α → E} {l : Filter α} [Norm E] {g : α → ℝ} (h : (fun x => ‖f x‖) ≤ᶠ[l] g) : f =O[l] g
• Asymptotics.IsBigO.pow_of_le_right 📋 Mathlib.Analysis.Asymptotics.Lemmas
  {α : Type u_1} {l : Filter α} {f : α → ℝ} (hf : 1 ≤ᶠ[l] f) {m n : ℕ} (h : n ≤ m) : (f ^ n) =O[l] (f ^ m)
• Asymptotics.IsBigO.sqrt 📋 Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
  {α : Type u_1} {l : Filter α} {f g : α → ℝ} (hfg : f =O[l] g) (hg : 0 ≤ᶠ[l] g) : (fun x => √(f x)) =O[l] fun x => √(g x)
• Asymptotics.IsLittleO.sqrt 📋 Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
  {α : Type u_1} {l : Filter α} {f g : α → ℝ} (hfg : f =o[l] g) (hg : 0 ≤ᶠ[l] g) : (fun x => √(f x)) =o[l] fun x => √(g x)
• Asymptotics.IsTheta.sqrt 📋 Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
  {α : Type u_1} {l : Filter α} {f g : α → ℝ} (hfg : f =Θ[l] g) (hf : 0 ≤ᶠ[l] f) (hg : 0 ≤ᶠ[l] g) : (fun x => √(f x)) =Θ[l] fun x => √(g x)
• Asymptotics.IsBigO.rpow 📋 Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
  {α : Type u_1} {r : ℝ} {l : Filter α} {f g : α → ℝ} (hr : 0 ≤ r) (hg : 0 ≤ᶠ[l] g) (h : f =O[l] g) : (fun x => f x ^ r) =O[l] fun x => g x ^ r
• Asymptotics.IsLittleO.rpow 📋 Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
  {α : Type u_1} {r : ℝ} {l : Filter α} {f g : α → ℝ} (hr : 0 < r) (hg : 0 ≤ᶠ[l] g) (h : f =o[l] g) : (fun x => f x ^ r) =o[l] fun x => g x ^ r
• Asymptotics.IsTheta.rpow 📋 Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
  {α : Type u_1} {r : ℝ} {l : Filter α} {f g : α → ℝ} (hf : 0 ≤ᶠ[l] f) (hg : 0 ≤ᶠ[l] g) (h : f =Θ[l] g) : (fun x => f x ^ r) =Θ[l] fun x => g x ^ r
• Asymptotics.IsBigOWith.rpow 📋 Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
  {α : Type u_1} {r c : ℝ} {l : Filter α} {f g : α → ℝ} (h : Asymptotics.IsBigOWith c l f g) (hc : 0 ≤ c) (hr : 0 ≤ r) (hg : 0 ≤ᶠ[l] g) : Asymptotics.IsBigOWith (c ^ r) l (fun x => f x ^ r) fun x => g x ^ r
• Filter.Germ.coe_le 📋 Mathlib.Order.Filter.Germ.Basic
  {α : Type u_1} {β : Type u_2} {l : Filter α} {f g : α → β} [LE β] : ↑f ≤ ↑g ↔ f ≤ᶠ[l] g
• MeasureTheory.AEEqFun.coeFn_le 📋 Mathlib.MeasureTheory.Function.AEEqFun
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [Preorder β] {f g : α →ₘ[μ] β} : ↑f ≤ᵐ[μ] ↑g ↔ f ≤ g
• MeasureTheory.AEEqFun.mk_le_mk 📋 Mathlib.MeasureTheory.Function.AEEqFun
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace β] [Preorder β] {f g : α → β} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) : MeasureTheory.AEEqFun.mk f hf ≤ MeasureTheory.AEEqFun.mk g hg ↔ f ≤ᵐ[μ] g
• MeasureTheory.Measure.ae_le_pi 📋 Mathlib.MeasureTheory.Constructions.Pi
  {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] {μ : (i : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] {β : ι → Type u_4} [(i : ι) → Preorder (β i)] {f f' : (i : ι) → α i → β i} (h : ∀ (i : ι), f i ≤ᵐ[μ i] f' i) : (fun x i => f i (x i)) ≤ᵐ[MeasureTheory.Measure.pi μ] fun x i => f' i (x i)
• essSup_le_of_ae_le 📋 Mathlib.MeasureTheory.Function.EssSup
  {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [ConditionallyCompleteLattice β] {f : α → β} (c : β) (hf : f ≤ᵐ[μ] fun x => c) (hfbdd : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae μ) f := by isBoundedDefault) : essSup f μ ≤ c
• le_essInf_of_ae_le 📋 Mathlib.MeasureTheory.Function.EssSup
  {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [ConditionallyCompleteLattice β] {f : α → β} (c : β) (hf : (fun x => c) ≤ᵐ[μ] f) (hfbdd : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) (MeasureTheory.ae μ) f := by isBoundedDefault) : c ≤ essInf f μ
• essInf_mono_ae 📋 Mathlib.MeasureTheory.Function.EssSup
  {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [ConditionallyCompleteLattice β] {f g : α → β} (hfg : f ≤ᵐ[μ] g) (hf : Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) (MeasureTheory.ae μ) f := by isBoundedDefault) (hg : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) (MeasureTheory.ae μ) g := by isBoundedDefault) : essInf f μ ≤ essInf g μ
• essSup_mono_ae 📋 Mathlib.MeasureTheory.Function.EssSup
  {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [ConditionallyCompleteLattice β] {f g : α → β} (hfg : f ≤ᵐ[μ] g) (hf : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae μ) f := by isBoundedDefault) (hg : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae μ) g := by isBoundedDefault) : essSup f μ ≤ essSup g μ
• MeasureTheory.Lp.coeFn_le 📋 Mathlib.MeasureTheory.Function.LpOrder
  {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedAddCommGroup E] [PartialOrder E] (f g : ↥(MeasureTheory.Lp E p μ)) : ↑↑f ≤ᵐ[μ] ↑↑g ↔ f ≤ g
• MeasureTheory.Lp.coeFn_nonneg 📋 Mathlib.MeasureTheory.Function.LpOrder
  {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedAddCommGroup E] [PartialOrder E] (f : ↥(MeasureTheory.Lp E p μ)) : 0 ≤ᵐ[μ] ↑↑f ↔ 0 ≤ f
• MeasureTheory.lintegral_ofReal_ne_top_iff_integrable 📋 Mathlib.MeasureTheory.Function.L1Space.Integrable
  {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hfm : MeasureTheory.AEStronglyMeasurable f μ) (hf : 0 ≤ᵐ[μ] f) : ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ ≠ ⊤ ↔ MeasureTheory.Integrable f μ
• MeasureTheory.integrable_of_le_of_le 📋 Mathlib.MeasureTheory.Function.L1Space.Integrable
  {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g₁ g₂ : α → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f μ) (h_le₁ : g₁ ≤ᵐ[μ] f) (h_le₂ : f ≤ᵐ[μ] g₂) (h_int₁ : MeasureTheory.Integrable g₁ μ) (h_int₂ : MeasureTheory.Integrable g₂ μ) : MeasureTheory.Integrable f μ
• MeasureTheory.integrable_left_of_integrable_add_of_nonneg 📋 Mathlib.MeasureTheory.Function.L1Space.Integrable
  {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ℝ} (h_meas : MeasureTheory.AEStronglyMeasurable f μ) (hf : 0 ≤ᵐ[μ] f) (hg : 0 ≤ᵐ[μ] g) (h_int : MeasureTheory.Integrable (f + g) μ) : MeasureTheory.Integrable f μ
• MeasureTheory.integrable_right_of_integrable_add_of_nonneg 📋 Mathlib.MeasureTheory.Function.L1Space.Integrable
  {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ℝ} (h_meas : MeasureTheory.AEStronglyMeasurable f μ) (hf : 0 ≤ᵐ[μ] f) (hg : 0 ≤ᵐ[μ] g) (h_int : MeasureTheory.Integrable (f + g) μ) : MeasureTheory.Integrable g μ
• MeasureTheory.integrable_add_iff_of_nonneg 📋 Mathlib.MeasureTheory.Function.L1Space.Integrable
  {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ℝ} (h_meas : MeasureTheory.AEStronglyMeasurable f μ) (hf : 0 ≤ᵐ[μ] f) (hg : 0 ≤ᵐ[μ] g) : MeasureTheory.Integrable (f + g) μ ↔ MeasureTheory.Integrable f μ ∧ MeasureTheory.Integrable g μ
• MeasureTheory.integrable_add_iff_of_nonpos 📋 Mathlib.MeasureTheory.Function.L1Space.Integrable
  {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ℝ} (h_meas : MeasureTheory.AEStronglyMeasurable f μ) (hf : f ≤ᵐ[μ] 0) (hg : g ≤ᵐ[μ] 0) : MeasureTheory.Integrable (f + g) μ ↔ MeasureTheory.Integrable f μ ∧ MeasureTheory.Integrable g μ
• indicator_eventuallyLE_indicator 📋 Mathlib.Order.Filter.IndicatorFunction
  {α : Type u_1} {β : Type u_2} [Zero β] [Preorder β] {s : Set α} {f g : α → β} {l : Filter α} (h : f ≤ᶠ[l ⊓ Filter.principal s] g) : s.indicator f ≤ᶠ[l] s.indicator g
• mulIndicator_eventuallyLE_mulIndicator 📋 Mathlib.Order.Filter.IndicatorFunction
  {α : Type u_1} {β : Type u_2} [One β] [Preorder β] {s : Set α} {f g : α → β} {l : Filter α} (h : f ≤ᶠ[l ⊓ Filter.principal s] g) : s.mulIndicator f ≤ᶠ[l] s.mulIndicator g
• MeasureTheory.Lp.simpleFunc.coeFn_le 📋 Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
  {α : Type u_1} [MeasurableSpace α] {p : ENNReal} {μ : MeasureTheory.Measure α} {G : Type u_7} [NormedAddCommGroup G] [PartialOrder G] (f g : ↥(MeasureTheory.Lp.simpleFunc G p μ)) : ↑↑↑f ≤ᵐ[μ] ↑↑↑g ↔ f ≤ g
• MeasureTheory.Lp.simpleFunc.coeFn_nonneg 📋 Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
  {α : Type u_1} [MeasurableSpace α] {p : ENNReal} {μ : MeasureTheory.Measure α} {G : Type u_7} [NormedAddCommGroup G] [PartialOrder G] (f : ↥(MeasureTheory.Lp.simpleFunc G p μ)) : 0 ≤ᵐ[μ] ↑↑↑f ↔ 0 ≤ f
• MeasureTheory.SimpleFunc.integral_eq_lintegral 📋 Mathlib.MeasureTheory.Integral.Bochner.L1
  {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α ℝ} (hf : MeasureTheory.Integrable (⇑f) μ) (h_pos : 0 ≤ᵐ[μ] ⇑f) : MeasureTheory.SimpleFunc.integral μ f = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
• MeasureTheory.SimpleFunc.integral_nonneg 📋 Mathlib.MeasureTheory.Integral.Bochner.L1
  {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PartialOrder F] [IsOrderedAddMonoid F] [IsOrderedModule ℝ F] {f : MeasureTheory.SimpleFunc α F} (hf : 0 ≤ᵐ[μ] ⇑f) : 0 ≤ MeasureTheory.SimpleFunc.integral μ f
• MeasureTheory.SimpleFunc.integral_mono_measure 📋 Mathlib.MeasureTheory.Integral.Bochner.L1
  {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PartialOrder F] [IsOrderedAddMonoid F] [IsOrderedModule ℝ F] {ν : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α F} (hf : 0 ≤ᵐ[ν] ⇑f) (hμν : μ ≤ ν) (hfν : MeasureTheory.Integrable (⇑f) ν) : MeasureTheory.SimpleFunc.integral μ f ≤ MeasureTheory.SimpleFunc.integral ν f
• MeasureTheory.SimpleFunc.integral_mono 📋 Mathlib.MeasureTheory.Integral.Bochner.L1
  {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PartialOrder F] [IsOrderedAddMonoid F] [IsOrderedModule ℝ F] {f g : MeasureTheory.SimpleFunc α F} (h : ⇑f ≤ᵐ[μ] ⇑g) (hf : MeasureTheory.Integrable (⇑f) μ) (hg : MeasureTheory.Integrable (⇑g) μ) : MeasureTheory.SimpleFunc.integral μ f ≤ MeasureTheory.SimpleFunc.integral μ g
• MeasureTheory.L1.SimpleFunc.integral_eq_lintegral 📋 Mathlib.MeasureTheory.Integral.Bochner.L1
  {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ↥(α →₁ₛ[μ] ℝ)} (h_pos : 0 ≤ᵐ[μ] ⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f)) : MeasureTheory.L1.SimpleFunc.integral f = (∫⁻ (a : α), ENNReal.ofReal ((MeasureTheory.Lp.simpleFunc.toSimpleFunc f) a) ∂μ).toReal
• MeasureTheory.setToFun_nonneg 📋 Mathlib.MeasureTheory.Integral.SetToL1.Function
  {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G' : Type u_5} {G'' : Type u_6} [NormedAddCommGroup G'] [PartialOrder G'] [NormedSpace ℝ G'] [NormedAddCommGroup G''] [PartialOrder G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] [ClosedIciTopology G''] {T : Set α → G' →L[ℝ] G''} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x) {f : α → G'} (hf : 0 ≤ᵐ[μ] f) : 0 ≤ MeasureTheory.setToFun μ T hT f
• MeasureTheory.setToFun_mono 📋 Mathlib.MeasureTheory.Integral.SetToL1.Function
  {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G' : Type u_5} {G'' : Type u_6} [NormedAddCommGroup G'] [PartialOrder G'] [NormedSpace ℝ G'] [NormedAddCommGroup G''] [PartialOrder G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] [ClosedIciTopology G''] [IsOrderedAddMonoid G'] {T : Set α → G' →L[ℝ] G''} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x) {f g : α → G'} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) (hfg : f ≤ᵐ[μ] g) : MeasureTheory.setToFun μ T hT f ≤ MeasureTheory.setToFun μ T hT g
• MeasureTheory.integral_eq_lintegral_of_nonneg_ae 📋 Mathlib.MeasureTheory.Integral.Bochner.Basic
  {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : 0 ≤ᵐ[μ] f) (hfm : MeasureTheory.AEStronglyMeasurable f μ) : ∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
• MeasureTheory.ofReal_integral_eq_lintegral_ofReal 📋 Mathlib.MeasureTheory.Integral.Bochner.Basic
  {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hfi : MeasureTheory.Integrable f μ) (f_nn : 0 ≤ᵐ[μ] f) : ENNReal.ofReal (∫ (x : α), f x ∂μ) = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ
• MeasureTheory.mul_meas_ge_le_integral_of_nonneg 📋 Mathlib.MeasureTheory.Integral.Bochner.Basic
  {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf_nonneg : 0 ≤ᵐ[μ] f) (hf_int : MeasureTheory.Integrable f μ) (ε : ℝ) : ε * μ.real {x | ε ≤ f x} ≤ ∫ (x : α), f x ∂μ
• MeasureTheory.integral_eq_zero_iff_of_nonneg_ae 📋 Mathlib.MeasureTheory.Integral.Bochner.Basic
  {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : 0 ≤ᵐ[μ] f) (hfi : MeasureTheory.Integrable f μ) : ∫ (x : α), f x ∂μ = 0 ↔ f =ᵐ[μ] 0
• MeasureTheory.integral_pos_iff_support_of_nonneg_ae 📋 Mathlib.MeasureTheory.Integral.Bochner.Basic
  {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : 0 ≤ᵐ[μ] f) (hfi : MeasureTheory.Integrable f μ) : 0 < ∫ (x : α), f x ∂μ ↔ 0 < μ (Function.support f)
• MeasureTheory.integral_eq_iff_of_ae_le 📋 Mathlib.MeasureTheory.Integral.Bochner.Basic
  {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ℝ} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) (hfg : f ≤ᵐ[μ] g) : ∫ (a : α), f a ∂μ = ∫ (a : α), g a ∂μ ↔ f =ᵐ[μ] g
• MeasureTheory.integral_nonneg_of_ae 📋 Mathlib.MeasureTheory.Integral.Bochner.Basic
  {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] [ClosedIciTopology E] {f : α → E} (hf : 0 ≤ᵐ[μ] f) : 0 ≤ ∫ (x : α), f x ∂μ
• MeasureTheory.integral_nonpos_of_ae 📋 Mathlib.MeasureTheory.Integral.Bochner.Basic
  {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] [ClosedIciTopology E] {f : α → E} (hf : f ≤ᵐ[μ] 0) : ∫ (x : α), f x ∂μ ≤ 0
• MeasureTheory.integral_mono_ae 📋 Mathlib.MeasureTheory.Integral.Bochner.Basic
  {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] [ClosedIciTopology E] {f g : α → E} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) (h : f ≤ᵐ[μ] g) : ∫ (x : α), f x ∂μ ≤ ∫ (x : α), g x ∂μ
• MeasureTheory.integral_mono_measure 📋 Mathlib.MeasureTheory.Integral.Bochner.Basic
  {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] [OrderClosedTopology E] {f : α → E} {ν : MeasureTheory.Measure α} (hle : μ ≤ ν) (hf : 0 ≤ᵐ[ν] f) (hfi : MeasureTheory.Integrable f ν) : ∫ (a : α), f a ∂μ ≤ ∫ (a : α), f a ∂ν
• MeasureTheory.integral_mono_of_nonneg 📋 Mathlib.MeasureTheory.Integral.Bochner.Basic
  {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] [ClosedIciTopology E] {f g : α → E} (hf : 0 ≤ᵐ[μ] f) (hgi : MeasureTheory.Integrable g μ) (h : f ≤ᵐ[μ] g) : ∫ (a : α), f a ∂μ ≤ ∫ (a : α), g a ∂μ
• MeasureTheory.integral_mul_le_Lp_mul_Lq_of_nonneg 📋 Mathlib.MeasureTheory.Integral.Bochner.Basic
  {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p q : ℝ} (hpq : p.HolderConjugate q) {f g : α → ℝ} (hf_nonneg : 0 ≤ᵐ[μ] f) (hg_nonneg : 0 ≤ᵐ[μ] g) (hf : MeasureTheory.MemLp f (ENNReal.ofReal p) μ) (hg : MeasureTheory.MemLp g (ENNReal.ofReal q) μ) : ∫ (a : α), f a * g a ∂μ ≤ (∫ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫ (a : α), g a ^ q ∂μ) ^ (1 / q)
• MeasureTheory.setIntegral_nonneg_of_ae 📋 Mathlib.MeasureTheory.Integral.Bochner.Set
  {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → ℝ} {s : Set X} (hf : 0 ≤ᵐ[μ] f) : 0 ≤ ∫ (x : X) in s, f x ∂μ
• MeasureTheory.setIntegral_nonpos_of_ae 📋 Mathlib.MeasureTheory.Integral.Bochner.Set
  {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → ℝ} {s : Set X} (hf : f ≤ᵐ[μ] 0) : ∫ (x : X) in s, f x ∂μ ≤ 0
• MeasureTheory.setIntegral_nonneg_of_ae_restrict 📋 Mathlib.MeasureTheory.Integral.Bochner.Set
  {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → ℝ} {s : Set X} (hf : 0 ≤ᵐ[μ.restrict s] f) : 0 ≤ ∫ (x : X) in s, f x ∂μ
• MeasureTheory.setIntegral_nonpos_of_ae_restrict 📋 Mathlib.MeasureTheory.Integral.Bochner.Set
  {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → ℝ} {s : Set X} (hf : f ≤ᵐ[μ.restrict s] 0) : ∫ (x : X) in s, f x ∂μ ≤ 0
• MeasureTheory.Integrable.measure_le_integral 📋 Mathlib.MeasureTheory.Integral.Bochner.Set
  {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → ℝ} (f_int : MeasureTheory.Integrable f μ) (f_nonneg : 0 ≤ᵐ[μ] f) {s : Set X} (hs : ∀ x ∈ s, 1 ≤ f x) : μ s ≤ ENNReal.ofReal (∫ (x : X), f x ∂μ)
• MeasureTheory.setIntegral_eq_zero_iff_of_nonneg_ae 📋 Mathlib.MeasureTheory.Integral.Bochner.Set
  {X : Type u_1} {mX : MeasurableSpace X} {s : Set X} {μ : MeasureTheory.Measure X} {f : X → ℝ} (hf : 0 ≤ᵐ[μ.restrict s] f) (hfi : MeasureTheory.IntegrableOn f s μ) : ∫ (x : X) in s, f x ∂μ = 0 ↔ f =ᵐ[μ.restrict s] 0
• MeasureTheory.setIntegral_pos_iff_support_of_nonneg_ae 📋 Mathlib.MeasureTheory.Integral.Bochner.Set
  {X : Type u_1} {mX : MeasurableSpace X} {s : Set X} {μ : MeasureTheory.Measure X} {f : X → ℝ} (hf : 0 ≤ᵐ[μ.restrict s] f) (hfi : MeasureTheory.IntegrableOn f s μ) : 0 < ∫ (x : X) in s, f x ∂μ ↔ 0 < μ (Function.support f ∩ s)
• MeasureTheory.setIntegral_le_integral 📋 Mathlib.MeasureTheory.Integral.Bochner.Set
  {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] {μ : MeasureTheory.Measure X} {f : X → E} {s : Set X} [OrderClosedTopology E] (hfi : MeasureTheory.Integrable f μ) (hf : 0 ≤ᵐ[μ] f) : ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X), f x ∂μ
• MeasureTheory.setIntegral_mono_ae 📋 Mathlib.MeasureTheory.Integral.Bochner.Set
  {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] {μ : MeasureTheory.Measure X} {f g : X → E} {s : Set X} [ClosedIciTopology E] (hf : MeasureTheory.IntegrableOn f s μ) (hg : MeasureTheory.IntegrableOn g s μ) (h : f ≤ᵐ[μ] g) : ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
• MeasureTheory.setIntegral_mono_ae_restrict 📋 Mathlib.MeasureTheory.Integral.Bochner.Set
  {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] {μ : MeasureTheory.Measure X} {f g : X → E} {s : Set X} [ClosedIciTopology E] (hf : MeasureTheory.IntegrableOn f s μ) (hg : MeasureTheory.IntegrableOn g s μ) (h : f ≤ᵐ[μ.restrict s] g) : ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
• MeasureTheory.setIntegral_mono_set 📋 Mathlib.MeasureTheory.Integral.Bochner.Set
  {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] [PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] {μ : MeasureTheory.Measure X} {f : X → E} {s t : Set X} [OrderClosedTopology E] (hfi : MeasureTheory.IntegrableOn f t μ) (hf : 0 ≤ᵐ[μ.restrict t] f) (hst : s ≤ᵐ[μ] t) : ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in t, f x ∂μ
• summable_condensed_iff_of_eventually_nonneg 📋 Mathlib.Analysis.PSeries
  {f : ℕ → ℝ} (h_nonneg : 0 ≤ᶠ[Filter.atTop] f) (h_mono : ∀ᶠ (k : ℕ) in Filter.atTop, f (k + 1) ≤ f k) : (Summable fun k => 2 ^ k * f (2 ^ k)) ↔ Summable f
• Asymptotics.IsBigOTVS.exists_eventuallyLE 📋 Mathlib.Analysis.Asymptotics.TVS
  {𝕜 : Type u_1} {α : Type u_2} {E : Type u_3} {F : Type u_4} [ENorm 𝕜] [TopologicalSpace E] [TopologicalSpace F] [Zero E] [Zero F] [SMul 𝕜 E] [SMul 𝕜 F] {l : Filter α} {f : α → E} {g : α → F} (self : f =O[𝕜; l] g) (U : Set E) : U ∈ nhds 0 → ∃ V ∈ nhds 0, (fun x => egauge 𝕜 U (f x)) ≤ᶠ[l] fun x => egauge 𝕜 V (g x)
• Asymptotics.IsBigOTVS.mk 📋 Mathlib.Analysis.Asymptotics.TVS
  {𝕜 : Type u_1} {α : Type u_2} {E : Type u_3} {F : Type u_4} [ENorm 𝕜] [TopologicalSpace E] [TopologicalSpace F] [Zero E] [Zero F] [SMul 𝕜 E] [SMul 𝕜 F] {l : Filter α} {f : α → E} {g : α → F} (exists_eventuallyLE : ∀ U ∈ nhds 0, ∃ V ∈ nhds 0, (fun x => egauge 𝕜 U (f x)) ≤ᶠ[l] fun x => egauge 𝕜 V (g x)) : f =O[𝕜; l] g
• Asymptotics.isBigOTVS_iff 📋 Mathlib.Analysis.Asymptotics.TVS
  (𝕜 : Type u_1) {α : Type u_2} {E : Type u_3} {F : Type u_4} [ENorm 𝕜] [TopologicalSpace E] [TopologicalSpace F] [Zero E] [Zero F] [SMul 𝕜 E] [SMul 𝕜 F] (l : Filter α) (f : α → E) (g : α → F) : f =O[𝕜; l] g ↔ ∀ U ∈ nhds 0, ∃ V ∈ nhds 0, (fun x => egauge 𝕜 U (f x)) ≤ᶠ[l] fun x => egauge 𝕜 V (g x)
• Asymptotics.IsLittleOTVS.exists_eventuallyLE_mul 📋 Mathlib.Analysis.Asymptotics.TVS
  {𝕜 : Type u_1} {α : Type u_2} {E : Type u_3} {F : Type u_4} [ENorm 𝕜] [TopologicalSpace E] [TopologicalSpace F] [Zero E] [Zero F] [SMul 𝕜 E] [SMul 𝕜 F] {l : Filter α} {f : α → E} {g : α → F} (self : f =o[𝕜; l] g) (U : Set E) : U ∈ nhds 0 → ∃ V ∈ nhds 0, ∀ (ε : NNReal), ε ≠ 0 → (fun x => egauge 𝕜 U (f x)) ≤ᶠ[l] fun x => ↑ε * egauge 𝕜 V (g x)
• Asymptotics.IsLittleOTVS.mk 📋 Mathlib.Analysis.Asymptotics.TVS
  {𝕜 : Type u_1} {α : Type u_2} {E : Type u_3} {F : Type u_4} [ENorm 𝕜] [TopologicalSpace E] [TopologicalSpace F] [Zero E] [Zero F] [SMul 𝕜 E] [SMul 𝕜 F] {l : Filter α} {f : α → E} {g : α → F} (exists_eventuallyLE_mul : ∀ U ∈ nhds 0, ∃ V ∈ nhds 0, ∀ (ε : NNReal), ε ≠ 0 → (fun x => egauge 𝕜 U (f x)) ≤ᶠ[l] fun x => ↑ε * egauge 𝕜 V (g x)) : f =o[𝕜; l] g
• Asymptotics.isLittleOTVS_iff 📋 Mathlib.Analysis.Asymptotics.TVS
  (𝕜 : Type u_1) {α : Type u_2} {E : Type u_3} {F : Type u_4} [ENorm 𝕜] [TopologicalSpace E] [TopologicalSpace F] [Zero E] [Zero F] [SMul 𝕜 E] [SMul 𝕜 F] (l : Filter α) (f : α → E) (g : α → F) : f =o[𝕜; l] g ↔ ∀ U ∈ nhds 0, ∃ V ∈ nhds 0, ∀ (ε : NNReal), ε ≠ 0 → (fun x => egauge 𝕜 U (f x)) ≤ᶠ[l] fun x => ↑ε * egauge 𝕜 V (g x)
• Asymptotics.IsLittleOTVS.exists_eventuallyLE_mul_ennreal 📋 Mathlib.Analysis.Asymptotics.TVS
  {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] {f : α → E} {g : α → F} {l : Filter α} (h : f =o[𝕜; l] g) {U : Set E} (hU : U ∈ nhds 0) : ∃ V ∈ nhds 0, ∀ (ε : ENNReal), ε ≠ 0 → (fun x => egauge 𝕜 U (f x)) ≤ᶠ[l] fun x => ε * egauge 𝕜 V (g x)
• Asymptotics.IsBigOTVS.of_egauge_le_mul 📋 Mathlib.Analysis.Asymptotics.TVS
  {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] {l : Filter α} {f : α → E} {g : α → F} [ContinuousConstSMul 𝕜 F] {ι : Sort u_7} {p : ι → Prop} {U : ι → Set E} (hb : (nhds 0).HasBasis p U) (h : ∀ (i : ι), p i → ∃ C, ∃ V ∈ nhds 0, (fun x => egauge 𝕜 (U i) (f x)) ≤ᶠ[l] fun x => ↑C * egauge 𝕜 V (g x)) : f =O[𝕜; l] g
• intervalIntegral.integral_nonneg_of_ae 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (hab : a ≤ b) (hf : 0 ≤ᵐ[μ] f) : 0 ≤ ∫ (u : ℝ) in a..b, f u ∂μ
• intervalIntegral.integral_nonneg_of_ae_restrict 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (hab : a ≤ b) (hf : 0 ≤ᵐ[μ.restrict (Set.Icc a b)] f) : 0 ≤ ∫ (u : ℝ) in a..b, f u ∂μ
• IntervalIntegrable.mono_fun_enorm' 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {ε : Type u_3} [TopologicalSpace ε] [ENormedAddMonoid ε] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [TopologicalSpace.PseudoMetrizableSpace ε] {f : ℝ → ε} {g : ℝ → ENNReal} (hg : IntervalIntegrable g μ a b) (hfm : MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.uIoc a b))) (hle : (fun x => ‖f x‖ₑ) ≤ᵐ[μ.restrict (Set.uIoc a b)] g) : IntervalIntegrable f μ a b
• IntervalIntegrable.mono_fun' 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {E : Type u_5} [NormedAddCommGroup E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → E} {g : ℝ → ℝ} (hg : IntervalIntegrable g μ a b) (hfm : MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.uIoc a b))) (hle : (fun x => ‖f x‖) ≤ᵐ[μ.restrict (Set.uIoc a b)] g) : IntervalIntegrable f μ a b
• intervalIntegral.integral_mono_ae 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {f g : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (hab : a ≤ b) (hf : IntervalIntegrable f μ a b) (hg : IntervalIntegrable g μ a b) (h : f ≤ᵐ[μ] g) : ∫ (u : ℝ) in a..b, f u ∂μ ≤ ∫ (u : ℝ) in a..b, g u ∂μ
• IntervalIntegrable.mono_fun_enorm 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {ε : Type u_3} {ε' : Type u_4} [TopologicalSpace ε] [ENormedAddMonoid ε] [TopologicalSpace ε'] [ENormedAddMonoid ε'] {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [TopologicalSpace.PseudoMetrizableSpace ε] [TopologicalSpace.PseudoMetrizableSpace ε'] {g : ℝ → ε'} (hf : IntervalIntegrable f μ a b) (hgm : MeasureTheory.AEStronglyMeasurable g (μ.restrict (Set.uIoc a b))) (hle : (fun x => ‖g x‖ₑ) ≤ᵐ[μ.restrict (Set.uIoc a b)] fun x => ‖f x‖ₑ) : IntervalIntegrable g μ a b
• intervalIntegral.integral_mono_ae_restrict 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {f g : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (hab : a ≤ b) (hf : IntervalIntegrable f μ a b) (hg : IntervalIntegrable g μ a b) (h : f ≤ᵐ[μ.restrict (Set.Icc a b)] g) : ∫ (u : ℝ) in a..b, f u ∂μ ≤ ∫ (u : ℝ) in a..b, g u ∂μ
• IntervalIntegrable.mono_fun 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → E} [NormedAddCommGroup F] {g : ℝ → F} (hf : IntervalIntegrable f μ a b) (hgm : MeasureTheory.AEStronglyMeasurable g (μ.restrict (Set.uIoc a b))) (hle : (fun x => ‖g x‖) ≤ᵐ[μ.restrict (Set.uIoc a b)] fun x => ‖f x‖) : IntervalIntegrable g μ a b
• intervalIntegral.integral_mono_interval 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {c d : ℝ} (hca : c ≤ a) (hab : a ≤ b) (hbd : b ≤ d) (hf : 0 ≤ᵐ[μ.restrict (Set.Ioc c d)] f) (hfi : IntervalIntegrable f μ c d) : ∫ (x : ℝ) in a..b, f x ∂μ ≤ ∫ (x : ℝ) in c..d, f x ∂μ
• intervalIntegral.abs_integral_mono_interval 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {c d : ℝ} (h : Set.uIoc a b ⊆ Set.uIoc c d) (hf : 0 ≤ᵐ[μ.restrict (Set.uIoc c d)] f) (hfi : IntervalIntegrable f μ c d) : |∫ (x : ℝ) in a..b, f x ∂μ| ≤ |∫ (x : ℝ) in c..d, f x ∂μ|
• intervalIntegral.integral_pos_iff_support_of_nonneg_ae 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (hf : 0 ≤ᵐ[μ] f) (hfi : IntervalIntegrable f μ a b) : 0 < ∫ (x : ℝ) in a..b, f x ∂μ ↔ a < b ∧ 0 < μ (Function.support f ∩ Set.Ioc a b)
• intervalIntegral.integral_eq_zero_iff_of_le_of_nonneg_ae 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (hab : a ≤ b) (hf : 0 ≤ᵐ[μ.restrict (Set.Ioc a b)] f) (hfi : IntervalIntegrable f μ a b) : ∫ (x : ℝ) in a..b, f x ∂μ = 0 ↔ f =ᵐ[μ.restrict (Set.Ioc a b)] 0
• intervalIntegral.integral_pos_iff_support_of_nonneg_ae' 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (hf : 0 ≤ᵐ[μ.restrict (Set.uIoc a b)] f) (hfi : IntervalIntegrable f μ a b) : 0 < ∫ (x : ℝ) in a..b, f x ∂μ ↔ a < b ∧ 0 < μ (Function.support f ∩ Set.Ioc a b)
• intervalIntegral.integral_eq_zero_iff_of_nonneg_ae 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (hf : 0 ≤ᵐ[μ.restrict (Set.Ioc a b ∪ Set.Ioc b a)] f) (hfi : IntervalIntegrable f μ a b) : ∫ (x : ℝ) in a..b, f x ∂μ = 0 ↔ f =ᵐ[μ.restrict (Set.Ioc a b ∪ Set.Ioc b a)] 0
• intervalIntegral.integral_lt_integral_of_ae_le_of_measure_setOfPred_lt_ne_zero 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {f g : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (hab : a ≤ b) (hfi : IntervalIntegrable f μ a b) (hgi : IntervalIntegrable g μ a b) (hle : f ≤ᵐ[μ.restrict (Set.Ioc a b)] g) (hlt : (μ.restrict (Set.Ioc a b)) {x | f x < g x} ≠ 0) : ∫ (x : ℝ) in a..b, f x ∂μ < ∫ (x : ℝ) in a..b, g x ∂μ
• intervalIntegral.integral_lt_integral_of_ae_le_of_measure_setOf_lt_ne_zero 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {f g : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (hab : a ≤ b) (hfi : IntervalIntegrable f μ a b) (hgi : IntervalIntegrable g μ a b) (hle : f ≤ᵐ[μ.restrict (Set.Ioc a b)] g) (hlt : (μ.restrict (Set.Ioc a b)) {x | f x < g x} ≠ 0) : ∫ (x : ℝ) in a..b, f x ∂μ < ∫ (x : ℝ) in a..b, g x ∂μ
• intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
  {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a : ℝ} {c : E} {l l' : Filter ℝ} {lt : Filter ι} {μ : MeasureTheory.Measure ℝ} {u v : ι → ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] [CompleteSpace E] [intervalIntegral.FTCFilter a l l'] (hfm : StronglyMeasurableAtFilter f l' μ) (hf : Filter.Tendsto f (l' ⊓ MeasureTheory.ae μ) (nhds c)) (hu : Filter.Tendsto u lt l) (hv : Filter.Tendsto v lt l) (huv : u ≤ᶠ[lt] v) : (fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ - μ.real (Set.Ioc (u t) (v t)) • c) =o[lt] fun t => μ.real (Set.Ioc (u t) (v t))
• intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_ge 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
  {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a : ℝ} {c : E} {l l' : Filter ℝ} {lt : Filter ι} {μ : MeasureTheory.Measure ℝ} {u v : ι → ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] [CompleteSpace E] [intervalIntegral.FTCFilter a l l'] (hfm : StronglyMeasurableAtFilter f l' μ) (hf : Filter.Tendsto f (l' ⊓ MeasureTheory.ae μ) (nhds c)) (hu : Filter.Tendsto u lt l) (hv : Filter.Tendsto v lt l) (huv : v ≤ᶠ[lt] u) : (fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ + μ.real (Set.Ioc (v t) (u t)) • c) =o[lt] fun t => μ.real (Set.Ioc (v t) (u t))
• intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le' 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
  {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {c : E} {l l' : Filter ℝ} {lt : Filter ι} {μ : MeasureTheory.Measure ℝ} {u v : ι → ℝ} [CompleteSpace E] [l'.IsMeasurablyGenerated] [Filter.TendstoIxxClass Set.Ioc l l'] (hfm : StronglyMeasurableAtFilter f l' μ) (hf : Filter.Tendsto f (l' ⊓ MeasureTheory.ae μ) (nhds c)) (hl : μ.FiniteAtFilter l') (hu : Filter.Tendsto u lt l) (hv : Filter.Tendsto v lt l) (huv : u ≤ᶠ[lt] v) : (fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ - μ.real (Set.Ioc (u t) (v t)) • c) =o[lt] fun t => μ.real (Set.Ioc (u t) (v t))
• intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_ge' 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
  {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {c : E} {l l' : Filter ℝ} {lt : Filter ι} {μ : MeasureTheory.Measure ℝ} {u v : ι → ℝ} [CompleteSpace E] [l'.IsMeasurablyGenerated] [Filter.TendstoIxxClass Set.Ioc l l'] (hfm : StronglyMeasurableAtFilter f l' μ) (hf : Filter.Tendsto f (l' ⊓ MeasureTheory.ae μ) (nhds c)) (hl : μ.FiniteAtFilter l') (hu : Filter.Tendsto u lt l) (hv : Filter.Tendsto v lt l) (huv : v ≤ᶠ[lt] u) : (fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ + μ.real (Set.Ioc (v t) (u t)) • c) =o[lt] fun t => μ.real (Set.Ioc (v t) (u t))
• LinearGrowth.linearGrowthInf_eventually_monotone 📋 Mathlib.Analysis.Asymptotics.LinearGrowth
  {u v : ℕ → EReal} (h : u ≤ᶠ[Filter.atTop] v) : LinearGrowth.linearGrowthInf u ≤ LinearGrowth.linearGrowthInf v
• LinearGrowth.linearGrowthSup_eventually_monotone 📋 Mathlib.Analysis.Asymptotics.LinearGrowth
  {u v : ℕ → EReal} (h : u ≤ᶠ[Filter.atTop] v) : LinearGrowth.linearGrowthSup u ≤ LinearGrowth.linearGrowthSup v
• LinearGrowth.le_linearGrowthInf_comp 📋 Mathlib.Analysis.Asymptotics.LinearGrowth
  {u : ℕ → EReal} {v : ℕ → ℕ} (hu : 0 ≤ᶠ[Filter.atTop] u) (hv : Filter.Tendsto v Filter.atTop Filter.atTop) : (LinearGrowth.linearGrowthInf fun n => ↑(v n)) * LinearGrowth.linearGrowthInf u ≤ LinearGrowth.linearGrowthInf (u ∘ v)
• ExpGrowth.expGrowthInf_eventually_monotone 📋 Mathlib.Analysis.Asymptotics.ExpGrowth
  {u v : ℕ → ENNReal} (h : u ≤ᶠ[Filter.atTop] v) : ExpGrowth.expGrowthInf u ≤ ExpGrowth.expGrowthInf v
• ExpGrowth.expGrowthSup_eventually_monotone 📋 Mathlib.Analysis.Asymptotics.ExpGrowth
  {u v : ℕ → ENNReal} (h : u ≤ᶠ[Filter.atTop] v) : ExpGrowth.expGrowthSup u ≤ ExpGrowth.expGrowthSup v
• ExpGrowth.le_expGrowthInf_comp 📋 Mathlib.Analysis.Asymptotics.ExpGrowth
  {u : ℕ → ENNReal} {v : ℕ → ℕ} (hu : 1 ≤ᶠ[Filter.atTop] u) (hv : Filter.Tendsto v Filter.atTop Filter.atTop) : (LinearGrowth.linearGrowthInf fun n => ↑(v n)) * ExpGrowth.expGrowthInf u ≤ ExpGrowth.expGrowthInf (u ∘ v)
• Asymptotics.SuperpolynomialDecay.trans_eventuallyLE 📋 Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
  {α : Type u_1} {β : Type u_2} {l : Filter α} {k f g g' : α → β} [TopologicalSpace β] [CommSemiring β] [PartialOrder β] [IsOrderedRing β] [OrderTopology β] (hk : 0 ≤ᶠ[l] k) (hg : Asymptotics.SuperpolynomialDecay l k g) (hg' : Asymptotics.SuperpolynomialDecay l k g') (hfg : g ≤ᶠ[l] f) (hfg' : f ≤ᶠ[l] g') : Asymptotics.SuperpolynomialDecay l k f
• Asymptotics.SuperpolynomialDecay.trans_eventually_abs_le 📋 Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
  {α : Type u_1} {β : Type u_2} {l : Filter α} {k f g : α → β} [TopologicalSpace β] [CommRing β] [LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β] (hf : Asymptotics.SuperpolynomialDecay l k f) (hfg : abs ∘ g ≤ᶠ[l] abs ∘ f) : Asymptotics.SuperpolynomialDecay l k g
• MeasureTheory.laverage_mono_ae 📋 Mathlib.MeasureTheory.Integral.Average
  {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} (h : f ≤ᵐ[μ] g) : ⨍⁻ (a : α), f a ∂μ ≤ ⨍⁻ (a : α), g a ∂μ
• MeasureTheory.setLAverage_mono_ae 📋 Mathlib.MeasureTheory.Integral.Average
  {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} (s : Set α) (h : f ≤ᵐ[μ] g) : ⨍⁻ (a : α) in s, f a ∂μ ≤ ⨍⁻ (a : α) in s, g a ∂μ
• MeasureTheory.ofReal_average 📋 Mathlib.MeasureTheory.Integral.Average
  {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.Integrable f μ) (hf₀ : 0 ≤ᵐ[μ] f) : ENNReal.ofReal (⨍ (x : α), f x ∂μ) = (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) / μ Set.univ
• MeasureTheory.ofReal_setAverage 📋 Mathlib.MeasureTheory.Integral.Average
  {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ℝ} (hf : MeasureTheory.IntegrableOn f s μ) (hf₀ : 0 ≤ᵐ[μ.restrict s] f) : ENNReal.ofReal (⨍ (x : α) in s, f x ∂μ) = (∫⁻ (x : α) in s, ENNReal.ofReal (f x) ∂μ) / μ s
• MeasureTheory.average_nonneg_of_ae 📋 Mathlib.MeasureTheory.Integral.Average
  {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure α} {f : α → E} [PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] [ClosedIciTopology E] (hf : 0 ≤ᵐ[μ] f) : 0 ≤ ⨍ (a : α), f a ∂μ
• MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite 📋 Mathlib.MeasureTheory.Function.AEEqOfLIntegral
  {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {f g : α → ENNReal} (hf : Measurable f) (h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ) : f ≤ᵐ[μ] g
• MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀ 📋 Mathlib.MeasureTheory.Function.AEEqOfLIntegral
  {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {f g : α → ENNReal} (hf : AEMeasurable f μ) (h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ) : f ≤ᵐ[μ] g
• MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul' 📋 Mathlib.MeasureTheory.Function.JacobianOneDim
  {f : ℝ → ℝ} (hf : MeasurableEmbedding f) {s : Set ℝ} (hs : MeasurableSet s) {f' : ℝ → ℝ} (hf' : ∀ (x : ℝ), HasDerivAt f (f' x) x) {g : ℝ → ℝ} (hg : 0 ≤ᵐ[MeasureTheory.volume] g) (hg_int : MeasureTheory.Integrable g MeasureTheory.volume) : (MeasureTheory.Measure.comap f (MeasureTheory.volume.withDensity fun x => ENNReal.ofReal (g x))) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))
• MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul' 📋 Mathlib.MeasureTheory.Function.JacobianOneDim
  (f : ℝ ≃ᵐ ℝ) {s : Set ℝ} (hs : MeasurableSet s) {f' : ℝ → ℝ} (hf' : ∀ (x : ℝ), HasDerivAt (⇑f) (f' x) x) {g : ℝ → ℝ} (hg : 0 ≤ᵐ[MeasureTheory.volume] g) (hg_int : MeasureTheory.Integrable g MeasureTheory.volume) : (MeasureTheory.Measure.map (⇑f.symm) (MeasureTheory.volume.withDensity fun x => ENNReal.ofReal (g x))) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))
• MeasureTheory.AECover.integral_eq_of_tendsto_of_nonneg_ae 📋 Mathlib.MeasureTheory.Integral.IntegralEqImproper
  {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι} [l.NeBot] [l.IsCountablyGenerated] {φ : ι → Set α} (hφ : MeasureTheory.AECover μ l φ) {f : α → ℝ} (I : ℝ) (hnng : 0 ≤ᵐ[μ] f) (hfi : ∀ (n : ι), MeasureTheory.IntegrableOn f (φ n) μ) (htendsto : Filter.Tendsto (fun n => ∫ (x : α) in φ n, f x ∂μ) l (nhds I)) : ∫ (x : α), f x ∂μ = I
• Filter.eventually_sub_nonneg 📋 Mathlib.Order.Filter.Ring
  {α : Type u} {β : Type v} [AddGroup β] [LE β] [AddRightMono β] {l : Filter α} {f g : α → β} : 0 ≤ᶠ[l] g - f ↔ f ≤ᶠ[l] g
• Filter.EventuallyLE.add_le_add 📋 Mathlib.Order.Filter.Ring
  {α : Type u} {β : Type v} [Add β] [Preorder β] [AddLeftMono β] [AddRightMono β] {l : Filter α} {f₁ f₂ g₁ g₂ : α → β} (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) : f₁ + g₁ ≤ᶠ[l] f₂ + g₂
• Filter.EventuallyLE.mul_le_mul' 📋 Mathlib.Order.Filter.Ring
  {α : Type u} {β : Type v} [Mul β] [Preorder β] [MulLeftMono β] [MulRightMono β] {l : Filter α} {f₁ f₂ g₁ g₂ : α → β} (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) : f₁ * g₁ ≤ᶠ[l] f₂ * g₂
• Filter.EventuallyLE.mul_nonneg 📋 Mathlib.Order.Filter.Ring
  {α : Type u} {β : Type v} [Semiring β] [PartialOrder β] [IsOrderedRing β] {l : Filter α} {f g : α → β} (hf : 0 ≤ᶠ[l] f) (hg : 0 ≤ᶠ[l] g) : 0 ≤ᶠ[l] f * g
• Filter.EventuallyLE.mul_le_mul 📋 Mathlib.Order.Filter.Ring
  {α : Type u} {β : Type v} [MulZeroClass β] [Preorder β] [PosMulMono β] [MulPosMono β] {l : Filter α} {f₁ f₂ g₁ g₂ : α → β} (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) (hg₀ : 0 ≤ᶠ[l] g₁) (hf₀ : 0 ≤ᶠ[l] f₂) : f₁ * g₁ ≤ᶠ[l] f₂ * g₂
• MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg 📋 Mathlib.MeasureTheory.Function.AEEqOfIntegral
  {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.Integrable f μ) (hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ) : 0 ≤ᵐ[μ] f
• MeasureTheory.ae_nonneg_restrict_of_forall_setIntegral_nonneg_inter 📋 Mathlib.MeasureTheory.Function.AEEqOfIntegral
  {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} {t : Set α} (hf : MeasureTheory.IntegrableOn f t μ) (hf_zero : ∀ (s : Set α), MeasurableSet s → μ (s ∩ t) < ⊤ → 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ) : 0 ≤ᵐ[μ.restrict t] f

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c