Loogle!

Result

Found 46 declarations mentioning intervalIntegral and Filter.Tendsto.

• intervalIntegral.tendsto_integral_filter_of_dominated_convergence 📋 Mathlib.MeasureTheory.Integral.DominatedConvergence
  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} {μ : MeasureTheory.Measure ℝ} {ι : Type u_3} {l : Filter ι} [l.IsCountablyGenerated] {F : ι → ℝ → E} (bound : ℝ → ℝ) (hF_meas : ∀ᶠ (n : ι) in l, MeasureTheory.AEStronglyMeasurable (F n) (μ.restrict (Set.uIoc a b))) (h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ, x ∈ Set.uIoc a b → ‖F n x‖ ≤ bound x) (bound_integrable : IntervalIntegrable bound μ a b) (h_lim : ∀ᵐ (x : ℝ) ∂μ, x ∈ Set.uIoc a b → Filter.Tendsto (fun n => F n x) l (nhds (f x))) : Filter.Tendsto (fun n => ∫ (x : ℝ) in a..b, F n x ∂μ) l (nhds (∫ (x : ℝ) in a..b, f x ∂μ))
• intervalIntegral.deriv_integral_of_tendsto_ae_right 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {c : E} {a b : ℝ} (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas : StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume) (hb : Filter.Tendsto f (nhds b ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c)) : deriv (fun u => ∫ (x : ℝ) in a..u, f x) b = c
• intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae 📋 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 μ] [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) : (fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ - ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] fun t => ∫ (x : ℝ) in u t..v t, 1 ∂μ
• intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae' 📋 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 : ι → ℝ} [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) : (fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ - ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] fun t => ∫ (x : ℝ) in u t..v t, 1 ∂μ
• intervalIntegral.deriv_integral_of_tendsto_ae_left 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {c : E} {a b : ℝ} (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas : StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume) (hb : Filter.Tendsto f (nhds a ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c)) : deriv (fun u => ∫ (x : ℝ) in u..b, f x) a = -c
• intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
  {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {c : E} {lb lb' : Filter ℝ} {lt : Filter ι} {μ : MeasureTheory.Measure ℝ} {u v : ι → ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] [intervalIntegral.FTCFilter b lb lb'] (hab : IntervalIntegrable f μ a b) (hmeas : StronglyMeasurableAtFilter f lb' μ) (hf : Filter.Tendsto f (lb' ⊓ MeasureTheory.ae μ) (nhds c)) (hu : Filter.Tendsto u lt lb) (hv : Filter.Tendsto v lt lb) : (fun t => ∫ (x : ℝ) in a..v t, f x ∂μ - ∫ (x : ℝ) in a..u t, f x ∂μ - ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] fun t => ∫ (x : ℝ) in u t..v t, 1 ∂μ
• intervalIntegral.derivWithin_integral_of_tendsto_ae_right 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {c : E} {a b : ℝ} (hf : IntervalIntegrable f MeasureTheory.volume a b) {s t : Set ℝ} [intervalIntegral.FTCFilter b (nhdsWithin b s) (nhdsWithin b t)] (hmeas : StronglyMeasurableAtFilter f (nhdsWithin b t) MeasureTheory.volume) (hb : Filter.Tendsto f (nhdsWithin b t ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c)) (hs : UniqueDiffWithinAt ℝ s b := by uniqueDiffWithinAt_Ici_Iic_univ) : derivWithin (fun u => ∫ (x : ℝ) in a..u, f x) s b = c
• intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_left 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
  {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {c : E} {la la' : Filter ℝ} {lt : Filter ι} {μ : MeasureTheory.Measure ℝ} {u v : ι → ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] [intervalIntegral.FTCFilter a la la'] (hab : IntervalIntegrable f μ a b) (hmeas : StronglyMeasurableAtFilter f la' μ) (hf : Filter.Tendsto f (la' ⊓ MeasureTheory.ae μ) (nhds c)) (hu : Filter.Tendsto u lt la) (hv : Filter.Tendsto v lt la) : (fun t => ∫ (x : ℝ) in v t..b, f x ∂μ - ∫ (x : ℝ) in u t..b, f x ∂μ + ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] fun t => ∫ (x : ℝ) in u t..v t, 1 ∂μ
