Loogle!

Result

Found 89 declarations mentioning MeasureTheory.LocallyIntegrable.

• MeasureTheory.LocallyIntegrable 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] (f : X → ε) (μ : MeasureTheory.Measure X := by volume_tac) : Prop
• MeasureTheory.Integrable.locallyIntegrable 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} (hf : MeasureTheory.Integrable f μ) : MeasureTheory.LocallyIntegrable f μ
• MeasureTheory.locallyIntegrableOn_univ 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} : MeasureTheory.LocallyIntegrableOn f Set.univ μ ↔ MeasureTheory.LocallyIntegrable f μ
• MeasureTheory.LocallyIntegrable.locallyIntegrableOn 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} (hf : MeasureTheory.LocallyIntegrable f μ) (s : Set X) : MeasureTheory.LocallyIntegrableOn f s μ
• MeasureTheory.LocallyIntegrable.aestronglyMeasurable 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} [TopologicalSpace.PseudoMetrizableSpace ε] [SecondCountableTopology X] (hf : MeasureTheory.LocallyIntegrable f μ) : MeasureTheory.AEStronglyMeasurable f μ
• MeasureTheory.locallyIntegrable_const 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} [MeasureTheory.IsLocallyFiniteMeasure μ] (c : E) : MeasureTheory.LocallyIntegrable (fun x => c) μ
• MeasureTheory.locallyIntegrable_zero 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {ε'' : Type u_5} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε''] [ESeminormedAddMonoid ε''] {μ : MeasureTheory.Measure X} : MeasureTheory.LocallyIntegrable (fun x => 0) μ
• MeasureTheory.locallyIntegrable_const_enorm 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {μ : MeasureTheory.Measure X} [MeasureTheory.IsLocallyFiniteMeasure μ] {c : ε} (hc : ‖c‖ₑ ≠ ⊤) : MeasureTheory.LocallyIntegrable (fun x => c) μ
• MeasureTheory.LocallyIntegrable.integrableOn_isCompact 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} [TopologicalSpace.PseudoMetrizableSpace ε] {k : Set X} (hf : MeasureTheory.LocallyIntegrable f μ) (hk : IsCompact k) : MeasureTheory.IntegrableOn f k μ
• MeasureTheory.locallyIntegrableOn_of_locallyIntegrable_restrict 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} {s : Set X} [OpensMeasurableSpace X] (hf : MeasureTheory.LocallyIntegrable f (μ.restrict s)) : MeasureTheory.LocallyIntegrableOn f s μ
• MeasureTheory.locallyIntegrable_iff 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} [TopologicalSpace.PseudoMetrizableSpace ε] [LocallyCompactSpace X] : MeasureTheory.LocallyIntegrable f μ ↔ ∀ (k : Set X), IsCompact k → MeasureTheory.IntegrableOn f k μ
• MeasureTheory.integrable_iff_integrableAtFilter_cocompact 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} [TopologicalSpace.PseudoMetrizableSpace ε] : MeasureTheory.Integrable f μ ↔ MeasureTheory.IntegrableAtFilter f (Filter.cocompact X) μ ∧ MeasureTheory.LocallyIntegrable f μ
• MeasureTheory.locallyIntegrableOn_iff_locallyIntegrable_restrict 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} {s : Set X} [OpensMeasurableSpace X] (hs : IsClosed s) : MeasureTheory.LocallyIntegrableOn f s μ ↔ MeasureTheory.LocallyIntegrable f (μ.restrict s)
• MeasureTheory.LocallyIntegrable.congr 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f g : X → ε} {μ : MeasureTheory.Measure X} (hf : MeasureTheory.LocallyIntegrable f μ) (h : f =ᵐ[μ] g) : MeasureTheory.LocallyIntegrable g μ
• MeasureTheory.MemLp.locallyIntegrable 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} [MeasureTheory.IsLocallyFiniteMeasure μ] {p : ENNReal} (hf : MeasureTheory.MemLp f p μ) (hp : 1 ≤ p) : MeasureTheory.LocallyIntegrable f μ
• MeasureTheory.locallyIntegrable_congr 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f g : X → ε} {μ : MeasureTheory.Measure X} (h : f =ᵐ[μ] g) : MeasureTheory.LocallyIntegrable f μ ↔ MeasureTheory.LocallyIntegrable g μ
• MeasureTheory.LocallyIntegrable.mono_measure 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ ν : MeasureTheory.Measure X} (hf : MeasureTheory.LocallyIntegrable f μ) (h : ν ≤ μ) : MeasureTheory.LocallyIntegrable f ν
• MeasureTheory.LocallyIntegrable.indicator 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {ε'' : Type u_5} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε''] [ESeminormedAddMonoid ε''] {μ : MeasureTheory.Measure X} {f : X → ε''} (hf : MeasureTheory.LocallyIntegrable f μ) {s : Set X} (hs : MeasurableSet s) : MeasureTheory.LocallyIntegrable (s.indicator f) μ
• MeasureTheory.LocallyIntegrable.integrableOn_nhds_isCompact 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} [TopologicalSpace.PseudoMetrizableSpace ε] (hf : MeasureTheory.LocallyIntegrable f μ) {k : Set X} (hk : IsCompact k) : ∃ u, IsOpen u ∧ k ⊆ u ∧ MeasureTheory.IntegrableOn f u μ
• MeasureTheory.LocallyIntegrable.exists_nat_integrableOn 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} [SecondCountableTopology X] (hf : MeasureTheory.LocallyIntegrable f μ) : ∃ u, (∀ (n : ℕ), IsOpen (u n)) ∧ ⋃ n, u n = Set.univ ∧ ∀ (n : ℕ), MeasureTheory.IntegrableOn f (u n) μ
• Continuous.locallyIntegrable 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {f : X → E} [MeasureTheory.IsLocallyFiniteMeasure μ] [SecondCountableTopologyEither X E] (hf : Continuous f) : MeasureTheory.LocallyIntegrable f μ
• MeasureTheory.LocallyIntegrable.neg 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} {f : X → E} (hf : MeasureTheory.LocallyIntegrable f μ) : MeasureTheory.LocallyIntegrable (-f) μ
• MeasureTheory.locallyIntegrable_neg_iff 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} {f : X → E} : MeasureTheory.LocallyIntegrable (-f) μ ↔ MeasureTheory.LocallyIntegrable f μ
• MeasureTheory.LocallyIntegrable.mono_enorm 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {ε : Type u_3} {ε' : Type u_4} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] [TopologicalSpace ε'] [ContinuousENorm ε'] {f : X → ε} {μ : MeasureTheory.Measure X} (hf : MeasureTheory.LocallyIntegrable f μ) {g : X → ε'} (hg : MeasureTheory.AEStronglyMeasurable g μ) (h : ∀ᵐ (x : X) ∂μ, ‖g x‖ₑ ≤ ‖f x‖ₑ) : MeasureTheory.LocallyIntegrable g μ
• MeasureTheory.locallyIntegrable_finsetSum 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] {μ : MeasureTheory.Measure X} {ε''' : Type u_9} [TopologicalSpace ε'''] [ESeminormedAddCommMonoid ε'''] [ContinuousAdd ε'''] {ι : Type u_10} (s : Finset ι) {f : ι → X → ε'''} (hf : ∀ i ∈ s, MeasureTheory.LocallyIntegrable (f i) μ) : MeasureTheory.LocallyIntegrable (fun a => ∑ i ∈ s, f i a) μ
• MeasureTheory.locallyIntegrable_finset_sum 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] {μ : MeasureTheory.Measure X} {ε''' : Type u_9} [TopologicalSpace ε'''] [ESeminormedAddCommMonoid ε'''] [ContinuousAdd ε'''] {ι : Type u_10} (s : Finset ι) {f : ι → X → ε'''} (hf : ∀ i ∈ s, MeasureTheory.LocallyIntegrable (f i) μ) : MeasureTheory.LocallyIntegrable (fun a => ∑ i ∈ s, f i a) μ
• MeasureTheory.LocallyIntegrable.add 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {ε'' : Type u_5} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε''] [ESeminormedAddMonoid ε''] {μ : MeasureTheory.Measure X} [ContinuousAdd ε''] {f g : X → ε''} (hf : MeasureTheory.LocallyIntegrable f μ) (hg : MeasureTheory.LocallyIntegrable g μ) : MeasureTheory.LocallyIntegrable (f + g) μ
• MeasureTheory.integrable_iff_integrableAtFilter_atBot 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} [TopologicalSpace.PseudoMetrizableSpace ε] [LinearOrder X] [OrderTop X] [CompactIccSpace X] : MeasureTheory.Integrable f μ ↔ MeasureTheory.IntegrableAtFilter f Filter.atBot μ ∧ MeasureTheory.LocallyIntegrable f μ
• MeasureTheory.integrable_iff_integrableAtFilter_atTop 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} [TopologicalSpace.PseudoMetrizableSpace ε] [LinearOrder X] [OrderBot X] [CompactIccSpace X] : MeasureTheory.Integrable f μ ↔ MeasureTheory.IntegrableAtFilter f Filter.atTop μ ∧ MeasureTheory.LocallyIntegrable f μ
• MeasureTheory.locallyIntegrable_finsetSum' 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] {μ : MeasureTheory.Measure X} {ε''' : Type u_9} [TopologicalSpace ε'''] [ESeminormedAddCommMonoid ε'''] [ContinuousAdd ε'''] {ι : Type u_10} (s : Finset ι) {f : ι → X → ε'''} (hf : ∀ i ∈ s, MeasureTheory.LocallyIntegrable (f i) μ) : MeasureTheory.LocallyIntegrable (∑ i ∈ s, f i) μ
• MeasureTheory.locallyIntegrable_finset_sum' 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] {μ : MeasureTheory.Measure X} {ε''' : Type u_9} [TopologicalSpace ε'''] [ESeminormedAddCommMonoid ε'''] [ContinuousAdd ε'''] {ι : Type u_10} (s : Finset ι) {f : ι → X → ε'''} (hf : ∀ i ∈ s, MeasureTheory.LocallyIntegrable (f i) μ) : MeasureTheory.LocallyIntegrable (∑ i ∈ s, f i) μ
• MeasureTheory.integrable_iff_integrableAtFilter_atBot_atTop 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {ε'' : Type u_5} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε''] [ESeminormedAddMonoid ε''] {μ : MeasureTheory.Measure X} [TopologicalSpace.PseudoMetrizableSpace ε''] {f : X → ε''} [LinearOrder X] [CompactIccSpace X] : MeasureTheory.Integrable f μ ↔ (MeasureTheory.IntegrableAtFilter f Filter.atBot μ ∧ MeasureTheory.IntegrableAtFilter f Filter.atTop μ) ∧ MeasureTheory.LocallyIntegrable f μ
• MeasureTheory.LocallyIntegrable.sub 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} {f g : X → E} (hf : MeasureTheory.LocallyIntegrable f μ) (hg : MeasureTheory.LocallyIntegrable g μ) : MeasureTheory.LocallyIntegrable (f - g) μ
• MeasureTheory.locallyIntegrable_comap 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {ε : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [TopologicalSpace ε] [ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} {s : Set X} (hs : MeasurableSet s) : MeasureTheory.LocallyIntegrable (fun x => f ↑x) (MeasureTheory.Measure.comap Subtype.val μ) ↔ MeasureTheory.LocallyIntegrableOn f s μ
• MeasureTheory.LocallyIntegrable.mono 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {E : Type u_6} {F : Type u_7} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] [NormedAddCommGroup F] {μ : MeasureTheory.Measure X} {f : X → E} (hf : MeasureTheory.LocallyIntegrable f μ) {g : X → F} (hg : MeasureTheory.AEStronglyMeasurable g μ) (h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖) : MeasureTheory.LocallyIntegrable g μ
• MeasureTheory.locallyIntegrable_map_homeomorph 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {Y : Type u_2} {ε'' : Type u_5} [MeasurableSpace X] [TopologicalSpace X] [MeasurableSpace Y] [TopologicalSpace Y] [TopologicalSpace ε''] [ESeminormedAddMonoid ε''] [BorelSpace X] [BorelSpace Y] (e : X ≃ₜ Y) {f : Y → ε''} {μ : MeasureTheory.Measure X} : MeasureTheory.LocallyIntegrable f (MeasureTheory.Measure.map (⇑e) μ) ↔ MeasureTheory.LocallyIntegrable (f ∘ ⇑e) μ
• Antitone.locallyIntegrable 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} [BorelSpace X] [ConditionallyCompleteLinearOrder X] [ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E] {f : X → E} [MeasureTheory.IsLocallyFiniteMeasure μ] (hanti : Antitone f) : MeasureTheory.LocallyIntegrable f μ
• Monotone.locallyIntegrable 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} [BorelSpace X] [ConditionallyCompleteLinearOrder X] [ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E] {f : X → E} [MeasureTheory.IsLocallyFiniteMeasure μ] (hmono : Monotone f) : MeasureTheory.LocallyIntegrable f μ
• MeasureTheory.LocallyIntegrable.continuous_mul 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {R : Type u_8} [MeasurableSpace X] [TopologicalSpace X] {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] [LocallyCompactSpace X] [T2Space X] [NormedRing R] [SecondCountableTopologyEither X R] {f g : X → R} (hg : Continuous g) (hf : MeasureTheory.LocallyIntegrable f μ) : MeasureTheory.LocallyIntegrable (fun x => g x * f x) μ
• MeasureTheory.LocallyIntegrable.mul_continuous 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {R : Type u_8} [MeasurableSpace X] [TopologicalSpace X] {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] [LocallyCompactSpace X] [T2Space X] [NormedRing R] [SecondCountableTopologyEither X R] {f g : X → R} (hg : Continuous g) (hf : MeasureTheory.LocallyIntegrable f μ) : MeasureTheory.LocallyIntegrable (fun x => f x * g x) μ
• MeasureTheory.LocallyIntegrable.smul 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} {f : X → E} {𝕜 : Type u_9} [NormedAddCommGroup 𝕜] [SMulZeroClass 𝕜 E] [IsBoundedSMul 𝕜 E] (hf : MeasureTheory.LocallyIntegrable f μ) (c : 𝕜) : MeasureTheory.LocallyIntegrable (c • f) μ
• MeasureTheory.locallyIntegrable_smul_iff 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} {𝕜 : Type u_9} [NormedField 𝕜] [NormedSpace 𝕜 E] {f : X → E} (c : 𝕜) : MeasureTheory.LocallyIntegrable (c • f) μ ↔ c = 0 ∨ MeasureTheory.LocallyIntegrable f μ
• MeasureTheory.LocallyIntegrable.continuous_smul 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] [LocallyCompactSpace X] [T2Space X] {𝕜 : Type u_9} [NormedRing 𝕜] [Module 𝕜 E] [NormSMulClass 𝕜 E] [SecondCountableTopologyEither X 𝕜] {f : X → E} {g : X → 𝕜} (hg : Continuous g) (hf : MeasureTheory.LocallyIntegrable f μ) : MeasureTheory.LocallyIntegrable (fun x => g x • f x) μ
• MeasureTheory.LocallyIntegrable.smul_continuous 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] [LocallyCompactSpace X] [T2Space X] {𝕜 : Type u_9} [NormedRing 𝕜] [Module 𝕜 E] [NormSMulClass 𝕜 E] [SecondCountableTopologyEither X E] {f : X → 𝕜} {g : X → E} (hg : Continuous g) (hf : MeasureTheory.LocallyIntegrable f μ) : MeasureTheory.LocallyIntegrable (fun x => f x • g x) μ
• MeasureTheory.LocallyIntegrable.integrable_smul_left_of_hasCompactSupport 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} {𝕜 : Type u_9} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [OpensMeasurableSpace X] [T2Space X] {f : X → E} (hf : MeasureTheory.LocallyIntegrable f μ) {g : X → 𝕜} (hg : Continuous g) (h'g : HasCompactSupport g) : MeasureTheory.Integrable (fun x => g x • f x) μ
• MeasureTheory.LocallyIntegrable.integrable_smul_right_of_hasCompactSupport 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} {𝕜 : Type u_9} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [OpensMeasurableSpace X] [T2Space X] {f : X → 𝕜} (hf : MeasureTheory.LocallyIntegrable f μ) {g : X → E} (hg : Continuous g) (h'g : HasCompactSupport g) : MeasureTheory.Integrable (fun x => f x • g x) μ
• VitaliFamily.eventually_filterAt_integrableOn 📋 Mathlib.MeasureTheory.Covering.Differentiation
  {α : Type u_1} [PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) {E : Type u_2} [NormedAddCommGroup E] (x : α) {f : α → E} (hf : MeasureTheory.LocallyIntegrable f μ) : ∀ᶠ (a : Set α) in v.filterAt x, MeasureTheory.IntegrableOn f a μ
• VitaliFamily.ae_tendsto_average 📋 Mathlib.MeasureTheory.Covering.Differentiation
  {α : Type u_1} [PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) {E : Type u_2} [NormedAddCommGroup E] [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] [NormedSpace ℝ E] [CompleteSpace E] {f : α → E} (hf : MeasureTheory.LocallyIntegrable f μ) : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => ⨍ (y : α) in a, f y ∂μ) (v.filterAt x) (nhds (f x))
