Loogle!

Result

Found 165 declarations mentioning HasCompactSupport.

• HasCompactSupport 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] (f : α → β) : Prop
• HasCompactSupport.of_compactSpace 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {γ : Type u_5} [TopologicalSpace α] [Zero γ] [CompactSpace α] (f : α → γ) : HasCompactSupport f
• HasCompactSupport.isCompact 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} (hf : HasCompactSupport f) : IsCompact (tsupport f)
• HasCompactSupport.zero 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_9} {β : Type u_10} [TopologicalSpace α] [Zero β] : HasCompactSupport 0
• hasCompactSupport_def 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} : HasCompactSupport f ↔ IsCompact (closure (Function.support f))
• HasCompactSupport.isCompact_range 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} [TopologicalSpace β] (h : HasCompactSupport f) (hf : Continuous f) : IsCompact (Set.range f)
• HasCompactSupport.is_zero_at_infty 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {γ : Type u_5} [TopologicalSpace α] [Zero γ] {f : α → γ} [TopologicalSpace γ] (h : HasCompactSupport f) : Filter.Tendsto f (Filter.cocompact α) (nhds 0)
• HasCompactSupport.of_support_subset_isCompact 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} {K : Set α} [R1Space α] (hK : IsCompact K) (h : Function.support f ⊆ K) : HasCompactSupport f
• hasCompactSupport_iff_eventuallyEq 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} : HasCompactSupport f ↔ f =ᶠ[Filter.coclosedCompact α] 0
• HasCompactSupport.comp_isClosedEmbedding 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {α' : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace α'] [Zero β] {f : α → β} (hf : HasCompactSupport f) {g : α' → α} (hg : Topology.IsClosedEmbedding g) : HasCompactSupport (f ∘ g)
• HasCompactSupport.mono 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {β : Type u_4} {γ : Type u_5} [TopologicalSpace α] [Zero β] [Zero γ] {f : α → β} {f' : α → γ} (hf : HasCompactSupport f) (hff' : Function.support f' ⊆ Function.support f) : HasCompactSupport f'
• HasCompactSupport.mono' 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {β : Type u_4} {γ : Type u_5} [TopologicalSpace α] [Zero β] [Zero γ] {f : α → β} {f' : α → γ} (hf : HasCompactSupport f) (hff' : Function.support f' ⊆ tsupport f) : HasCompactSupport f'
• HasCompactSupport.intro 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} {K : Set α} [R1Space α] (hK : IsCompact K) (hfK : ∀ x ∉ K, f x = 0) : HasCompactSupport f
• HasCompactSupport.intro' 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} {K : Set α} (hK : IsCompact K) (h'K : IsClosed K) (hfK : ∀ x ∉ K, f x = 0) : HasCompactSupport f
• HasCompactSupport.comp_left 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {β : Type u_4} {γ : Type u_5} [TopologicalSpace α] [Zero β] [Zero γ] {g : β → γ} {f : α → β} (hf : HasCompactSupport f) (hg : g 0 = 0) : HasCompactSupport (g ∘ f)
• HasCompactSupport.mul_left 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [MulZeroClass β] {f f' : α → β} (hf : HasCompactSupport f') : HasCompactSupport (f * f')
• HasCompactSupport.mul_right 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [MulZeroClass β] {f f' : α → β} (hf : HasCompactSupport f) : HasCompactSupport (f * f')
• HasCompactSupport.neg 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_9} {β : Type u_10} [TopologicalSpace α] [SubtractionMonoid β] {f : α → β} (hf : HasCompactSupport f) : HasCompactSupport (-f)
• exists_compact_iff_hasCompactSupport 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} [R1Space α] : (∃ K, IsCompact K ∧ ∀ x ∉ K, f x = 0) ↔ HasCompactSupport f
• HasCompactSupport.isCompact_preimage 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [Zero β] {f : α → β} [TopologicalSpace β] {K : Set β} (h'f : HasCompactSupport f) (hf : Continuous f) (hk : IsClosed K) (h'k : 0 ∉ K) : IsCompact (f ⁻¹' K)
• hasCompactSupport_comp_left 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {β : Type u_4} {γ : Type u_5} [TopologicalSpace α] [Zero β] [Zero γ] {g : β → γ} {f : α → β} (hg : ∀ {x : β}, g x = 0 ↔ x = 0) : HasCompactSupport (g ∘ f) ↔ HasCompactSupport f
• HasCompactSupport.extend_zero 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {α' : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace α'] [Zero β] {f : α → β} [T2Space α'] (hf : HasCompactSupport f) {g : α → α'} (cont : Continuous g) : HasCompactSupport (Function.extend g f 0)
• HasCompactSupport.smul_left 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {M : Type u_7} {R : Type u_8} [TopologicalSpace α] [Zero M] [SMulZeroClass R M] {f : α → R} {f' : α → M} (hf : HasCompactSupport f') : HasCompactSupport (f • f')
• HasCompactSupport.comp_homeomorph 📋 Mathlib.Topology.Algebra.Support
  {X : Type u_9} {Y : Type u_10} [TopologicalSpace X] [TopologicalSpace Y] {M : Type u_11} [Zero M] {f : Y → M} (hf : HasCompactSupport f) (φ : X ≃ₜ Y) : HasCompactSupport (f ∘ ⇑φ)
• HasCompactSupport.mem_addSubmonoid_iff 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [AddZeroClass β] {f : α → β} : f ∈ HasCompactSupport.addSubmonoid α β ↔ HasCompactSupport f
• HasCompactSupport.multiset_sum 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [AddCommMonoid β] (m : Multiset (α → β)) (hm : ∀ f ∈ m, HasCompactSupport f) : HasCompactSupport m.sum
• HasCompactSupport.smul_right 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {M : Type u_7} {R : Type u_8} [TopologicalSpace α] [Zero R] [Zero M] [SMulWithZero R M] {f : α → R} {f' : α → M} (hf : HasCompactSupport f) : HasCompactSupport (f • f')
• HasCompactSupport.add 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [AddZeroClass β] {f f' : α → β} (hf : HasCompactSupport f) (hf' : HasCompactSupport f') : HasCompactSupport (f + f')
• HasCompactSupport.comp₂_left 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [TopologicalSpace α] [Zero β] [Zero γ] [Zero δ] {f : α → β} {f₂ : α → γ} {m : β → γ → δ} (hf : HasCompactSupport f) (hf₂ : HasCompactSupport f₂) (hm : m 0 0 = 0) : HasCompactSupport fun x => m (f x) (f₂ x)
• HasCompactSupport.finset_sum 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [AddCommMonoid β] {ι : Type u_9} {s : Finset ι} {f : ι → α → β} (hf : ∀ i ∈ s, HasCompactSupport (f i)) : HasCompactSupport (∑ i ∈ s, f i)
• HasCompactSupport.sub 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_9} {β : Type u_10} [TopologicalSpace α] [SubtractionMonoid β] {f f' : α → β} (hf : HasCompactSupport f) (hf' : HasCompactSupport f') : HasCompactSupport (f - f')
• HasCompactSupport.tsupport_extend_zero_subset 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {α' : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace α'] [Zero β] {f : α → β} [T2Space α'] (hf : HasCompactSupport f) {g : α → α'} (cont : Continuous g) : tsupport (Function.extend g f 0) ⊆ g '' tsupport f
• HasCompactSupport.tsupport_extend_zero 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {α' : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace α'] [Zero β] {f : α → β} [T2Space α'] (hf : HasCompactSupport f) {g : α → α'} (cont : Continuous g) (inj : Function.Injective g) : tsupport (Function.extend g f 0) = g '' tsupport f
• HasCompactSupport.abs 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_2} {β : Type u_4} [TopologicalSpace α] [AddGroup β] [Lattice β] [AddLeftMono β] {f : α → β} (hf : HasCompactSupport f) : HasCompactSupport |f|
• HasCompactSupport.list_sum 📋 Mathlib.Topology.Algebra.Support
  {α : Type u_9} {β : Type u_10} [TopologicalSpace α] [AddMonoid β] {l : List (α → β)} (hl : ∀ f ∈ l, HasCompactSupport f) : HasCompactSupport l.sum