• intervalIntegral.derivWithin_integral_of_tendsto_ae_left 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {c : E} {a b : ℝ} (hf : IntervalIntegrable f MeasureTheory.volume a b) {s t : Set ℝ} [intervalIntegral.FTCFilter a (nhdsWithin a s) (nhdsWithin a t)] (hmeas : StronglyMeasurableAtFilter f (nhdsWithin a t) MeasureTheory.volume) (ha : Filter.Tendsto f (nhdsWithin a t ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c)) (hs : UniqueDiffWithinAt ℝ s a := by uniqueDiffWithinAt_Ici_Iic_univ) : derivWithin (fun u => ∫ (x : ℝ) in u..b, f x) s a = -c
• intervalIntegral.integral_hasDerivAt_of_tendsto_ae_right 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {c : E} {a b : ℝ} (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas : StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume) (hb : Filter.Tendsto f (nhds b ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c)) : HasDerivAt (fun u => ∫ (x : ℝ) in a..u, f x) c b
• intervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_right 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {c : E} {a b : ℝ} (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas : StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume) (hb : Filter.Tendsto f (nhds b ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c)) : HasStrictDerivAt (fun u => ∫ (x : ℝ) in a..u, f x) c b
• intervalIntegral.integral_hasDerivAt_of_tendsto_ae_left 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {c : E} {a b : ℝ} (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas : StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume) (ha : Filter.Tendsto f (nhds a ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c)) : HasDerivAt (fun u => ∫ (x : ℝ) in u..b, f x) (-c) a
• intervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_left 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {c : E} {a b : ℝ} (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas : StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume) (ha : Filter.Tendsto f (nhds a ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c)) : HasStrictDerivAt (fun u => ∫ (x : ℝ) in u..b, f x) (-c) a
• intervalIntegral.integral_eq_sub_of_hasDerivAt_of_tendsto 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] {f f' : ℝ → E} (hab : a < b) {fa fb : E} (hderiv : ∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x) (hint : IntervalIntegrable f' MeasureTheory.volume a b) (ha : Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds fa)) (hb : Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds fb)) : ∫ (y : ℝ) in a..b, f' y = fb - fa
• intervalIntegral.integral_hasDerivWithinAt_of_tendsto_ae_right 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {c : E} {a b : ℝ} (hf : IntervalIntegrable f MeasureTheory.volume a b) {s t : Set ℝ} [intervalIntegral.FTCFilter b (nhdsWithin b s) (nhdsWithin b t)] (hmeas : StronglyMeasurableAtFilter f (nhdsWithin b t) MeasureTheory.volume) (hb : Filter.Tendsto f (nhdsWithin b t ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c)) : HasDerivWithinAt (fun u => ∫ (x : ℝ) in a..u, f x) c s b
• intervalIntegral.integral_hasDerivWithinAt_of_tendsto_ae_left 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {c : E} {a b : ℝ} (hf : IntervalIntegrable f MeasureTheory.volume a b) {s t : Set ℝ} [intervalIntegral.FTCFilter a (nhdsWithin a s) (nhdsWithin a t)] (hmeas : StronglyMeasurableAtFilter f (nhdsWithin a t) MeasureTheory.volume) (ha : Filter.Tendsto f (nhdsWithin a t ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c)) : HasDerivWithinAt (fun u => ∫ (x : ℝ) in u..b, f x) (-c) s a
• 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.integral_sub_linear_isLittleO_of_tendsto_ae 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
  {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {c : E} {l l' : Filter ℝ} {lt : Filter ι} {a : ℝ} [intervalIntegral.FTCFilter a l l'] (hfm : StronglyMeasurableAtFilter f l' MeasureTheory.volume) (hf : Filter.Tendsto f (l' ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c)) {u v : ι → ℝ} (hu : Filter.Tendsto u lt l) (hv : Filter.Tendsto v lt l) : (fun t => (∫ (x : ℝ) in u t..v t, f x) - (v t - u t) • c) =o[lt] (v - u)