• VitaliFamily.ae_tendsto_average_norm_sub 📋 Mathlib.MeasureTheory.Covering.Differentiation
  {α : Type u_1} [PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) {E : Type u_2} [NormedAddCommGroup E] [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {f : α → E} (hf : MeasureTheory.LocallyIntegrable f μ) : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (nhds 0)
• VitaliFamily.ae_tendsto_lintegral_enorm_sub_div 📋 Mathlib.MeasureTheory.Covering.Differentiation
  {α : Type u_1} [PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) {E : Type u_2} [NormedAddCommGroup E] [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {f : α → E} (hf : MeasureTheory.LocallyIntegrable f μ) : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (nhds 0)
• IsUnifLocDoublingMeasure.ae_tendsto_average 📋 Mathlib.MeasureTheory.Covering.DensityTheorem
  {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : α → E} (hf : MeasureTheory.LocallyIntegrable f μ) (K : ℝ) : ∀ᵐ (x : α) ∂μ, ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ), Filter.Tendsto δ l (nhdsWithin 0 (Set.Ioi 0)) → (∀ᶠ (j : ι) in l, x ∈ Metric.closedBall (w j) (K * δ j)) → Filter.Tendsto (fun j => ⨍ (y : α) in Metric.closedBall (w j) (δ j), f y ∂μ) l (nhds (f x))
• IsUnifLocDoublingMeasure.ae_tendsto_average_norm_sub 📋 Mathlib.MeasureTheory.Covering.DensityTheorem
  {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) [IsUnifLocDoublingMeasure μ] [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {E : Type u_2} [NormedAddCommGroup E] {f : α → E} (hf : MeasureTheory.LocallyIntegrable f μ) (K : ℝ) : ∀ᵐ (x : α) ∂μ, ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ), Filter.Tendsto δ l (nhdsWithin 0 (Set.Ioi 0)) → (∀ᶠ (j : ι) in l, x ∈ Metric.closedBall (w j) (K * δ j)) → Filter.Tendsto (fun j => ⨍ (y : α) in Metric.closedBall (w j) (δ j), ‖f y - f x‖ ∂μ) l (nhds 0)
• HasCompactSupport.convolutionExists_left_of_continuous_right 📋 Mathlib.Analysis.Convolution
  {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} {g : G → E'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [BorelSpace G] (hcf : HasCompactSupport f) (hf : MeasureTheory.LocallyIntegrable f μ) (hg : Continuous g) : MeasureTheory.ConvolutionExists f g L μ
• HasCompactSupport.convolutionExists_right 📋 Mathlib.Analysis.Convolution
  {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} {g : G → E'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [BorelSpace G] (hcg : HasCompactSupport g) (hf : MeasureTheory.LocallyIntegrable f μ) (hg : Continuous g) : MeasureTheory.ConvolutionExists f g L μ
• HasCompactSupport.continuous_convolution_right 📋 Mathlib.Analysis.Convolution
  {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} {g : G → E'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [BorelSpace G] (hcg : HasCompactSupport g) (hf : MeasureTheory.LocallyIntegrable f μ) (hg : Continuous g) : Continuous (MeasureTheory.convolution f g L μ)
• HasCompactSupport.convolutionExists_left 📋 Mathlib.Analysis.Convolution
  {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} {g : G → E'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [BorelSpace G] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (hcf : HasCompactSupport f) (hf : Continuous f) (hg : MeasureTheory.LocallyIntegrable g μ) : MeasureTheory.ConvolutionExists f g L μ
• HasCompactSupport.convolutionExists_right_of_continuous_left 📋 Mathlib.Analysis.Convolution
  {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} {g : G → E'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [BorelSpace G] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (hcg : HasCompactSupport g) (hf : Continuous f) (hg : MeasureTheory.LocallyIntegrable g μ) : MeasureTheory.ConvolutionExists f g L μ
• HasCompactSupport.continuous_convolution_left 📋 Mathlib.Analysis.Convolution
  {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} {g : G → E'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [AddCommGroup G] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] [TopologicalSpace G] [IsTopologicalAddGroup G] [BorelSpace G] (hcf : HasCompactSupport f) (hf : Continuous f) (hg : MeasureTheory.LocallyIntegrable g μ) : Continuous (MeasureTheory.convolution f g L μ)
• MeasureTheory.continuousOn_convolution_right_with_param_comp 📋 Mathlib.Analysis.Convolution
  {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [BorelSpace G] [TopologicalSpace P] {s : Set P} {v : P → G} (hv : ContinuousOn v s) {g : P → G → E'} {k : Set G} (hk : IsCompact k) (hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) (hf : MeasureTheory.LocallyIntegrable f μ) (hg : ContinuousOn (↿g) (s ×ˢ Set.univ)) : ContinuousOn (fun x => MeasureTheory.convolution f (g x) L μ (v x)) s
• MeasureTheory.continuousOn_convolution_right_with_param 📋 Mathlib.Analysis.Convolution
  {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ F] [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [BorelSpace G] [TopologicalSpace P] {g : P → G → E'} {s : Set P} {k : Set G} (hk : IsCompact k) (hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) (hf : MeasureTheory.LocallyIntegrable f μ) (hg : ContinuousOn (↿g) (s ×ˢ Set.univ)) : ContinuousOn (fun q => MeasureTheory.convolution f (g q.1) L μ q.2) (s ×ˢ Set.univ)
• HasCompactSupport.convolutionExistsAt 📋 Mathlib.Analysis.Convolution
  {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} {g : G → E'} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) [MeasurableSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [BorelSpace G] {x₀ : G} (h : HasCompactSupport fun t => (L (f t)) (g (x₀ - t))) (hf : MeasureTheory.LocallyIntegrable f μ) (hg : Continuous g) : MeasureTheory.ConvolutionExistsAt f g x₀ L μ
• MeasureTheory.convolution_precompR_apply 📋 Mathlib.Analysis.Convolution
  {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {E'' : Type uE''} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup E''] [NormedAddCommGroup F] {f : G → E} [RCLike 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 E''] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [MeasurableSpace G] {μ : MeasureTheory.Measure G} (L : E →L[𝕜] E' →L[𝕜] F) [NormedAddCommGroup G] [BorelSpace G] {g : G → E'' →L[𝕜] E'} (hf : MeasureTheory.LocallyIntegrable f μ) (hcg : HasCompactSupport g) (hg : Continuous g) (x₀ : G) (x : E'') : (MeasureTheory.convolution f g (ContinuousLinearMap.precompR E'' L) μ x₀) x = MeasureTheory.convolution f (fun a => (g a) x) L μ x₀
• HasCompactSupport.contDiff_convolution_right 📋 Mathlib.Analysis.Calculus.ContDiff.Convolution
  {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} {g : G → E'} [RCLike 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [MeasurableSpace G] [NormedAddCommGroup G] [BorelSpace G] [NormedSpace 𝕜 G] {μ : MeasureTheory.Measure G} (L : E →L[𝕜] E' →L[𝕜] F) {n : ℕ∞} (hcg : HasCompactSupport g) (hf : MeasureTheory.LocallyIntegrable f μ) (hg : ContDiff 𝕜 (↑n) g) : ContDiff 𝕜 (↑n) (MeasureTheory.convolution f g L μ)
• HasCompactSupport.contDiff_convolution_left 📋 Mathlib.Analysis.Calculus.ContDiff.Convolution
  {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} {g : G → E'} [RCLike 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [MeasurableSpace G] [NormedAddCommGroup G] [BorelSpace G] [NormedSpace 𝕜 G] {μ : MeasureTheory.Measure G} (L : E →L[𝕜] E' →L[𝕜] F) [μ.IsAddLeftInvariant] [μ.IsNegInvariant] {n : ℕ∞} (hcf : HasCompactSupport f) (hf : ContDiff 𝕜 (↑n) f) (hg : MeasureTheory.LocallyIntegrable g μ) : ContDiff 𝕜 (↑n) (MeasureTheory.convolution f g L μ)
• MeasureTheory.contDiffOn_convolution_right_with_param_comp 📋 Mathlib.Analysis.Calculus.ContDiff.Convolution
  {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] [RCLike 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [MeasurableSpace G] [NormedAddCommGroup G] [BorelSpace G] [NormedSpace 𝕜 G] [NormedAddCommGroup P] [NormedSpace 𝕜 P] {μ : MeasureTheory.Measure G} {n : ℕ∞} (L : E →L[𝕜] E' →L[𝕜] F) {s : Set P} {v : P → G} (hv : ContDiffOn 𝕜 (↑n) v s) {f : G → E} {g : P → G → E'} {k : Set G} (hs : IsOpen s) (hk : IsCompact k) (hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) (hf : MeasureTheory.LocallyIntegrable f μ) (hg : ContDiffOn 𝕜 (↑n) (↿g) (s ×ˢ Set.univ)) : ContDiffOn 𝕜 (↑n) (fun x => MeasureTheory.convolution f (g x) L μ (v x)) s
• MeasureTheory.contDiffOn_convolution_right_with_param 📋 Mathlib.Analysis.Calculus.ContDiff.Convolution
  {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] [RCLike 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [MeasurableSpace G] [NormedAddCommGroup G] [BorelSpace G] [NormedSpace 𝕜 G] [NormedAddCommGroup P] [NormedSpace 𝕜 P] {μ : MeasureTheory.Measure G} {f : G → E} {n : ℕ∞} (L : E →L[𝕜] E' →L[𝕜] F) {g : P → G → E'} {s : Set P} {k : Set G} (hs : IsOpen s) (hk : IsCompact k) (hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) (hf : MeasureTheory.LocallyIntegrable f μ) (hg : ContDiffOn 𝕜 (↑n) (↿g) (s ×ˢ Set.univ)) : ContDiffOn 𝕜 (↑n) (fun q => MeasureTheory.convolution f (g q.1) L μ q.2) (s ×ˢ Set.univ)
• MeasureTheory.contDiffOn_convolution_right_with_param_aux 📋 Mathlib.Analysis.Calculus.ContDiff.Convolution
  {𝕜 : Type u𝕜} {E : Type uE} [NormedAddCommGroup E] [RCLike 𝕜] [NormedSpace 𝕜 E] {G E' F P : Type uP} [NormedAddCommGroup E'] [NormedAddCommGroup F] [NormedSpace 𝕜 E'] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedAddCommGroup G] [BorelSpace G] [NormedSpace 𝕜 G] [NormedAddCommGroup P] [NormedSpace 𝕜 P] {f : G → E} {n : ℕ∞} (L : E →L[𝕜] E' →L[𝕜] F) {g : P → G → E'} {s : Set P} {k : Set G} (hs : IsOpen s) (hk : IsCompact k) (hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) (hf : MeasureTheory.LocallyIntegrable f μ) (hg : ContDiffOn 𝕜 (↑n) (↿g) (s ×ˢ Set.univ)) : ContDiffOn 𝕜 (↑n) (fun q => MeasureTheory.convolution f (g q.1) L μ q.2) (s ×ˢ Set.univ)
• MeasureTheory.contDiffOn_convolution_left_with_param_comp 📋 Mathlib.Analysis.Calculus.ContDiff.Convolution
  {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] [RCLike 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [MeasurableSpace G] [NormedAddCommGroup G] [BorelSpace G] [NormedSpace 𝕜 G] [NormedAddCommGroup P] [NormedSpace 𝕜 P] {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (L : E' →L[𝕜] E →L[𝕜] F) {s : Set P} {n : ℕ∞} {v : P → G} (hv : ContDiffOn 𝕜 (↑n) v s) {f : G → E} {g : P → G → E'} {k : Set G} (hs : IsOpen s) (hk : IsCompact k) (hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) (hf : MeasureTheory.LocallyIntegrable f μ) (hg : ContDiffOn 𝕜 (↑n) (↿g) (s ×ˢ Set.univ)) : ContDiffOn 𝕜 (↑n) (fun x => MeasureTheory.convolution (g x) f L μ (v x)) s
• MeasureTheory.contDiffOn_convolution_left_with_param 📋 Mathlib.Analysis.Calculus.ContDiff.Convolution
  {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] [RCLike 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [MeasurableSpace G] [NormedAddCommGroup G] [BorelSpace G] [NormedSpace 𝕜 G] [NormedAddCommGroup P] [NormedSpace 𝕜 P] {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (L : E' →L[𝕜] E →L[𝕜] F) {f : G → E} {n : ℕ∞} {g : P → G → E'} {s : Set P} {k : Set G} (hs : IsOpen s) (hk : IsCompact k) (hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) (hf : MeasureTheory.LocallyIntegrable f μ) (hg : ContDiffOn 𝕜 (↑n) (↿g) (s ×ˢ Set.univ)) : ContDiffOn 𝕜 (↑n) (fun q => MeasureTheory.convolution (g q.1) f L μ q.2) (s ×ˢ Set.univ)
• HasCompactSupport.hasDerivAt_convolution_right 📋 Mathlib.Analysis.Calculus.ContDiff.Convolution
  {𝕜 : Type u𝕜} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] [RCLike 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace ℝ F] [NormedSpace 𝕜 F] {f₀ : 𝕜 → E} {g₀ : 𝕜 → E'} (L : E →L[𝕜] E' →L[𝕜] F) {μ : MeasureTheory.Measure 𝕜} [μ.IsAddLeftInvariant] [MeasureTheory.SFinite μ] (hf : MeasureTheory.LocallyIntegrable f₀ μ) (hcg : HasCompactSupport g₀) (hg : ContDiff 𝕜 1 g₀) (x₀ : 𝕜) : HasDerivAt (MeasureTheory.convolution f₀ g₀ L μ) (MeasureTheory.convolution f₀ (deriv g₀) L μ x₀) x₀
• HasCompactSupport.hasDerivAt_convolution_left 📋 Mathlib.Analysis.Calculus.ContDiff.Convolution
  {𝕜 : Type u𝕜} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] [RCLike 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace ℝ F] [NormedSpace 𝕜 F] {f₀ : 𝕜 → E} {g₀ : 𝕜 → E'} (L : E →L[𝕜] E' →L[𝕜] F) {μ : MeasureTheory.Measure 𝕜} [μ.IsAddLeftInvariant] [MeasureTheory.SFinite μ] [μ.IsNegInvariant] (hcf : HasCompactSupport f₀) (hf : ContDiff 𝕜 1 f₀) (hg : MeasureTheory.LocallyIntegrable g₀ μ) (x₀ : 𝕜) : HasDerivAt (MeasureTheory.convolution f₀ g₀ L μ) (MeasureTheory.convolution (deriv f₀) g₀ L μ x₀) x₀
• HasCompactSupport.hasFDerivAt_convolution_right 📋 Mathlib.Analysis.Calculus.ContDiff.Convolution
  {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} {g : G → E'} [RCLike 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [MeasurableSpace G] {μ : MeasureTheory.Measure G} (L : E →L[𝕜] E' →L[𝕜] F) [NormedAddCommGroup G] [BorelSpace G] [NormedSpace 𝕜 G] [MeasureTheory.SFinite μ] [μ.IsAddLeftInvariant] (hcg : HasCompactSupport g) (hf : MeasureTheory.LocallyIntegrable f μ) (hg : ContDiff 𝕜 1 g) (x₀ : G) : HasFDerivAt (MeasureTheory.convolution f g L μ) (MeasureTheory.convolution f (fderiv 𝕜 g) (ContinuousLinearMap.precompR G L) μ x₀) x₀
• HasCompactSupport.hasFDerivAt_convolution_left 📋 Mathlib.Analysis.Calculus.ContDiff.Convolution
  {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} {g : G → E'} [RCLike 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [MeasurableSpace G] {μ : MeasureTheory.Measure G} (L : E →L[𝕜] E' →L[𝕜] F) [NormedAddCommGroup G] [BorelSpace G] [NormedSpace 𝕜 G] [MeasureTheory.SFinite μ] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (hcf : HasCompactSupport f) (hf : ContDiff 𝕜 1 f) (hg : MeasureTheory.LocallyIntegrable g μ) (x₀ : G) : HasFDerivAt (MeasureTheory.convolution f g L μ) (MeasureTheory.convolution (fderiv 𝕜 f) g (ContinuousLinearMap.precompL G L) μ x₀) x₀
• MeasureTheory.hasFDerivAt_convolution_right_with_param 📋 Mathlib.Analysis.Calculus.ContDiff.Convolution
  {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] {f : G → E} [RCLike 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [MeasurableSpace G] [NormedAddCommGroup G] [BorelSpace G] [NormedSpace 𝕜 G] [NormedAddCommGroup P] [NormedSpace 𝕜 P] {μ : MeasureTheory.Measure G} (L : E →L[𝕜] E' →L[𝕜] F) {g : P → G → E'} {s : Set P} {k : Set G} (hs : IsOpen s) (hk : IsCompact k) (hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) (hf : MeasureTheory.LocallyIntegrable f μ) (hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ Set.univ)) (q₀ : P × G) (hq₀ : q₀.1 ∈ s) : HasFDerivAt (fun q => MeasureTheory.convolution f (g q.1) L μ q.2) (MeasureTheory.convolution f (fun x => fderiv 𝕜 ↿g (q₀.1, x)) (ContinuousLinearMap.precompR (P × G) L) μ q₀.2) q₀
• ContDiffBump.ae_convolution_tendsto_right_of_locallyIntegrable 📋 Mathlib.Analysis.Calculus.BumpFunction.Convolution
  {G : Type uG} {E' : Type uE'} [NormedAddCommGroup E'] {g : G → E'} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ E'] [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace E'] [BorelSpace G] [FiniteDimensional ℝ G] [μ.IsAddHaarMeasure] {ι : Type u_1} {φ : ι → ContDiffBump 0} {l : Filter ι} {K : ℝ} (hφ : Filter.Tendsto (fun i => (φ i).rOut) l (nhds 0)) (h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn) (hg : MeasureTheory.LocallyIntegrable g μ) : ∀ᵐ (x₀ : G) ∂μ, Filter.Tendsto (fun i => MeasureTheory.convolution ((φ i).normed μ) g (ContinuousLinearMap.lsmul ℝ ℝ) μ x₀) l (nhds (g x₀))
• MeasureTheory.LocallyIntegrable.exists_contDiff_dist_le_of_forall_mem_ball_dist_le 📋 Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox
  {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : E → F} {ε : ℝ} [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] (hf : MeasureTheory.LocallyIntegrable f μ) (hε : 0 < ε) : ∃ g, ContDiff ℝ (↑⊤) g ∧ ∀ (a : E) (δ : ℝ), (∀ x ∈ Metric.ball a ε, dist (f x) (f a) ≤ δ) → dist (g a) (f a) ≤ δ
• MeasureTheory.ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero' 📋 Mathlib.MeasureTheory.Function.AEEqOfIntegral
  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {β : Type u_3} [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] [SigmaCompactSpace β] [R1Space β] {μ : MeasureTheory.Measure β} {f : β → E} (hf : MeasureTheory.LocallyIntegrable f μ) (h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0) : f =ᵐ[μ] 0
• ae_eq_zero_of_integral_contDiff_smul_eq_zero 📋 Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [MeasurableSpace E] [BorelSpace E] {f : E → F} {μ : MeasureTheory.Measure E} (hf : MeasureTheory.LocallyIntegrable f μ) (h : ∀ (g : E → ℝ), ContDiff ℝ (↑⊤) g → HasCompactSupport g → ∫ (x : E), g x • f x ∂μ = 0) : ∀ᵐ (x : E) ∂μ, f x = 0
• ae_eq_zero_of_integral_contMDiff_smul_eq_zero 📋 Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [MeasurableSpace M] [BorelSpace M] [T2Space M] {f : M → F} {μ : MeasureTheory.Measure M} [SigmaCompactSpace M] (hf : MeasureTheory.LocallyIntegrable f μ) (h : ∀ (g : M → ℝ), ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0) : ∀ᵐ (x : M) ∂μ, f x = 0
• ae_eq_of_integral_contDiff_smul_eq 📋 Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [MeasurableSpace E] [BorelSpace E] {f f' : E → F} {μ : MeasureTheory.Measure E} (hf : MeasureTheory.LocallyIntegrable f μ) (hf' : MeasureTheory.LocallyIntegrable f' μ) (h : ∀ (g : E → ℝ), ContDiff ℝ (↑⊤) g → HasCompactSupport g → ∫ (x : E), g x • f x ∂μ = ∫ (x : E), g x • f' x ∂μ) : ∀ᵐ (x : E) ∂μ, f x = f' x
• ae_eq_of_integral_contMDiff_smul_eq 📋 Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [MeasurableSpace M] [BorelSpace M] [T2Space M] {f f' : M → F} {μ : MeasureTheory.Measure M} [SigmaCompactSpace M] (hf : MeasureTheory.LocallyIntegrable f μ) (hf' : MeasureTheory.LocallyIntegrable f' μ) (h : ∀ (g : M → ℝ), ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = ∫ (x : M), g x • f' x ∂μ) : ∀ᵐ (x : M) ∂μ, f x = f' x
• LipschitzWith.locallyIntegrable_lineDeriv 📋 Mathlib.Analysis.Calculus.Rademacher
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {C : NNReal} {f : E → ℝ} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] (hf : LipschitzWith C f) (v : E) : MeasureTheory.LocallyIntegrable (fun x => lineDeriv ℝ f x v) μ
• LocallyIntegrable.ae_hasDerivAt_integral 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} (hf : MeasureTheory.LocallyIntegrable f MeasureTheory.volume) : ∀ᵐ (x : ℝ), ∀ (c : ℝ), HasDerivAt (fun x => ∫ (t : ℝ) in c..x, f t) (f x) x
• MeasureTheory.LocallyIntegrable.integrable_of_isBigO_cocompact 📋 Mathlib.MeasureTheory.Integral.Asymptotics
  {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] {f : α → E} {g : α → F} [TopologicalSpace α] [SecondCountableTopology α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [(Filter.cocompact α).IsMeasurablyGenerated] (hf : MeasureTheory.LocallyIntegrable f μ) (ho : f =O[Filter.cocompact α] g) (hg : MeasureTheory.IntegrableAtFilter g (Filter.cocompact α) μ) : MeasureTheory.Integrable f μ
• MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atBot 📋 Mathlib.MeasureTheory.Integral.Asymptotics
  {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] {f : α → E} {g : α → F} [TopologicalSpace α] [SecondCountableTopology α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [LinearOrder α] [CompactIccSpace α] [Filter.atBot.IsMeasurablyGenerated] [OrderTop α] (hf : MeasureTheory.LocallyIntegrable f μ) (ho : f =O[Filter.atBot] g) (hg : MeasureTheory.IntegrableAtFilter g Filter.atBot μ) : MeasureTheory.Integrable f μ
• MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atTop 📋 Mathlib.MeasureTheory.Integral.Asymptotics
  {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] {f : α → E} {g : α → F} [TopologicalSpace α] [SecondCountableTopology α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [LinearOrder α] [CompactIccSpace α] [Filter.atTop.IsMeasurablyGenerated] [OrderBot α] (hf : MeasureTheory.LocallyIntegrable f μ) (ho : f =O[Filter.atTop] g) (hg : MeasureTheory.IntegrableAtFilter g Filter.atTop μ) : MeasureTheory.Integrable f μ
• MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atBot_atTop 📋 Mathlib.MeasureTheory.Integral.Asymptotics
  {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] {f : α → E} {g : α → F} [TopologicalSpace α] [SecondCountableTopology α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [LinearOrder α] [CompactIccSpace α] {g' : α → F} [Filter.atBot.IsMeasurablyGenerated] [Filter.atTop.IsMeasurablyGenerated] (hf : MeasureTheory.LocallyIntegrable f μ) (ho : f =O[Filter.atBot] g) (hg : MeasureTheory.IntegrableAtFilter g Filter.atBot μ) (ho' : f =O[Filter.atTop] g') (hg' : MeasureTheory.IntegrableAtFilter g' Filter.atTop μ) : MeasureTheory.Integrable f μ
• MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atTop_of_norm_isNegInvariant 📋 Mathlib.MeasureTheory.Integral.Asymptotics
  {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] {f : α → E} {g : α → F} [TopologicalSpace α] [SecondCountableTopology α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [CompactIccSpace α] [Filter.atTop.IsMeasurablyGenerated] [MeasurableNeg α] [μ.IsNegInvariant] (hf : MeasureTheory.LocallyIntegrable f μ) (hsymm : norm ∘ f =ᵐ[μ] norm ∘ f ∘ Neg.neg) (ho : f =O[Filter.atTop] g) (hg : MeasureTheory.IntegrableAtFilter g Filter.atTop μ) : MeasureTheory.Integrable f μ
• MeasureTheory.locallyIntegrable_of_norm_le_rpow 📋 Mathlib.Analysis.SpecialFunctions.Pow.Integral
  {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] (hdim : 1 ≤ Module.finrank ℝ E) {f : E → F} {C α : ℝ} (hα : α < ↑(Module.finrank ℝ E)) (h_decay : ∀ᵐ (x : E) ∂μ, ‖f x‖ ≤ C * ‖x‖ ^ (-α)) (h_meas : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.LocallyIntegrable 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 69fae59