• HasCompactSupport.continuous_extend_zero 📋 Mathlib.Topology.Algebra.Support
  {α' : Type u_3} {β : Type u_4} [TopologicalSpace α'] [Zero β] [T2Space α'] [TopologicalSpace β] {U : Set α'} (hU : IsOpen U) {f : ↑U → β} (cont : Continuous f) (supp : HasCompactSupport f) : Continuous (Function.extend Subtype.val f 0)
• HasCompactSupport.comp_smul 📋 Mathlib.Topology.Algebra.ConstMulAction
  {α : Type u_2} {G₀ : Type u_4} [TopologicalSpace α] [GroupWithZero G₀] [MulAction G₀ α] [ContinuousConstSMul G₀ α] {β : Type u_5} [Zero β] {f : α → β} (h : HasCompactSupport f) {c : G₀} (hc : c ≠ 0) : HasCompactSupport fun x => f (c • x)
• HasCompactSupport.uniformContinuous_of_continuous 📋 Mathlib.Topology.UniformSpace.HeineCantor
  {α : Type u_1} {β : Type u_2} [UniformSpace α] [UniformSpace β] {f : α → β} [Zero β] (h1 : HasCompactSupport f) (h2 : Continuous f) : UniformContinuous f
• HasCompactSupport.eq_zero_or_locallyCompactSpace_of_addGroup 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} {α : Type u} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [TopologicalSpace α] [Zero α] [T1Space α] {f : G → α} (hf : HasCompactSupport f) (h'f : Continuous f) : f = 0 ∨ LocallyCompactSpace G
• HasCompactSupport.eq_zero_or_locallyCompactSpace_of_group 📋 Mathlib.Topology.Algebra.Group.Pointwise
  {G : Type w} {α : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [TopologicalSpace α] [Zero α] [T1Space α] {f : G → α} (hf : HasCompactSupport f) (h'f : Continuous f) : f = 0 ∨ LocallyCompactSpace G
• HasCompactSupport.norm 📋 Mathlib.Analysis.Normed.Group.Basic
  {α : Type u_2} {E : Type u_4} [NormedAddGroup E] [TopologicalSpace α] {f : α → E} : HasCompactSupport f → HasCompactSupport fun x => ‖f x‖
• hasCompactSupport_norm_iff 📋 Mathlib.Analysis.Normed.Group.Basic
  {α : Type u_2} {E : Type u_4} [NormedAddGroup E] [TopologicalSpace α] {f : α → E} : (HasCompactSupport fun x => ‖f x‖) ↔ HasCompactSupport f
• Continuous.bddAbove_range_of_hasCompactSupport 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIciTopology α] [Zero α] {f : β → α} (hf : Continuous f) (h : HasCompactSupport f) : BddAbove (Set.range f)
• Continuous.bddBelow_range_of_hasCompactSupport 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] [Zero α] {f : β → α} (hf : Continuous f) (h : HasCompactSupport f) : BddBelow (Set.range f)
• Continuous.exists_forall_ge_of_hasCompactSupport 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIciTopology α] [Nonempty β] [Zero α] {f : β → α} (hf : Continuous f) (h : HasCompactSupport f) : ∃ x, ∀ (y : β), f y ≤ f x
• Continuous.exists_forall_le_of_hasCompactSupport 📋 Mathlib.Topology.Order.Compact
  {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] [Nonempty β] [Zero α] {f : β → α} (hf : Continuous f) (h : HasCompactSupport f) : ∃ x, ∀ (y : β), f x ≤ f y