• 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_integral_sub_linear_isLittleO_of_tendsto_ae 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
  {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {ca cb : E} {la la' lb lb' : Filter ℝ} {lt : Filter ι} {μ : MeasureTheory.Measure ℝ} {ua va ub vb : ι → ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] [intervalIntegral.FTCFilter a la la'] [intervalIntegral.FTCFilter b lb lb'] (hab : IntervalIntegrable f μ a b) (hmeas_a : StronglyMeasurableAtFilter f la' μ) (hmeas_b : StronglyMeasurableAtFilter f lb' μ) (ha_lim : Filter.Tendsto f (la' ⊓ MeasureTheory.ae μ) (nhds ca)) (hb_lim : Filter.Tendsto f (lb' ⊓ MeasureTheory.ae μ) (nhds cb)) (hua : Filter.Tendsto ua lt la) (hva : Filter.Tendsto va lt la) (hub : Filter.Tendsto ub lt lb) (hvb : Filter.Tendsto vb lt lb) : (fun t => ∫ (x : ℝ) in va t..vb t, f x ∂μ - ∫ (x : ℝ) in ua t..ub t, f x ∂μ - (∫ (x : ℝ) in ub t..vb t, cb ∂μ - ∫ (x : ℝ) in ua t..va t, ca ∂μ)) =o[lt] fun t => ‖∫ (x : ℝ) in ua t..va t, 1 ∂μ‖ + ‖∫ (x : ℝ) in ub t..vb t, 1 ∂μ‖
• 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_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))
• intervalIntegral.integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
  {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {c : E} {lb lb' : Filter ℝ} {lt : Filter ι} {a b : ℝ} {u v : ι → ℝ} [intervalIntegral.FTCFilter b lb lb'] (hab : IntervalIntegrable f MeasureTheory.volume a b) (hmeas : StronglyMeasurableAtFilter f lb' MeasureTheory.volume) (hf : Filter.Tendsto f (lb' ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c)) (hu : Filter.Tendsto u lt lb) (hv : Filter.Tendsto v lt lb) : (fun t => ((∫ (x : ℝ) in a..v t, f x) - ∫ (x : ℝ) in a..u t, f x) - (v t - u t) • c) =o[lt] (v - u)
• intervalIntegral.integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_left 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
  {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {c : E} {la la' : Filter ℝ} {lt : Filter ι} {a b : ℝ} {u v : ι → ℝ} [intervalIntegral.FTCFilter a la la'] (hab : IntervalIntegrable f MeasureTheory.volume a b) (hmeas : StronglyMeasurableAtFilter f la' MeasureTheory.volume) (hf : Filter.Tendsto f (la' ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c)) (hu : Filter.Tendsto u lt la) (hv : Filter.Tendsto v lt la) : (fun t => ((∫ (x : ℝ) in v t..b, f x) - ∫ (x : ℝ) in u t..b, f x) + (v t - u t) • c) =o[lt] (v - u)