• HasCompactSupport.exists_bound_of_continuous 📋 Mathlib.Analysis.Normed.Group.Bounded
  {α : Type u_1} {E : Type u_2} [SeminormedAddGroup E] [TopologicalSpace α] {f : α → E} (hf : HasCompactSupport f) (h'f : Continuous f) : ∃ C, ∀ (x : α), ‖f x‖ ≤ C
• Continuous.bounded_above_of_compact_support 📋 Mathlib.Analysis.Normed.Group.Bounded
  {α : Type u_1} {E : Type u_2} [NormedAddGroup E] [TopologicalSpace α] {f : α → E} (hf : Continuous f) (h : HasCompactSupport f) : ∃ C, ∀ (x : α), ‖f x‖ ≤ C
• HasCompactSupport.exists_pos_le_norm 📋 Mathlib.Analysis.Normed.Group.Bounded
  {α : Type u_1} {E : Type u_2} [NormedAddGroup α] {f : α → E} [Zero E] (hf : HasCompactSupport f) : ∃ R, 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 0
• HasCompactSupport.measurable_of_prod 📋 Mathlib.MeasureTheory.Function.SimpleFuncDense
  {X : Type u_3} {Y : Type u_4} {α : Type u_5} [Zero α] [TopologicalSpace X] [TopologicalSpace Y] [MeasurableSpace X] [MeasurableSpace Y] [OpensMeasurableSpace X] [OpensMeasurableSpace Y] [TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α] [MeasurableSpace α] [BorelSpace α] {f : X × Y → α} (hf : Continuous f) (h'f : HasCompactSupport f) : Measurable f
• HasCompactSupport.exists_simpleFunc_approx_of_prod 📋 Mathlib.MeasureTheory.Function.SimpleFuncDense
  {X : Type u_3} {Y : Type u_4} {α : Type u_5} [Zero α] [TopologicalSpace X] [TopologicalSpace Y] [MeasurableSpace X] [MeasurableSpace Y] [OpensMeasurableSpace X] [OpensMeasurableSpace Y] [PseudoMetricSpace α] {f : X × Y → α} (hf : Continuous f) (h'f : HasCompactSupport f) {ε : ℝ} (hε : 0 < ε) : ∃ g, ∀ (x : X × Y), dist (f x) (g x) < ε
• Continuous.stronglyMeasurable_of_hasCompactSupport 📋 Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [TopologicalSpace α] [OpensMeasurableSpace α] [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [Zero β] {f : α → β} (hf : Continuous f) (h'f : HasCompactSupport f) : MeasureTheory.StronglyMeasurable f
• HasCompactSupport.stronglyMeasurable_of_prod 📋 Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
  {α : Type u_1} {X : Type u_5} {Y : Type u_6} [Zero α] [TopologicalSpace X] [TopologicalSpace Y] [MeasurableSpace X] [MeasurableSpace Y] [OpensMeasurableSpace X] [OpensMeasurableSpace Y] [TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α] {f : X × Y → α} (hf : Continuous f) (h'f : HasCompactSupport f) : MeasureTheory.StronglyMeasurable f
• HasCompactSupport.rpow_const 📋 Mathlib.Analysis.SpecialFunctions.Pow.Real
  {α : Type u_1} [TopologicalSpace α] {f : α → ℝ} (hf : HasCompactSupport f) {r : ℝ} (hr : r ≠ 0) : HasCompactSupport fun x => f x ^ r
• Continuous.memLp_top_of_hasCompactSupport 📋 Mathlib.MeasureTheory.Function.LpSeminorm.Basic
  {E : Type u_4} [NormedAddCommGroup E] {X : Type u_7} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {f : X → E} (hf : Continuous f) (h'f : HasCompactSupport f) (μ : MeasureTheory.Measure X) : MeasureTheory.MemLp f ⊤ μ
• HasCompactSupport.eq_zero_or_finiteDimensional 📋 Mathlib.Topology.Algebra.Module.FiniteDimension
  (𝕜 : Type u_4) [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_5} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [T2Space E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] {X : Type u_7} [TopologicalSpace X] [Zero X] [T1Space X] {f : E → X} (hf : HasCompactSupport f) (h'f : Continuous f) : f = 0 ∨ FiniteDimensional 𝕜 E
• Continuous.memLp_of_hasCompactSupport 📋 Mathlib.MeasureTheory.Function.LpSpace.Indicator
  {E : Type u_2} {p : ENNReal} [NormedAddCommGroup E] {X : Type u_3} [TopologicalSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasureOnCompacts μ] [OpensMeasurableSpace X] {f : X → E} (hf : Continuous f) (h'f : HasCompactSupport f) : MeasureTheory.MemLp f p μ
• HasCompactSupport.memLp_of_bound 📋 Mathlib.MeasureTheory.Function.LpSpace.Indicator
  {E : Type u_2} {p : ENNReal} [NormedAddCommGroup E] {X : Type u_3} [TopologicalSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {f : X → E} (hf : HasCompactSupport f) (h2f : MeasureTheory.AEStronglyMeasurable f μ) (C : ℝ) (hfC : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C) : MeasureTheory.MemLp f p μ
• HasCompactSupport.memLp_of_enorm_bound 📋 Mathlib.MeasureTheory.Function.LpSpace.Indicator
  {E : Type u_2} {p : ENNReal} [NormedAddCommGroup E] {X : Type u_3} [TopologicalSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {f : X → E} (hf : HasCompactSupport f) (h2f : MeasureTheory.AEStronglyMeasurable f μ) {C : ENNReal} (hfC : ∀ᵐ (x : X) ∂μ, ‖f x‖ₑ ≤ C) (hC : C ≠ ⊤) : MeasureTheory.MemLp f p μ
• Continuous.integrable_of_hasCompactSupport 📋 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.IsFiniteMeasureOnCompacts μ] (hf : Continuous f) (hcf : HasCompactSupport f) : MeasureTheory.Integrable f μ
• 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) μ
• Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero 📋 Mathlib.MeasureTheory.Integral.Bochner.Set
  {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ] {f : X → ℝ} {x : X} (f_cont : Continuous f) (f_comp : HasCompactSupport f) (f_nonneg : 0 ≤ f) (f_x : f x ≠ 0) : 0 < ∫ (x : X), f x ∂μ
• HasCompactSupport.fderiv 📋 Mathlib.Analysis.Calculus.FDeriv.Const
  (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] {f : E → F} (hf : HasCompactSupport f) : HasCompactSupport (fderiv 𝕜 f)
• HasCompactSupport.fderiv_apply 📋 Mathlib.Analysis.Calculus.FDeriv.Const
  (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] {f : E → F} (hf : HasCompactSupport f) (v : E) : HasCompactSupport fun x => (fderiv 𝕜 f x) v
• HasCompactSupport.deriv 📋 Mathlib.Analysis.Calculus.Deriv.Support
  {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} (hf : HasCompactSupport f) : HasCompactSupport (deriv f)
• HasCompactSupport.iteratedFDeriv 📋 Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
  {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} (hf : HasCompactSupport f) (n : ℕ) : HasCompactSupport (iteratedFDeriv 𝕜 n f)
• ContDiff.lipschitzWith_of_hasCompactSupport 📋 Mathlib.Analysis.Calculus.ContDiff.RCLike
  {n : WithTop ℕ∞} {𝕂 : Type u_1} [RCLike 𝕂] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕂 E'] {F' : Type u_3} [NormedAddCommGroup F'] [NormedSpace 𝕂 F'] {f : E' → F'} (hf : HasCompactSupport f) (h'f : ContDiff 𝕂 n f) (hn : n ≠ 0) : ∃ C, LipschitzWith C f
• MeasureTheory.integral_integral_swap_of_hasCompactSupport 📋 Mathlib.MeasureTheory.Integral.Prod
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : Type u_5} {Y : Type u_6} [TopologicalSpace X] [TopologicalSpace Y] [MeasurableSpace X] [MeasurableSpace Y] [OpensMeasurableSpace X] [OpensMeasurableSpace Y] {f : X → Y → E} (hf : Continuous (Function.uncurry f)) (h'f : HasCompactSupport (Function.uncurry f)) {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.IsFiniteMeasureOnCompacts μ] [MeasureTheory.IsFiniteMeasureOnCompacts ν] : ∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ = ∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν
• exists_continuous_nonneg_pos 📋 Mathlib.Topology.UrysohnsLemma
  {X : Type u_1} [TopologicalSpace X] [RegularSpace X] [LocallyCompactSpace X] (x : X) : ∃ f, HasCompactSupport ⇑f ∧ 0 ≤ ⇑f ∧ f x ≠ 0
• exists_continuous_one_zero_of_isCompact 📋 Mathlib.Topology.UrysohnsLemma
  {X : Type u_1} [TopologicalSpace X] [RegularSpace X] [LocallyCompactSpace X] {s t : Set X} (hs : IsCompact s) (ht : IsClosed t) (hd : Disjoint s t) : ∃ f, Set.EqOn (⇑f) 1 s ∧ Set.EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Set.Icc 0 1
• exists_continuous_one_zero_of_isCompact_of_isGδ 📋 Mathlib.Topology.UrysohnsLemma
  {X : Type u_1} [TopologicalSpace X] [RegularSpace X] [LocallyCompactSpace X] {s t : Set X} (hs : IsCompact s) (h's : IsGδ s) (ht : IsClosed t) (hd : Disjoint s t) : ∃ f, s = ⇑f ⁻¹' {1} ∧ Set.EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Set.Icc 0 1
• ContDiffBump.hasCompactSupport 📋 Mathlib.Analysis.Calculus.BumpFunction.Basic
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [HasContDiffBump E] {c : E} (f : ContDiffBump c) [FiniteDimensional ℝ E] : HasCompactSupport ↑f
• 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.convolution 📋 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] [T2Space G] (hcf : HasCompactSupport f) (hcg : HasCompactSupport g) : HasCompactSupport (MeasureTheory.convolution 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 μ)
• 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.convolution_integrand_bound_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) [AddGroup G] [TopologicalSpace G] (hcf : HasCompactSupport f) (hf : Continuous f) {x t : G} {s : Set G} (hx : x ∈ s) : ‖(L (f (x - t))) (g t)‖ ≤ (-tsupport f + s).indicator (fun t => (‖L‖ * ⨆ i, ‖f i‖) * ‖g t‖) t
• HasCompactSupport.convolution_integrand_bound_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) [AddGroup G] [TopologicalSpace G] (hcg : HasCompactSupport g) (hg : Continuous g) {x t : G} {s : Set G} (hx : x ∈ s) : ‖(L (f t)) (g (x - t))‖ ≤ (-tsupport g + s).indicator (fun t => ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖) t
• HasCompactSupport.convolution_integrand_bound_right_of_subset 📋 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) [AddGroup G] [TopologicalSpace G] (hcg : HasCompactSupport g) (hg : Continuous g) {x t : G} {s u : Set G} (hx : x ∈ s) (hu : -tsupport g + s ⊆ u) : ‖(L (f t)) (g (x - t))‖ ≤ u.indicator (fun t => ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖) t
• 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 μ)
• 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.Measure.innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_addGroup 📋 Mathlib.MeasureTheory.Measure.EverywherePos
  {G : Type u_2} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.InnerRegularCompactLTTop] : μ.InnerRegularWRT (fun s => ∃ f, Continuous f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) fun s => MeasurableSet s ∧ μ s ≠ ⊤
• MeasureTheory.Measure.innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_group 📋 Mathlib.MeasureTheory.Measure.EverywherePos
  {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.InnerRegularCompactLTTop] : μ.InnerRegularWRT (fun s => ∃ f, Continuous f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) fun s => MeasurableSet s ∧ μ s ≠ ⊤
• MeasureTheory.continuous_integral_apply_inv_mul 📋 Mathlib.MeasureTheory.Measure.Haar.Unique
  {G : Type u_1} [TopologicalSpace G] [LocallyCompactSpace G] [Group G] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : G → E} (hg : Continuous g) (h'g : HasCompactSupport g) : Continuous fun x => ∫ (y : G), g (y⁻¹ * x) ∂μ
• MeasureTheory.continuous_integral_apply_neg_add 📋 Mathlib.MeasureTheory.Measure.Haar.Unique
  {G : Type u_1} [TopologicalSpace G] [LocallyCompactSpace G] [AddGroup G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : G → E} (hg : Continuous g) (h'g : HasCompactSupport g) : Continuous fun x => ∫ (y : G), g (-y + x) ∂μ
• MeasureTheory.Measure.exists_integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport 📋 Mathlib.MeasureTheory.Measure.Haar.Unique
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] (μ' μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsAddLeftInvariant] : ∃ c, ∀ (f : G → ℝ), Continuous f → HasCompactSupport f → ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂c • μ
• MeasureTheory.Measure.exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport 📋 Mathlib.MeasureTheory.Measure.Haar.Unique
  {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (μ' μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsMulLeftInvariant] : ∃ c, ∀ (f : G → ℝ), Continuous f → HasCompactSupport f → ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂c • μ
• MeasureTheory.Measure.measure_preimage_isAddLeftInvariant_eq_smul_of_hasCompactSupport 📋 Mathlib.MeasureTheory.Measure.Haar.Unique
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] (μ' μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsAddLeftInvariant] {f : G → ℝ} (hf : Continuous f) (h'f : HasCompactSupport f) : μ' (f ⁻¹' {1}) = μ'.addHaarScalarFactor μ • μ (f ⁻¹' {1})
• MeasureTheory.Measure.measure_preimage_isMulLeftInvariant_eq_smul_of_hasCompactSupport 📋 Mathlib.MeasureTheory.Measure.Haar.Unique
  {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (μ' μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsMulLeftInvariant] {f : G → ℝ} (hf : Continuous f) (h'f : HasCompactSupport f) : μ' (f ⁻¹' {1}) = μ'.haarScalarFactor μ • μ (f ⁻¹' {1})
• MeasureTheory.Measure.addHaarScalarFactor_eq_integral_div 📋 Mathlib.MeasureTheory.Measure.Haar.Unique
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] (μ' μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsAddLeftInvariant] {f : G → ℝ} (hf : Continuous f) (h'f : HasCompactSupport f) (int_nonzero : ∫ (x : G), f x ∂μ ≠ 0) : ↑(μ'.addHaarScalarFactor μ) = (∫ (x : G), f x ∂μ') / ∫ (x : G), f x ∂μ
• MeasureTheory.Measure.haarScalarFactor_eq_integral_div 📋 Mathlib.MeasureTheory.Measure.Haar.Unique
  {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (μ' μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsMulLeftInvariant] {f : G → ℝ} (hf : Continuous f) (h'f : HasCompactSupport f) (int_nonzero : ∫ (x : G), f x ∂μ ≠ 0) : ↑(μ'.haarScalarFactor μ) = (∫ (x : G), f x ∂μ') / ∫ (x : G), f x ∂μ
• MeasureTheory.Measure.integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport 📋 Mathlib.MeasureTheory.Measure.Haar.Unique
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] (μ' μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsAddLeftInvariant] {f : G → ℝ} (hf : Continuous f) (h'f : HasCompactSupport f) : ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂μ'.addHaarScalarFactor μ • μ
• MeasureTheory.Measure.integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport 📋 Mathlib.MeasureTheory.Measure.Haar.Unique
  {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (μ' μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsMulLeftInvariant] {f : G → ℝ} (hf : Continuous f) (h'f : HasCompactSupport f) : ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂μ'.haarScalarFactor μ • μ
• MeasureTheory.Measure.integral_isAddLeftInvariant_isAddRightInvariant_combo 📋 Mathlib.MeasureTheory.Measure.Haar.Unique
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] {μ ν : MeasureTheory.Measure G} [MeasureTheory.IsFiniteMeasureOnCompacts μ] [MeasureTheory.IsFiniteMeasureOnCompacts ν] [μ.IsAddLeftInvariant] [ν.IsAddRightInvariant] [ν.IsOpenPosMeasure] {f g : G → ℝ} (hf : Continuous f) (h'f : HasCompactSupport f) (hg : Continuous g) (h'g : HasCompactSupport g) (g_nonneg : 0 ≤ g) {x₀ : G} (g_pos : g x₀ ≠ 0) : ∫ (x : G), f x ∂μ = (∫ (y : G), f y * (∫ (z : G), g (-z + y) ∂ν)⁻¹ ∂ν) * ∫ (x : G), g x ∂μ
• MeasureTheory.Measure.integral_isMulLeftInvariant_isMulRightInvariant_combo 📋 Mathlib.MeasureTheory.Measure.Haar.Unique
  {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] {μ ν : MeasureTheory.Measure G} [MeasureTheory.IsFiniteMeasureOnCompacts μ] [MeasureTheory.IsFiniteMeasureOnCompacts ν] [μ.IsMulLeftInvariant] [ν.IsMulRightInvariant] [ν.IsOpenPosMeasure] {f g : G → ℝ} (hf : Continuous f) (h'f : HasCompactSupport f) (hg : Continuous g) (h'g : HasCompactSupport g) (g_nonneg : 0 ≤ g) {x₀ : G} (g_pos : g x₀ ≠ 0) : ∫ (x : G), f x ∂μ = (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) * ∫ (x : G), g x ∂μ
• MeasureTheory.Measure.addHaarScalarFactor_eq_integral_div_of_continuous_nonneg_pos 📋 Mathlib.MeasureTheory.Measure.Haar.Unique
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] (μ' μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsAddLeftInvariant] {f : C(G, ℝ)} (hf : HasCompactSupport ⇑f ∧ 0 ≤ f ∧ f 0 ≠ 0) : ↑(μ'.addHaarScalarFactor μ) = (∫ (x : G), f x ∂μ') / ∫ (x : G), f x ∂μ
• MeasureTheory.Measure.haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos 📋 Mathlib.MeasureTheory.Measure.Haar.Unique
  {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (μ' μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsMulLeftInvariant] {f : C(G, ℝ)} (hf : HasCompactSupport ⇑f ∧ 0 ≤ f ∧ f 1 ≠ 0) : ↑(μ'.haarScalarFactor μ) = (∫ (x : G), f x ∂μ') / ∫ (x : G), f x ∂μ
• ExistsContDiffBumpBase.u_compact_support 📋 Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
  (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] : HasCompactSupport ExistsContDiffBumpBase.u
• ExistsContDiffBumpBase.w_compact_support 📋 Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
  (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {D : ℝ} (Dpos : 0 < D) : HasCompactSupport (ExistsContDiffBumpBase.w D)
• exists_contDiff_tsupport_subset 📋 Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {x : E} {n : ℕ∞} (hs : s ∈ nhds x) : ∃ f, tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ (↑n) f ∧ Set.range f ⊆ Set.Icc 0 1 ∧ f x = 1
• ContDiffBump.hasCompactSupport_normed 📋 Mathlib.Analysis.Calculus.BumpFunction.Normed
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [HasContDiffBump E] [MeasurableSpace E] {c : E} (f : ContDiffBump c) {μ : MeasureTheory.Measure E} [BorelSpace E] [FiniteDimensional ℝ E] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] : HasCompactSupport (f.normed μ)
• HasCompactSupport.integral_Iic_deriv_eq 📋 Mathlib.MeasureTheory.Integral.IntegralEqImproper
  {E : Type u_1} {f : ℝ → E} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (hf : ContDiff ℝ 1 f) (h2f : HasCompactSupport f) (b : ℝ) : ∫ (x : ℝ) in Set.Iic b, deriv f x = f b
• HasCompactSupport.integral_Ioi_deriv_eq 📋 Mathlib.MeasureTheory.Integral.IntegralEqImproper
  {E : Type u_1} {f : ℝ → E} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (hf : ContDiff ℝ 1 f) (h2f : HasCompactSupport f) (b : ℝ) : ∫ (x : ℝ) in Set.Ioi b, deriv f x = -f b
• HasCompactSupport.enorm_le_lintegral_Ici_deriv 📋 Mathlib.MeasureTheory.Integral.IntegralEqImproper
  {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ → F} (hf : ContDiff ℝ 1 f) (h'f : HasCompactSupport f) (x : ℝ) : ‖f x‖ₑ ≤ ∫⁻ (y : ℝ) in Set.Iic x, ‖deriv f y‖ₑ
• ContMDiff.extend_zero 📋 Mathlib.Geometry.Manifold.ContMDiff.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M] [ChartedSpace H' M'] [T2Space M] [Zero M'] {n : WithTop ℕ∞} {U : TopologicalSpace.Opens M} {f : ↥U → M'} (supp : HasCompactSupport f) (diff : ContMDiff I I' n f) : ContMDiff I I' n (Function.extend Subtype.val f 0)
• SmoothBumpFunction.hasCompactSupport 📋 Mathlib.Geometry.Manifold.BumpFunction
  {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {c : M} (f : SmoothBumpFunction I c) [FiniteDimensional ℝ E] [T2Space M] : HasCompactSupport ↑f
• BumpCovering.exists_isSubordinate_hasCompactSupport_of_locallyFinite_t2space 📋 Mathlib.Topology.PartitionOfUnity
  {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} [LocallyCompactSpace X] [T2Space X] (hs : IsCompact s) (U : ι → Set X) (ho : ∀ (i : ι), IsOpen (U i)) (hf : LocallyFinite U) (hU : s ⊆ ⋃ i, U i) : ∃ f, f.IsSubordinate U ∧ ∀ (i : ι), HasCompactSupport ⇑(f i)
• PartitionOfUnity.exists_isSubordinate_of_locallyFinite_t2space 📋 Mathlib.Topology.PartitionOfUnity
  {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} [LocallyCompactSpace X] [T2Space X] (hs : IsCompact s) (U : ι → Set X) (ho : ∀ (i : ι), IsOpen (U i)) (hf : LocallyFinite U) (hU : s ⊆ ⋃ i, U i) : ∃ f, f.IsSubordinate U ∧ ∀ (i : ι), HasCompactSupport ⇑(f i)
• exists_continuous_sum_one_of_isOpen_isCompact 📋 Mathlib.Topology.PartitionOfUnity
  {X : Type v} [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] {n : ℕ} {t : Set X} {s : Fin n → Set X} (hs : ∀ (i : Fin n), IsOpen (s i)) (htcp : IsCompact t) (hst : t ⊆ ⋃ i, s i) : ∃ f, (∀ (i : Fin n), tsupport ⇑(f i) ⊆ s i) ∧ Set.EqOn (∑ i, ⇑(f i)) 1 t ∧ (∀ (i : Fin n) (x : X), (f i) x ∈ Set.Icc 0 1) ∧ ∀ (i : Fin n), HasCompactSupport ⇑(f i)
• BumpCovering.exists_isSubordinate_of_locallyFinite_of_prop_t2space 📋 Mathlib.Topology.PartitionOfUnity
  {ι : Type u} {X : Type v} [TopologicalSpace X] {s : Set X} [LocallyCompactSpace X] [T2Space X] (p : (X → ℝ) → Prop) (h01 : ∀ (s t : Set X), IsClosed s → IsCompact t → Disjoint s t → ∃ f, p ⇑f ∧ Set.EqOn (⇑f) 0 s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Set.Icc 0 1) (hs : IsCompact s) (U : ι → Set X) (ho : ∀ (i : ι), IsOpen (U i)) (hf : LocallyFinite U) (hU : s ⊆ ⋃ i, U i) : ∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U ∧ ∀ (i : ι), HasCompactSupport ⇑(f i)
• 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
• IsOpen.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} {U : Set E} (hU : IsOpen U) (hf : MeasureTheory.LocallyIntegrableOn f U μ) (h : ∀ (g : E → ℝ), ContDiff ℝ (↑⊤) g → HasCompactSupport g → tsupport g ⊆ U → ∫ (x : E), g x • f x ∂μ = 0) : ∀ᵐ (x : E) ∂μ, x ∈ U → 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
• IsOpen.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] {U : Set M} (hU : IsOpen U) (hf : MeasureTheory.LocallyIntegrableOn f U μ) (h : ∀ (g : M → ℝ), ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) g → HasCompactSupport g → tsupport g ⊆ U → ∫ (x : M), g x • f x ∂μ = 0) : ∀ᵐ (x : M) ∂μ, x ∈ U → f x = 0
• IsOpen.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} {U : Set M} (hU : IsOpen U) (hSig : IsSigmaCompact U) (hf : MeasureTheory.LocallyIntegrableOn f U μ) (h : ∀ (g : M → ℝ), ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) g → HasCompactSupport g → tsupport g ⊆ U → ∫ (x : M), g x • f x ∂μ = 0) : ∀ᵐ (x : M) ∂μ, x ∈ U → f x = 0
• 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.integral_lineDeriv_mul_eq 📋 Mathlib.Analysis.Calculus.Rademacher
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {C D : NNReal} {f g : E → ℝ} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] (hf : LipschitzWith C f) (hg : LipschitzWith D g) (h'g : HasCompactSupport g) (v : E) : ∫ (x : E), lineDeriv ℝ f x v * g x ∂μ = ∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ
• LipschitzWith.integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul' 📋 Mathlib.Analysis.Calculus.Rademacher
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {C : NNReal} {f g : E → ℝ} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] (hf : LipschitzWith C f) (h'f : HasCompactSupport f) (hg : Continuous g) (v : E) : Filter.Tendsto (fun t => ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
• ContDiffMapSupportedIn.compact_supp 📋 Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
  {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (f : ContDiffMapSupportedIn E F n K) : HasCompactSupport ⇑f
• ContDiffMapSupportedIn.hasCompactSupport 📋 Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
  {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (f : ContDiffMapSupportedIn E F n K) : HasCompactSupport ⇑f
• TestFunction.hasCompactSupport' 📋 Mathlib.Analysis.Distribution.TestFunction
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} (self : TestFunction Ω F n) : HasCompactSupport self.toFun
• TestFunctionClass.map_hasCompactSupport 📋 Mathlib.Analysis.Distribution.TestFunction
  {B : Type u_6} {E : outParam (Type u_7)} {inst✝ : NormedAddCommGroup E} {inst✝¹ : NormedSpace ℝ E} {Ω : outParam (TopologicalSpace.Opens E)} {F : outParam (Type u_8)} {inst✝² : NormedAddCommGroup F} {inst✝³ : NormedSpace ℝ F} {n : outParam ℕ∞} [self : TestFunctionClass B Ω F n] (f : B) : HasCompactSupport ⇑f
• TestFunction.hasCompactSupport 📋 Mathlib.Analysis.Distribution.TestFunction
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} (f : TestFunction Ω F n) : HasCompactSupport ⇑f
• TestFunction.mk 📋 Mathlib.Analysis.Distribution.TestFunction
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} (toFun : E → F) (contDiff' : ContDiff ℝ (↑n) toFun) (hasCompactSupport' : HasCompactSupport toFun) (tsupport_subset' : tsupport toFun ⊆ ↑Ω) : TestFunction Ω F n
• TestFunctionClass.mk 📋 Mathlib.Analysis.Distribution.TestFunction
  {B : Type u_6} {E : outParam (Type u_7)} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : outParam (TopologicalSpace.Opens E)} {F : outParam (Type u_8)} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : outParam ℕ∞} [toDFunLike : DFunLike B E fun x => F] (map_contDiff : ∀ (f : B), ContDiff ℝ ↑n ⇑f) (map_hasCompactSupport : ∀ (f : B), HasCompactSupport ⇑f) (tsupport_map_subset : ∀ (f : B), tsupport ⇑f ⊆ ↑Ω) : TestFunctionClass B Ω F n