• intervalIntegral.integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
  {ι : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {ca cb : E} {la la' lb lb' : Filter ℝ} {lt : Filter ι} {a b : ℝ} {ua ub va vb : ι → ℝ} [intervalIntegral.FTCFilter a la la'] [intervalIntegral.FTCFilter b lb lb'] (hab : IntervalIntegrable f MeasureTheory.volume a b) (hmeas_a : StronglyMeasurableAtFilter f la' MeasureTheory.volume) (hmeas_b : StronglyMeasurableAtFilter f lb' MeasureTheory.volume) (ha_lim : Filter.Tendsto f (la' ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds ca)) (hb_lim : Filter.Tendsto f (lb' ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds cb)) (hua : Filter.Tendsto ua lt la) (hva : Filter.Tendsto va lt la) (hub : Filter.Tendsto ub lt lb) (hvb : Filter.Tendsto vb lt lb) : (fun t => ((∫ (x : ℝ) in va t..vb t, f x) - ∫ (x : ℝ) in ua t..ub t, f x) - ((vb t - ub t) • cb - (va t - ua t) • ca)) =o[lt] fun t => ‖va t - ua t‖ + ‖vb t - ub t‖
• intervalIntegral.integral_hasFDerivWithinAt 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {la lb : Filter ℝ} {a b : ℝ} (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas_a : StronglyMeasurableAtFilter f la MeasureTheory.volume) (hmeas_b : StronglyMeasurableAtFilter f lb MeasureTheory.volume) {s t : Set ℝ} [intervalIntegral.FTCFilter a (nhdsWithin a s) la] [intervalIntegral.FTCFilter b (nhdsWithin b t) lb] (ha : Filter.Tendsto f la (nhds (f a))) (hb : Filter.Tendsto f lb (nhds (f b))) : HasFDerivWithinAt (fun p => ∫ (x : ℝ) in p.1..p.2, f x) ((ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight (f b) - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight (f a)) (s ×ˢ t) (a, b)
• intervalIntegral.integral_hasFDerivAt_of_tendsto_ae 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {ca cb : E} {a b : ℝ} (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas_a : StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume) (hmeas_b : StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume) (ha : Filter.Tendsto f (nhds a ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds ca)) (hb : Filter.Tendsto f (nhds b ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds cb)) : HasFDerivAt (fun p => ∫ (x : ℝ) in p.1..p.2, f x) ((ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight cb - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight ca) (a, b)
• intervalIntegral.integral_hasStrictFDerivAt_of_tendsto_ae 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {ca cb : E} {a b : ℝ} (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas_a : StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume) (hmeas_b : StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume) (ha : Filter.Tendsto f (nhds a ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds ca)) (hb : Filter.Tendsto f (nhds b ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds cb)) : HasStrictFDerivAt (fun p => ∫ (x : ℝ) in p.1..p.2, f x) ((ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight cb - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight ca) (a, b)
• intervalIntegral.integral_hasFDerivWithinAt_of_tendsto_ae 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {ca cb : E} {la lb : Filter ℝ} {a b : ℝ} (hf : IntervalIntegrable f MeasureTheory.volume a b) {s t : Set ℝ} [intervalIntegral.FTCFilter a (nhdsWithin a s) la] [intervalIntegral.FTCFilter b (nhdsWithin b t) lb] (hmeas_a : StronglyMeasurableAtFilter f la MeasureTheory.volume) (hmeas_b : StronglyMeasurableAtFilter f lb MeasureTheory.volume) (ha : Filter.Tendsto f (la ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds ca)) (hb : Filter.Tendsto f (lb ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds cb)) : HasFDerivWithinAt (fun p => ∫ (x : ℝ) in p.1..p.2, f x) ((ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight cb - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight ca) (s ×ˢ t) (a, b)
• intervalIntegral.fderiv_integral_of_tendsto_ae 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {ca cb : E} {a b : ℝ} (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas_a : StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume) (hmeas_b : StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume) (ha : Filter.Tendsto f (nhds a ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds ca)) (hb : Filter.Tendsto f (nhds b ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds cb)) : fderiv ℝ (fun p => ∫ (x : ℝ) in p.1..p.2, f x) (a, b) = (ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight cb - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight ca
• intervalIntegral.fderivWithin_integral_of_tendsto_ae 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {ca cb : E} {la lb : Filter ℝ} {a b : ℝ} (hf : IntervalIntegrable f MeasureTheory.volume a b) (hmeas_a : StronglyMeasurableAtFilter f la MeasureTheory.volume) (hmeas_b : StronglyMeasurableAtFilter f lb MeasureTheory.volume) {s t : Set ℝ} [intervalIntegral.FTCFilter a (nhdsWithin a s) la] [intervalIntegral.FTCFilter b (nhdsWithin b t) lb] (ha : Filter.Tendsto f (la ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds ca)) (hb : Filter.Tendsto f (lb ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds cb)) (hs : UniqueDiffWithinAt ℝ s a := by uniqueDiffWithinAt_Ici_Iic_univ) (ht : UniqueDiffWithinAt ℝ t b := by uniqueDiffWithinAt_Ici_Iic_univ) : fderivWithin ℝ (fun p => ∫ (x : ℝ) in p.1..p.2, f x) (s ×ˢ t) (a, b) = (ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight cb - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight ca
• MeasureTheory.intervalIntegral_tendsto_integral 📋 Mathlib.MeasureTheory.Integral.IntegralEqImproper
  {ι : Type u_1} {E : Type u_2} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [l.IsCountablyGenerated] [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ι → ℝ} {f : ℝ → E} (hfi : MeasureTheory.Integrable f μ) (ha : Filter.Tendsto a l Filter.atBot) (hb : Filter.Tendsto b l Filter.atTop) : Filter.Tendsto (fun i => ∫ (x : ℝ) in a i..b i, f x ∂μ) l (nhds (∫ (x : ℝ), f x ∂μ))
• MeasureTheory.intervalIntegral_tendsto_integral_Iic 📋 Mathlib.MeasureTheory.Integral.IntegralEqImproper
  {ι : Type u_1} {E : Type u_2} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [l.IsCountablyGenerated] [NormedAddCommGroup E] [NormedSpace ℝ E] {a : ι → ℝ} {f : ℝ → E} (b : ℝ) (hfi : MeasureTheory.IntegrableOn f (Set.Iic b) μ) (ha : Filter.Tendsto a l Filter.atBot) : Filter.Tendsto (fun i => ∫ (x : ℝ) in a i..b, f x ∂μ) l (nhds (∫ (x : ℝ) in Set.Iic b, f x ∂μ))
• MeasureTheory.intervalIntegral_tendsto_integral_Ioi 📋 Mathlib.MeasureTheory.Integral.IntegralEqImproper
  {ι : Type u_1} {E : Type u_2} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [l.IsCountablyGenerated] [NormedAddCommGroup E] [NormedSpace ℝ E] {b : ι → ℝ} {f : ℝ → E} (a : ℝ) (hfi : MeasureTheory.IntegrableOn f (Set.Ioi a) μ) (hb : Filter.Tendsto b l Filter.atTop) : Filter.Tendsto (fun i => ∫ (x : ℝ) in a..b i, f x ∂μ) l (nhds (∫ (x : ℝ) in Set.Ioi a, f x ∂μ))
• MeasureTheory.integrableOn_Iic_of_intervalIntegral_norm_bounded 📋 Mathlib.MeasureTheory.Integral.IntegralEqImproper
  {ι : Type u_1} {E : Type u_2} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [l.NeBot] [l.IsCountablyGenerated] [NormedAddCommGroup E] {a : ι → ℝ} {f : ℝ → E} (I b : ℝ) (hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc (a i) b) μ) (ha : Filter.Tendsto a l Filter.atBot) (h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I) : MeasureTheory.IntegrableOn f (Set.Iic b) μ
• MeasureTheory.integrableOn_Ioi_of_intervalIntegral_norm_bounded 📋 Mathlib.MeasureTheory.Integral.IntegralEqImproper
  {ι : Type u_1} {E : Type u_2} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [l.NeBot] [l.IsCountablyGenerated] [NormedAddCommGroup E] {b : ι → ℝ} {f : ℝ → E} (I a : ℝ) (hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc a (b i)) μ) (hb : Filter.Tendsto b l Filter.atTop) (h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I) : MeasureTheory.IntegrableOn f (Set.Ioi a) μ
• MeasureTheory.integrableOn_Iic_of_intervalIntegral_norm_tendsto 📋 Mathlib.MeasureTheory.Integral.IntegralEqImproper
  {ι : Type u_1} {E : Type u_2} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [l.NeBot] [l.IsCountablyGenerated] [NormedAddCommGroup E] {a : ι → ℝ} {f : ℝ → E} (I b : ℝ) (hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc (a i) b) μ) (ha : Filter.Tendsto a l Filter.atBot) (h : Filter.Tendsto (fun i => ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ) l (nhds I)) : MeasureTheory.IntegrableOn f (Set.Iic b) μ
• MeasureTheory.integrableOn_Ioi_of_intervalIntegral_norm_tendsto 📋 Mathlib.MeasureTheory.Integral.IntegralEqImproper
  {ι : Type u_1} {E : Type u_2} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [l.NeBot] [l.IsCountablyGenerated] [NormedAddCommGroup E] {b : ι → ℝ} {f : ℝ → E} (I a : ℝ) (hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc a (b i)) μ) (hb : Filter.Tendsto b l Filter.atTop) (h : Filter.Tendsto (fun i => ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ) l (nhds I)) : MeasureTheory.IntegrableOn f (Set.Ioi a) μ
• MeasureTheory.integrable_of_intervalIntegral_norm_bounded 📋 Mathlib.MeasureTheory.Integral.IntegralEqImproper
  {ι : Type u_1} {E : Type u_2} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [l.NeBot] [l.IsCountablyGenerated] [NormedAddCommGroup E] {a b : ι → ℝ} {f : ℝ → E} (I : ℝ) (hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc (a i) (b i)) μ) (ha : Filter.Tendsto a l Filter.atBot) (hb : Filter.Tendsto b l Filter.atTop) (h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I) : MeasureTheory.Integrable f μ
• MeasureTheory.integrable_of_intervalIntegral_norm_tendsto 📋 Mathlib.MeasureTheory.Integral.IntegralEqImproper
  {ι : Type u_1} {E : Type u_2} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [l.NeBot] [l.IsCountablyGenerated] [NormedAddCommGroup E] {a b : ι → ℝ} {f : ℝ → E} (I : ℝ) (hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc (a i) (b i)) μ) (ha : Filter.Tendsto a l Filter.atBot) (hb : Filter.Tendsto b l Filter.atTop) (h : Filter.Tendsto (fun i => ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ) l (nhds I)) : MeasureTheory.Integrable f μ
• Function.Periodic.tendsto_atBot_intervalIntegral_of_pos 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
  {T : ℝ} {g : ℝ → ℝ} (hg : Function.Periodic g T) (h₀ : 0 < ∫ (x : ℝ) in 0..T, g x) (hT : 0 < T) : Filter.Tendsto (fun t => ∫ (x : ℝ) in 0..t, g x) Filter.atBot Filter.atBot
• Function.Periodic.tendsto_atBot_intervalIntegral_of_pos' 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
  {T : ℝ} {g : ℝ → ℝ} (hg : Function.Periodic g T) (h_int : IntervalIntegrable g MeasureTheory.volume 0 T) (h₀ : ∀ (x : ℝ), 0 < g x) (hT : 0 < T) : Filter.Tendsto (fun t => ∫ (x : ℝ) in 0..t, g x) Filter.atBot Filter.atBot
• Function.Periodic.tendsto_atTop_intervalIntegral_of_pos 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
  {T : ℝ} {g : ℝ → ℝ} (hg : Function.Periodic g T) (h₀ : 0 < ∫ (x : ℝ) in 0..T, g x) (hT : 0 < T) : Filter.Tendsto (fun t => ∫ (x : ℝ) in 0..t, g x) Filter.atTop Filter.atTop
• Function.Periodic.tendsto_atTop_intervalIntegral_of_pos' 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
  {T : ℝ} {g : ℝ → ℝ} (hg : Function.Periodic g T) (h_int : IntervalIntegrable g MeasureTheory.volume 0 T) (h₀ : ∀ (x : ℝ), 0 < g x) (hT : 0 < T) : Filter.Tendsto (fun t => ∫ (x : ℝ) in 0..t, g x) Filter.atTop Filter.atTop
• EulerSine.tendsto_integral_cos_pow_mul_div 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
  {f : ℝ → ℂ} (hf : ContinuousOn f (Set.Icc 0 (Real.pi / 2))) : Filter.Tendsto (fun n => (∫ (x : ℝ) in 0..Real.pi / 2, ↑(Real.cos x) ^ n * f x) / ↑(∫ (x : ℝ) in 0..Real.pi / 2, Real.cos x ^ n)) Filter.atTop (nhds (f 0))
• Complex.approx_Gamma_integral_tendsto_Gamma_integral 📋 Mathlib.Analysis.SpecialFunctions.Gamma.Beta
  {s : ℂ} (hs : 0 < s.re) : Filter.Tendsto (fun n => ∫ (x : ℝ) in 0..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) Filter.atTop (nhds (Complex.Gamma s))

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. 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.

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.

This is Loogle revision 187ba29 serving mathlib revision df9f011