• TestFunction.coe_mk 📋 Mathlib.Analysis.Distribution.TestFunction
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ∞} {f : E → F} {contDiff : ContDiff ℝ (↑n) f} {hasCompactSupport : HasCompactSupport f} {tsupport_subset : tsupport f ⊆ ↑Ω} : ⇑{ toFun := f, contDiff' := contDiff, hasCompactSupport' := hasCompactSupport, tsupport_subset' := tsupport_subset } = f
• HasCompactSupport.hasTemperateGrowth 📋 Mathlib.Analysis.Distribution.TemperateGrowth
  {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} (h₁ : HasCompactSupport f) (h₂ : ContDiff ℝ (↑⊤) f) : Function.HasTemperateGrowth f
• MeasureTheory.Integrable.exists_hasCompactSupport_integral_sub_le 📋 Mathlib.MeasureTheory.Function.ContinuousMapDense
  {α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [NormedSpace ℝ E] [R1Space α] [WeaklyLocallyCompactSpace α] [μ.Regular] {f : α → E} (hf : MeasureTheory.Integrable f μ) {ε : ℝ} (hε : 0 < ε) : ∃ g, HasCompactSupport g ∧ ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ Continuous g ∧ MeasureTheory.Integrable g μ
• MeasureTheory.Integrable.exists_hasCompactSupport_lintegral_sub_le 📋 Mathlib.MeasureTheory.Function.ContinuousMapDense
  {α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [NormedSpace ℝ E] [R1Space α] [WeaklyLocallyCompactSpace α] [μ.Regular] {f : α → E} (hf : MeasureTheory.Integrable f μ) {ε : ENNReal} (hε : ε ≠ 0) : ∃ g, HasCompactSupport g ∧ ∫⁻ (x : α), ‖f x - g x‖ₑ ∂μ ≤ ε ∧ Continuous g ∧ MeasureTheory.Integrable g μ
• MeasureTheory.MemLp.exists_hasCompactSupport_integral_rpow_sub_le 📋 Mathlib.MeasureTheory.Function.ContinuousMapDense
  {α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [NormedSpace ℝ E] [R1Space α] [WeaklyLocallyCompactSpace α] [μ.Regular] {p : ℝ} (hp : 0 < p) {f : α → E} (hf : MeasureTheory.MemLp f (ENNReal.ofReal p) μ) {ε : ℝ} (hε : 0 < ε) : ∃ g, HasCompactSupport g ∧ ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧ Continuous g ∧ MeasureTheory.MemLp g (ENNReal.ofReal p) μ
• MeasureTheory.MemLp.exists_hasCompactSupport_eLpNorm_sub_le 📋 Mathlib.MeasureTheory.Function.ContinuousMapDense
  {α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedSpace ℝ E] [R1Space α] [WeaklyLocallyCompactSpace α] [μ.Regular] (hp : p ≠ ⊤) {f : α → E} (hf : MeasureTheory.MemLp f p μ) {ε : ENNReal} (hε : ε ≠ 0) : ∃ g, HasCompactSupport g ∧ MeasureTheory.eLpNorm (f - g) p μ ≤ ε ∧ Continuous g ∧ MeasureTheory.MemLp g p μ
• HasCompactSupport.exist_eLpNorm_sub_le_of_continuous 📋 Mathlib.Analysis.Normed.Lp.SmoothApprox
  {E : Type u_3} {F : Type u_4} [MeasurableSpace E] [NormedAddCommGroup F] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] [NormedSpace ℝ F] (μ : MeasureTheory.Measure E := by volume_tac) [MeasureTheory.IsFiniteMeasureOnCompacts μ] {p : ENNReal} {ε : ℝ} (hε : 0 < ε) {f : E → F} (h₁ : HasCompactSupport f) (h₂ : Continuous f) : ∃ g, HasCompactSupport g ∧ ContDiff ℝ (↑⊤) g ∧ MeasureTheory.eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
• MeasureTheory.MemLp.exist_eLpNorm_sub_le 📋 Mathlib.Analysis.Normed.Lp.SmoothApprox
  {E : Type u_3} {F : Type u_4} [MeasurableSpace E] [NormedAddCommGroup F] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] [NormedSpace ℝ F] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {p : ENNReal} (hp : p ≠ ⊤) (hp₂ : 1 ≤ p) {f : E → F} (hf : MeasureTheory.MemLp f p μ) {ε : ℝ} (hε : 0 < ε) : ∃ g, HasCompactSupport g ∧ ContDiff ℝ (↑⊤) g ∧ MeasureTheory.eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
• MeasureTheory.Lp.dense_hasCompactSupport_contDiff 📋 Mathlib.Analysis.Normed.Lp.SmoothApprox
  {E : Type u_3} {F : Type u_4} [MeasurableSpace E] [NormedAddCommGroup F] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] [NormedSpace ℝ F] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {p : ENNReal} (hp : p ≠ ⊤) [hp₂ : Fact (1 ≤ p)] : Dense {f | ∃ g, ↑↑f =ᵐ[μ] g ∧ HasCompactSupport g ∧ ContDiff ℝ (↑⊤) g}
• HasCompactSupport.toSchwartzMap 📋 Mathlib.Analysis.Distribution.SchwartzSpace.Basic
  {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} (h₁ : HasCompactSupport f) (h₂ : ContDiff ℝ (↑⊤) f) : SchwartzMap E F
• HasCompactSupport.toSchwartzMap_toFun 📋 Mathlib.Analysis.Distribution.SchwartzSpace.Basic
  {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} (h₁ : HasCompactSupport f) (h₂ : ContDiff ℝ (↑⊤) f) (a✝ : E) : (h₁.toSchwartzMap h₂) a✝ = f a✝
• tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support 📋 Mathlib.Analysis.Fourier.RiemannLebesgueLemma
  {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : V → E} [NormedAddCommGroup V] [MeasurableSpace V] [BorelSpace V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] (hf1 : Continuous f) (hf2 : HasCompactSupport f) : Filter.Tendsto (fun w => ∫ (v : V), Real.fourierChar (-inner ℝ v w) • f v) (Filter.cocompact V) (nhds 0)
• MeasureTheory.eLpNorm_le_eLpNorm_fderiv_one 📋 Mathlib.Analysis.FunctionalSpaces.SobolevInequality
  {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {u : E → F} (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u) {p : NNReal} (hp : (↑(Module.finrank ℝ E)).HolderConjugate p) : MeasureTheory.eLpNorm u (↑p) μ ≤ ↑(MeasureTheory.eLpNormLESNormFDerivOneConst μ ↑p) * MeasureTheory.eLpNorm (fderiv ℝ u) 1 μ
• MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv 📋 Mathlib.Analysis.FunctionalSpaces.SobolevInequality
  {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {u : E → F} (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u) {p : ℝ} (hp : (↑(Module.finrank ℝ E)).HolderConjugate p) : ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂μ ≤ ↑(MeasureTheory.lintegralPowLePowLIntegralFDerivConst μ p) * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ∂μ) ^ p
• MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq 📋 Mathlib.Analysis.FunctionalSpaces.SobolevInequality
  {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] [FiniteDimensional ℝ F] {u : E → F} (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u) {p p' : NNReal} (hp : 1 ≤ p) (hn : 0 < Module.finrank ℝ E) (hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑(Module.finrank ℝ E))⁻¹) : MeasureTheory.eLpNorm u (↑p') μ ≤ ↑(MeasureTheory.SNormLESNormFDerivOfEqConst F μ ↑p) * MeasureTheory.eLpNorm (fderiv ℝ u) (↑p) μ
• MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq_inner 📋 Mathlib.Analysis.FunctionalSpaces.SobolevInequality
  {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {F' : Type u_5} [NormedAddCommGroup F'] [InnerProductSpace ℝ F'] {u : E → F'} (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u) {p p' : NNReal} (hp : 1 ≤ p) (hn : 0 < Module.finrank ℝ E) (hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑(Module.finrank ℝ E))⁻¹) : MeasureTheory.eLpNorm u (↑p') μ ≤ ↑(MeasureTheory.eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * MeasureTheory.eLpNorm (fderiv ℝ u) (↑p) μ
• MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv_aux 📋 Mathlib.Analysis.FunctionalSpaces.SobolevInequality
  {ι : Type u_1} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] [Fintype ι] {p : ℝ} (hp : (↑(Fintype.card ι)).HolderConjugate p) {u : (ι → ℝ) → F} (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u) : ∫⁻ (x : ι → ℝ), ‖u x‖ₑ ^ p ≤ (∫⁻ (x : ι → ℝ), ‖fderiv ℝ u x‖ₑ) ^ p
• HasCompactSupport.inf 📋 Mathlib.Topology.Algebra.Order.Support
  {X : Type u_1} {M : Type u_2} [TopologicalSpace X] [Zero M] [SemilatticeInf M] {f g : X → M} (hf : HasCompactSupport f) (hg : HasCompactSupport g) : HasCompactSupport (f ⊓ g)
• HasCompactSupport.sup 📋 Mathlib.Topology.Algebra.Order.Support
  {X : Type u_1} {M : Type u_2} [TopologicalSpace X] [Zero M] [SemilatticeSup M] {f g : X → M} (hf : HasCompactSupport f) (hg : HasCompactSupport g) : HasCompactSupport (f ⊔ g)
• CompactlySupportedContinuousMap.mk 📋 Mathlib.Topology.ContinuousMap.CompactlySupported
  {α : Type u_5} {β : Type u_6} [TopologicalSpace α] [Zero β] [TopologicalSpace β] (toContinuousMap : C(α, β)) (hasCompactSupport' : HasCompactSupport toContinuousMap.toFun) : CompactlySupportedContinuousMap α β
• CompactlySupportedContinuousMap.hasCompactSupport' 📋 Mathlib.Topology.ContinuousMap.CompactlySupported
  {α : Type u_5} {β : Type u_6} [TopologicalSpace α] [Zero β] [TopologicalSpace β] (self : CompactlySupportedContinuousMap α β) : HasCompactSupport self.toFun
• CompactlySupportedContinuousMap.hasCompactSupport 📋 Mathlib.Topology.ContinuousMap.CompactlySupported
  {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] (f : CompactlySupportedContinuousMap α β) : HasCompactSupport ⇑f
• CompactlySupportedContinuousMapClass.hasCompactSupport 📋 Mathlib.Topology.ContinuousMap.CompactlySupported
  {F : Type u_5} {α : outParam (Type u_6)} {β : outParam (Type u_7)} {inst✝ : TopologicalSpace α} {inst✝¹ : Zero β} {inst✝² : TopologicalSpace β} {inst✝³ : FunLike F α β} [self : CompactlySupportedContinuousMapClass F α β] (f : F) : HasCompactSupport ⇑f
• CompactlySupportedContinuousMapClass.mk 📋 Mathlib.Topology.ContinuousMap.CompactlySupported
  {F : Type u_5} {α : outParam (Type u_6)} {β : outParam (Type u_7)} [TopologicalSpace α] [Zero β] [TopologicalSpace β] [FunLike F α β] [toContinuousMapClass : ContinuousMapClass F α β] (hasCompactSupport : ∀ (f : F), HasCompactSupport ⇑f) : CompactlySupportedContinuousMapClass F α β
• CompactlySupportedContinuousMap.coe_mk 📋 Mathlib.Topology.ContinuousMap.CompactlySupported
  {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [Zero β] (f : C(α, β)) (h : HasCompactSupport ⇑f) : ⇑{ toContinuousMap := f, hasCompactSupport' := h } = ⇑f
• IsCompact.measure_eq_biInf_integral_hasCompactSupport 📋 Mathlib.MeasureTheory.Integral.Regular
  {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] {k : Set X} (hk : IsCompact k) (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.InnerRegularCompactLTTop] [LocallyCompactSpace X] [RegularSpace X] : μ k = ⨅ f, ⨅ (_ : Continuous f), ⨅ (_ : HasCompactSupport f), ⨅ (_ : Set.EqOn f 1 k), ⨅ (_ : 0 ≤ f), ENNReal.ofReal (∫ (x : X), f x ∂μ)
• ofCompactSupport 📋 Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
  {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [NonUnitalNormedRing γ] (g : α → γ) (hg₁ : Continuous g) (hg₂ : HasCompactSupport g) : BoundedContinuousFunction α γ
• ofCompactSupport_mem 📋 Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
  {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [NonUnitalNormedRing γ] (g : α → γ) (hg₁ : Continuous g) (hg₂ : HasCompactSupport g) : ofCompactSupport g hg₁ hg₂ ∈ compactlySupported α γ
• mem_compactlySupported 📋 Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
  {α : Type u_1} {γ : Type u_2} [TopologicalSpace α] [NonUnitalNormedRing γ] {f : BoundedContinuousFunction α γ} : f ∈ compactlySupported α γ ↔ HasCompactSupport ⇑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