Loogle!

Result

Found 166 declarations mentioning Metric.eball.

• Metric.eball 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [EDist α] (x : α) (ε : ENNReal) : Set α
• Metric.isOpen_eball 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} {x : α} [PseudoEMetricSpace α] {r : ENNReal} : IsOpen (Metric.eball x r)
• Metric.eball_subset_closedEBall 📋 Mathlib.Topology.EMetricSpace.Defs
  {ε : ENNReal} {α : Type u_4} [EDist α] {x : α} : Metric.eball x ε ⊆ Metric.closedEBall x ε
• Metric.eball_zero 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_4} [EDist α] {x : α} : Metric.eball x 0 = ∅
• Metric.eball_subset_eball 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} {x : α} {ε₁ ε₂ : ENNReal} [EDist α] (h : ε₁ ≤ ε₂) : Metric.eball x ε₁ ⊆ Metric.eball x ε₂
• Metric.isClosed_eball_top 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_2} [PseudoEMetricSpace α] {x : α} : IsClosed (Metric.eball x ⊤)
• Metric.ordConnected_setOfPred_eball_subset 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] (x : α) (s : Set α) : {r | Metric.eball x r ⊆ s}.OrdConnected
• Metric.ordConnected_setOf_eball_subset 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] (x : α) (s : Set α) : {r | Metric.eball x r ⊆ s}.OrdConnected
• Metric.mem_eball 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [EDist α] {x y : α} {ε : ENNReal} : y ∈ Metric.eball x ε ↔ edist y x < ε
• Metric.pos_of_mem_eball 📋 Mathlib.Topology.EMetricSpace.Defs
  {ε : ENNReal} {α : Type u_4} [EDist α] {x y : α} (hy : y ∈ Metric.eball x ε) : 0 < ε
• Metric.eball_eq_empty_iff 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x : α} {ε : ENNReal} : Metric.eball x ε = ∅ ↔ ε = 0
• Metric.nhds_basis_eball 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} {x : α} [PseudoEMetricSpace α] : (nhds x).HasBasis (fun ε => 0 < ε) (Metric.eball x)
• Metric.mem_eball_self 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x : α} {ε : ENNReal} (h : 0 < ε) : x ∈ Metric.eball x ε
• Metric.mem_eball_comm 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x y : α} {ε : ENNReal} : x ∈ Metric.eball y ε ↔ y ∈ Metric.eball x ε
• Metric.mem_eball' 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x y : α} {ε : ENNReal} : y ∈ Metric.eball x ε ↔ edist x y < ε
• Metric.nhdsWithin_basis_eball 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} {x : α} {s : Set α} [PseudoEMetricSpace α] : (nhdsWithin x s).HasBasis (fun ε => 0 < ε) fun ε => Metric.eball x ε ∩ s
• Metric.eball_mem_nhds 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_2} [PseudoEMetricSpace α] (x : α) {ε : ENNReal} (ε0 : 0 < ε) : Metric.eball x ε ∈ nhds x
• EMetric.dense_iff 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_2} [PseudoEMetricSpace α] {s : Set α} : Dense s ↔ ∀ (x : α), ∀ r > 0, (Metric.eball x r ∩ s).Nonempty
• EMetric.isOpen_iff 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} {s : Set α} [PseudoEMetricSpace α] : IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, Metric.eball x ε ⊆ s
• EMetric.mem_nhds_iff 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} {x : α} {s : Set α} [PseudoEMetricSpace α] : s ∈ nhds x ↔ ∃ ε > 0, Metric.eball x ε ⊆ s
• Subtype.preimage_eball 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_3} [EDist α] {p : α → Prop} (a : { a // p a }) (r : ENNReal) : Subtype.val ⁻¹' Metric.eball (↑a) r = Metric.eball a r
• Subtype.image_eball 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_3} [EDist α] {p : α → Prop} (a : { a // p a }) (r : ENNReal) : Subtype.val '' Metric.eball a r = Metric.eball (↑a) r ∩ {a | p a}
• EMetric.mem_nhdsWithin_iff 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} {x : α} {s t : Set α} [PseudoEMetricSpace α] : s ∈ nhdsWithin x t ↔ ∃ ε > 0, Metric.eball x ε ∩ t ⊆ s
• Metric.exists_eball_subset_eball 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x y : α} {ε : ENNReal} (h : y ∈ Metric.eball x ε) : ∃ ε' > 0, Metric.eball y ε' ⊆ Metric.eball x ε
• EMetric.nhds_eq 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} {x : α} [PseudoEMetricSpace α] : nhds x = ⨅ ε, ⨅ (_ : ε > 0), Filter.principal (Metric.eball x ε)
• Metric.eball_subset 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x y : α} {ε₁ ε₂ : ENNReal} (h : edist x y + ε₁ ≤ ε₂) (h' : edist x y ≠ ⊤) : Metric.eball x ε₁ ⊆ Metric.eball y ε₂
• WeakPseudoEMetricSpace.topology_eq_on_restrict 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} {τ : TopologicalSpace α} [self : WeakPseudoEMetricSpace α] (x : α) (r : ENNReal) : IsOpen (Subtype.val ⁻¹' Metric.eball x r)
• Metric.eball_disjoint 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x y : α} {ε₁ ε₂ : ENNReal} (h : ε₁ + ε₂ ≤ edist x y) : Disjoint (Metric.eball x ε₁) (Metric.eball y ε₂)
• Metric.eball_prod_same 📋 Mathlib.Topology.EMetricSpace.Defs
  {β : Type v} {α : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (x : α) (y : β) (r : ENNReal) : Metric.eball x r ×ˢ Metric.eball y r = Metric.eball (x, y) r
• WeakPseudoEMetricSpace.mk 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [τ : TopologicalSpace α] [toEDist : EDist α] (edist_self : ∀ (x : α), edist x x = 0) (edist_comm : ∀ (x y : α), edist x y = edist y x) (edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z) (topology_le : (uniformSpaceOfEDist edist edist_self edist_comm edist_triangle).toTopologicalSpace ≤ τ) (topology_eq_on_restrict : ∀ (x : α) (r : ENNReal), IsOpen (Subtype.val ⁻¹' Metric.eball x r)) : WeakPseudoEMetricSpace α
• Metric.eball_top 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x : α) : Metric.eball x ⊤ = Set.univ
• Metric.eball_top_eq_univ 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x : α) : Metric.eball x ⊤ = Set.univ
• Metric.eball_ofReal 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.eball x (ENNReal.ofReal ε) = Metric.ball x ε
• Metric.eball_coe 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : NNReal} : Metric.eball x ↑ε = Metric.ball x ↑ε
• EMetric.totallyBounded_iff 📋 Mathlib.Topology.EMetricSpace.Basic
  {γ : Type u} [PseudoEMetricSpace γ] {s : Set γ} : TotallyBounded s ↔ ∀ ε > 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, Metric.eball y ε
• EMetric.totallyBounded_iff' 📋 Mathlib.Topology.EMetricSpace.Basic
  {γ : Type u} [PseudoEMetricSpace γ] {s : Set γ} : TotallyBounded s ↔ ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, Metric.eball y ε
• lebesgue_number_lemma_of_emetric 📋 Mathlib.Topology.EMetricSpace.Basic
  {γ : Type w} [EMetricSpace γ] {s : Set γ} {ι : Sort u_2} {c : ι → Set γ} (hs : IsCompact s) (hc₁ : ∀ (i : ι), IsOpen (c i)) (hc₂ : s ⊆ ⋃ i, c i) : ∃ δ > 0, ∀ x ∈ s, ∃ i, Metric.eball x δ ⊆ c i
• lebesgue_number_lemma_of_emetric_nhds 📋 Mathlib.Topology.EMetricSpace.Basic
  {γ : Type w} [EMetricSpace γ] {s : Set γ} {c : γ → Set γ} (hs : IsCompact s) (hc : ∀ x ∈ s, c x ∈ nhds x) : ∃ δ > 0, ∀ x ∈ s, ∃ y, Metric.eball x δ ⊆ c y
• lebesgue_number_lemma_of_emetric_nhdsWithin 📋 Mathlib.Topology.EMetricSpace.Basic
  {γ : Type w} [EMetricSpace γ] {s : Set γ} {c : γ → Set γ} (hs : IsCompact s) (hc : ∀ x ∈ s, c x ∈ nhdsWithin x s) : ∃ δ > 0, ∀ x ∈ s, ∃ y, Metric.eball x δ ∩ s ⊆ c y
• lebesgue_number_lemma_of_emetric_sUnion 📋 Mathlib.Topology.EMetricSpace.Basic
  {γ : Type w} [EMetricSpace γ] {s : Set γ} {c : Set (Set γ)} (hs : IsCompact s) (hc₁ : ∀ t ∈ c, IsOpen t) (hc₂ : s ⊆ ⋃₀ c) : ∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, Metric.eball x δ ⊆ t
• lebesgue_number_lemma_of_emetric_nhds' 📋 Mathlib.Topology.EMetricSpace.Basic
  {γ : Type w} [EMetricSpace γ] {s : Set γ} {c : (x : γ) → x ∈ s → Set γ} (hs : IsCompact s) (hc : ∀ (x : γ) (hx : x ∈ s), c x hx ∈ nhds x) : ∃ δ > 0, ∀ x ∈ s, ∃ y, Metric.eball x δ ⊆ c ↑y ⋯
• lebesgue_number_lemma_of_emetric_nhdsWithin' 📋 Mathlib.Topology.EMetricSpace.Basic
  {γ : Type w} [EMetricSpace γ] {s : Set γ} {c : (x : γ) → x ∈ s → Set γ} (hs : IsCompact s) (hc : ∀ (x : γ) (hx : x ∈ s), c x hx ∈ nhdsWithin x s) : ∃ δ > 0, ∀ x ∈ s, ∃ y, Metric.eball x δ ∩ s ⊆ c ↑y ⋯
• mem_eball_one_iff 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedGroup E] {a : E} {r : ENNReal} : a ∈ Metric.eball 1 r ↔ ‖a‖ₑ < r
• mem_eball_zero_iff 📋 Mathlib.Analysis.Normed.Group.Basic
  {E : Type u_4} [SeminormedAddGroup E] {a : E} {r : ENNReal} : a ∈ Metric.eball 0 r ↔ ‖a‖ₑ < r
• Metric.ediam_eball_le 📋 Mathlib.Topology.EMetricSpace.Diam
  {X : Type u_2} {x : X} [TopologicalSpace X] [WeakPseudoEMetricSpace X] {r : ENNReal} : Metric.ediam (Metric.eball x r) ≤ 2 * r
• LipschitzWith.mapsTo_eball 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (h : LipschitzWith K f) (hK : K ≠ 0) (x : α) (r : ENNReal) : Set.MapsTo f (Metric.eball x r) (Metric.eball (f x) (↑K * r))
• Isometry.mapsTo_eball 📋 Mathlib.Topology.MetricSpace.Isometry
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (hf : Isometry f) (x : α) (r : ENNReal) : Set.MapsTo f (Metric.eball x r) (Metric.eball (f x) r)
• Isometry.preimage_eball 📋 Mathlib.Topology.MetricSpace.Isometry
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (h : Isometry f) (x : α) (r : ENNReal) : f ⁻¹' Metric.eball (f x) r = Metric.eball x r
• IsometryEquiv.image_eball 📋 Mathlib.Topology.MetricSpace.Isometry
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) (x : α) (r : ENNReal) : ⇑h '' Metric.eball x r = Metric.eball (h x) r
• IsometryEquiv.preimage_eball 📋 Mathlib.Topology.MetricSpace.Isometry
  {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (h : α ≃ᵢ β) (x : β) (r : ENNReal) : ⇑h ⁻¹' Metric.eball x r = Metric.eball (h.symm x) r
• metricSpaceEMetricBall 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {β : Type u_2} [EMetricSpace β] (a : β) (r : ENNReal) : MetricSpace ↑(Metric.eball a r)
• edist_ne_top_of_mem_ball 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {β : Type u_2} [EMetricSpace β] {a : β} {r : ENNReal} (x y : ↑(Metric.eball a r)) : edist ↑x ↑y ≠ ⊤
• nhds_eq_nhds_emetric_ball 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {β : Type u_2} [EMetricSpace β] (a x : β) (r : ENNReal) (h : x ∈ Metric.eball a r) : nhds x = Filter.map Subtype.val (nhds ⟨x, h⟩)
• Metric.preimage_add_left_eball 📋 Mathlib.Topology.MetricSpace.IsometricSMul
  {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsIsometricVAdd G G] (a b : G) (r : ENNReal) : (fun x => a + x) ⁻¹' Metric.eball b r = Metric.eball (-a + b) r
• Metric.preimage_mul_left_eball 📋 Mathlib.Topology.MetricSpace.IsometricSMul
  {G : Type v} [Group G] [PseudoEMetricSpace G] [IsIsometricSMul G G] (a b : G) (r : ENNReal) : (fun x => a * x) ⁻¹' Metric.eball b r = Metric.eball (a⁻¹ * b) r
• Metric.preimage_add_right_eball 📋 Mathlib.Topology.MetricSpace.IsometricSMul
  {G : Type v} [AddGroup G] [PseudoEMetricSpace G] [IsIsometricVAdd Gᵃᵒᵖ G] (a b : G) (r : ENNReal) : (fun x => x + a) ⁻¹' Metric.eball b r = Metric.eball (b - a) r
• Metric.preimage_mul_right_eball 📋 Mathlib.Topology.MetricSpace.IsometricSMul
  {G : Type v} [Group G] [PseudoEMetricSpace G] [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) (r : ENNReal) : (fun x => x * a) ⁻¹' Metric.eball b r = Metric.eball (b / a) r
• Metric.smul_eball 📋 Mathlib.Topology.MetricSpace.IsometricSMul
  {G : Type v} {X : Type w} [PseudoEMetricSpace X] [Group G] [MulAction G X] [IsIsometricSMul G X] (c : G) (x : X) (r : ENNReal) : c • Metric.eball x r = Metric.eball (c • x) r
• Metric.vadd_eball 📋 Mathlib.Topology.MetricSpace.IsometricSMul
  {G : Type v} {X : Type w} [PseudoEMetricSpace X] [AddGroup G] [AddAction G X] [IsIsometricVAdd G X] (c : G) (x : X) (r : ENNReal) : c +ᵥ Metric.eball x r = Metric.eball (c +ᵥ x) r
• Metric.preimage_smul_eball 📋 Mathlib.Topology.MetricSpace.IsometricSMul
  {G : Type v} {X : Type w} [PseudoEMetricSpace X] [Group G] [MulAction G X] [IsIsometricSMul G X] (c : G) (x : X) (r : ENNReal) : (fun x => c • x) ⁻¹' Metric.eball x r = Metric.eball (c⁻¹ • x) r
• Metric.preimage_vadd_eball 📋 Mathlib.Topology.MetricSpace.IsometricSMul
  {G : Type v} {X : Type w} [PseudoEMetricSpace X] [AddGroup G] [AddAction G X] [IsIsometricVAdd G X] (c : G) (x : X) (r : ENNReal) : (fun x => c +ᵥ x) ⁻¹' Metric.eball x r = Metric.eball (-c +ᵥ x) r
• Dilation.mapsTo_eball 📋 Mathlib.Topology.MetricSpace.Dilation
  {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) (x : α) (r : ENNReal) : Set.MapsTo (⇑f) (Metric.eball x r) (Metric.eball (f x) (↑(Dilation.ratio f) * r))
• measurableSet_eball 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
  {α : Type u_1} [PseudoEMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {x : α} {ε : ENNReal} : MeasurableSet (Metric.eball x ε)
• Metric.measure_eball_pos 📋 Mathlib.MeasureTheory.Measure.OpenPos
  {X : Type u_1} [PseudoEMetricSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] (x : X) {r : ENNReal} (hr : r ≠ 0) : 0 < μ (Metric.eball x r)
• convex_eball 📋 Mathlib.Analysis.Normed.Module.Convex
  {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (a : E) (r : ENNReal) : Convex ℝ (Metric.eball a r)
• Real.volume_eball 📋 Mathlib.MeasureTheory.Measure.Lebesgue.Basic
  (a : ℝ) (r : ENNReal) : MeasureTheory.volume (Metric.eball a r) = 2 * r
• IsCompact.uniform_oscillation 📋 Mathlib.Analysis.Oscillation
  {E : Type u} {F : Type v} [PseudoEMetricSpace F] [PseudoEMetricSpace E] {K : Set E} (comp : IsCompact K) {f : E → F} {ε : ENNReal} (hK : ∀ x ∈ K, oscillation f x < ε) : ∃ δ > 0, ∀ x ∈ K, Metric.ediam (f '' Metric.eball x (ENNReal.ofReal δ)) ≤ ε
• IsCompact.uniform_oscillationWithin 📋 Mathlib.Analysis.Oscillation
  {E : Type u} {F : Type v} [PseudoEMetricSpace F] [PseudoEMetricSpace E] {K : Set E} {f : E → F} {D : Set E} {ε : ENNReal} (comp : IsCompact K) (hK : ∀ x ∈ K, oscillationWithin f D x < ε) : ∃ δ > 0, ∀ x ∈ K, Metric.ediam (f '' (Metric.eball x (ENNReal.ofReal δ) ∩ D)) ≤ ε
• FormalMultilinearSeries.summable_norm_apply 📋 Mathlib.Analysis.Analytic.ConvergenceRadius
  {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {x : E} (hx : x ∈ Metric.eball 0 p.radius) : Summable fun n => ‖(p n) fun x_1 => x‖
• FormalMultilinearSeries.summable 📋 Mathlib.Analysis.Analytic.ConvergenceRadius
  {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (p : FormalMultilinearSeries 𝕜 E F) {x : E} (hx : x ∈ Metric.eball 0 p.radius) : Summable fun n => (p n) fun x_1 => x
• FormalMultilinearSeries.hasSum 📋 Mathlib.Analysis.Analytic.ConvergenceRadius
  {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (p : FormalMultilinearSeries 𝕜 E F) {x : E} (hx : x ∈ Metric.eball 0 p.radius) : HasSum (fun n => (p n) fun x_1 => x) (p.sum x)
• HasFPowerSeriesOnBall.congr 📋 Mathlib.Analysis.Analytic.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) (hg : Set.EqOn f g (Metric.eball x r)) : HasFPowerSeriesOnBall g p x r
• HasFPowerSeriesOnBall.unique 📋 Mathlib.Analysis.Analytic.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) (hg : HasFPowerSeriesOnBall g p x r) : Set.EqOn f g (Metric.eball x r)
• HasFPowerSeriesOnBall.continuousOn 📋 Mathlib.Analysis.Analytic.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) : ContinuousOn f (Metric.eball x r)
• HasFPowerSeriesWithinOnBall.congr 📋 Mathlib.Analysis.Analytic.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (h : HasFPowerSeriesWithinOnBall f p s x r) (h' : Set.EqOn g f (s ∩ Metric.eball x r)) (h'' : g x = f x) : HasFPowerSeriesWithinOnBall g p s x r
• HasFPowerSeriesWithinOnBall.congr' 📋 Mathlib.Analysis.Analytic.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (h : HasFPowerSeriesWithinOnBall f p s x r) (h' : Set.EqOn g f (insert x s ∩ Metric.eball x r)) : HasFPowerSeriesWithinOnBall g p s x r
• HasFPowerSeriesWithinOnBall.unique 📋 Mathlib.Analysis.Analytic.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) (hg : HasFPowerSeriesWithinOnBall g p s x r) : Set.EqOn f g (insert x s ∩ Metric.eball x r)
• HasFPowerSeriesWithinOnBall.continuousOn 📋 Mathlib.Analysis.Analytic.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) : ContinuousOn f (insert x s ∩ Metric.eball x r)
• HasFPowerSeriesOnBall.hasSum_sub 📋 Mathlib.Analysis.Analytic.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) {y : E} (hy : y ∈ Metric.eball x r) : HasSum (fun n => (p n) fun x_1 => y - x) (f y)
• HasFPowerSeriesWithinOnBall.hasSum_sub 📋 Mathlib.Analysis.Analytic.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) {y : E} (hy : y ∈ insert x s ∩ Metric.eball x r) : HasSum (fun n => (p n) fun x_1 => y - x) (f y)
• HasFPowerSeriesOnBall.hasSum 📋 Mathlib.Analysis.Analytic.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (self : HasFPowerSeriesOnBall f p x r) {y : E} : y ∈ Metric.eball 0 r → HasSum (fun n => (p n) fun x => y) (f (x + y))
• HasFPowerSeriesOnBall.mk 📋 Mathlib.Analysis.Analytic.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (r_le : r ≤ p.radius) (r_pos : 0 < r) (hasSum : ∀ {y : E}, y ∈ Metric.eball 0 r → HasSum (fun n => (p n) fun x => y) (f (x + y))) : HasFPowerSeriesOnBall f p x r
• HasFPowerSeriesWithinOnBall.hasSum 📋 Mathlib.Analysis.Analytic.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (self : HasFPowerSeriesWithinOnBall f p s x r) {y : E} : x + y ∈ insert x s → y ∈ Metric.eball 0 r → HasSum (fun n => (p n) fun x => y) (f (x + y))
• HasFPowerSeriesWithinOnBall.mk 📋 Mathlib.Analysis.Analytic.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (r_le : r ≤ p.radius) (r_pos : 0 < r) (hasSum : ∀ {y : E}, x + y ∈ insert x s → y ∈ Metric.eball 0 r → HasSum (fun n => (p n) fun x => y) (f (x + y))) : HasFPowerSeriesWithinOnBall f p s x r
• HasFPowerSeriesOnBall.image_sub_sub_deriv_le 📋 Mathlib.Analysis.Analytic.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r r' : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) (hr : r' < r) : ∃ C, ∀ y ∈ Metric.eball x r', ∀ z ∈ Metric.eball x r', ‖f y - f z - (p 1) fun x => y - z‖ ≤ C * max ‖y - x‖ ‖z - x‖ * ‖y - z‖
• HasFPowerSeriesOnBall.isBigO_image_sub_image_sub_deriv_principal 📋 Mathlib.Analysis.Analytic.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r r' : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) (hr : r' < r) : (fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[Filter.principal (Metric.eball (x, x) r')] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖
• HasFPowerSeriesWithinOnBall.image_sub_sub_deriv_le 📋 Mathlib.Analysis.Analytic.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r r' : ENNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) (hr : r' < r) : ∃ C, ∀ y ∈ insert x s ∩ Metric.eball x r', ∀ z ∈ insert x s ∩ Metric.eball x r', ‖f y - f z - (p 1) fun x => y - z‖ ≤ C * max ‖y - x‖ ‖z - x‖ * ‖y - z‖
• HasFPowerSeriesWithinOnBall.isBigO_image_sub_image_sub_deriv_principal 📋 Mathlib.Analysis.Analytic.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r r' : ENNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) (hr : r' < r) : (fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[Filter.principal (Metric.eball (x, x) r' ∩ insert x s ×ˢ insert x s)] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖
• FormalMultilinearSeries.continuousOn 📋 Mathlib.Analysis.Analytic.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} [CompleteSpace F] : ContinuousOn p.sum (Metric.eball 0 p.radius)
• HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn' 📋 Mathlib.Analysis.Analytic.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) : TendstoLocallyUniformlyOn (fun n y => p.partialSum n (y - x)) f Filter.atTop (Metric.eball x r)
• HasFPowerSeriesOnBall.sum 📋 Mathlib.Analysis.Analytic.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (h : HasFPowerSeriesOnBall f p x r) {y : E} (hy : y ∈ Metric.eball 0 r) : f (x + y) = p.sum y
• HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn' 📋 Mathlib.Analysis.Analytic.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) : TendstoLocallyUniformlyOn (fun n y => p.partialSum n (y - x)) f Filter.atTop (insert x s ∩ Metric.eball x r)
• HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn 📋 Mathlib.Analysis.Analytic.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) : TendstoLocallyUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) Filter.atTop (Metric.eball 0 r)
• HasFPowerSeriesOnBall.tendsto_partialSum 📋 Mathlib.Analysis.Analytic.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) {y : E} (hy : y ∈ Metric.eball 0 r) : Filter.Tendsto (fun n => p.partialSum n y) Filter.atTop (nhds (f (x + y)))
• HasFPowerSeriesWithinOnBall.sum 📋 Mathlib.Analysis.Analytic.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (h : HasFPowerSeriesWithinOnBall f p s x r) {y : E} (h'y : x + y ∈ insert x s) (hy : y ∈ Metric.eball 0 r) : f (x + y) = p.sum y
• HasFPowerSeriesOnBall.tendsto_partialSum_prod 📋 Mathlib.Analysis.Analytic.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {y : E} (hf : HasFPowerSeriesOnBall f p x r) (hy : y ∈ Metric.eball 0 r) : Filter.Tendsto (fun z => p.partialSum z.1 z.2) (Filter.atTop ×ˢ nhds y) (nhds (f (x + y)))
• HasFPowerSeriesWithinOnBall.tendsto_partialSum 📋 Mathlib.Analysis.Analytic.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) {y : E} (hy : y ∈ Metric.eball 0 r) (h'y : x + y ∈ insert x s) : Filter.Tendsto (fun n => p.partialSum n y) Filter.atTop (nhds (f (x + y)))
• HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn 📋 Mathlib.Analysis.Analytic.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) : TendstoLocallyUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) Filter.atTop ((fun x_1 => x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r)
• HasFPowerSeriesWithinOnBall.tendsto_partialSum_prod 📋 Mathlib.Analysis.Analytic.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} {y : E} (hf : HasFPowerSeriesWithinOnBall f p s x r) (hy : y ∈ Metric.eball 0 r) (h'y : x + y ∈ insert x s) : Filter.Tendsto (fun z => p.partialSum z.1 z.2) (Filter.atTop ×ˢ nhds y) (nhds (f (x + y)))
• HasFPowerSeriesOnBall.analyticOnNhd 📋 Mathlib.Analysis.Analytic.ChangeOrigin
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) : AnalyticOnNhd 𝕜 f (Metric.eball x r)
• HasFPowerSeriesOnBall.analyticAt_of_mem 📋 Mathlib.Analysis.Analytic.ChangeOrigin
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x y : E} {r : ENNReal} (hf : HasFPowerSeriesOnBall f p x r) (h : y ∈ Metric.eball x r) : AnalyticAt 𝕜 f y
• HasFPowerSeriesWithinOnBall.analyticOn 📋 Mathlib.Analysis.Analytic.ChangeOrigin
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) : AnalyticOn 𝕜 f (insert x s ∩ Metric.eball x r)
• HasFPowerSeriesWithinOnBall.analyticWithinAt_of_mem 📋 Mathlib.Analysis.Analytic.ChangeOrigin
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x y : E} {r : ENNReal} (hf : HasFPowerSeriesWithinOnBall f p s x r) (h : y ∈ insert x s ∩ Metric.eball x r) : AnalyticWithinAt 𝕜 f s y
• FormalMultilinearSeries.analyticOnNhd 📋 Mathlib.Analysis.Analytic.ChangeOrigin
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {p : FormalMultilinearSeries 𝕜 E F} : AnalyticOnNhd 𝕜 p.sum (Metric.eball 0 p.radius)
• HasFiniteFPowerSeriesOnBall.cpolynomialOn 📋 Mathlib.Analysis.Analytic.CPolynomialDef
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {n : ℕ} {x : E} (hf : HasFiniteFPowerSeriesOnBall f p x n r) : CPolynomialOn 𝕜 f (Metric.eball x r)
• HasFiniteFPowerSeriesOnBall.eq_const_of_bound_one 📋 Mathlib.Analysis.Analytic.CPolynomialDef
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {pf : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFiniteFPowerSeriesOnBall f pf x 1 r) (y : E) : y ∈ Metric.eball x r → f y = f x
• HasFiniteFPowerSeriesOnBall.cpolynomialAt_of_mem 📋 Mathlib.Analysis.Analytic.CPolynomialDef
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {n : ℕ} {x y : E} (hf : HasFiniteFPowerSeriesOnBall f p x n r) (h : y ∈ Metric.eball x r) : CPolynomialAt 𝕜 f y
• HasFiniteFPowerSeriesOnBall.congr 📋 Mathlib.Analysis.Analytic.CPolynomialDef
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {n : ℕ} (hf : HasFiniteFPowerSeriesOnBall f p x n r) (hg : Set.EqOn f g (Metric.eball x r)) : HasFiniteFPowerSeriesOnBall g p x n r
• HasFiniteFPowerSeriesOnBall.continuousOn 📋 Mathlib.Analysis.Analytic.CPolynomialDef
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {n : ℕ} (hf : HasFiniteFPowerSeriesOnBall f p x n r) : ContinuousOn f (Metric.eball x r)
• HasFiniteFPowerSeriesOnBall.eq_zero_of_bound_zero 📋 Mathlib.Analysis.Analytic.CPolynomialDef
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {pf : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : HasFiniteFPowerSeriesOnBall f pf x 0 r) (y : E) : y ∈ Metric.eball x r → f y = 0
• HasFiniteFPowerSeriesOnBall.bound_zero_of_eq_zero 📋 Mathlib.Analysis.Analytic.CPolynomialDef
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} (hf : ∀ y ∈ Metric.eball x r, f y = 0) (r_pos : 0 < r) (hp : ∀ (n : ℕ), p n = 0) : HasFiniteFPowerSeriesOnBall f p x 0 r
• HasFiniteFPowerSeriesOnBall.mk' 📋 Mathlib.Analysis.Analytic.CPolynomialDef
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {n : ℕ} {r : ENNReal} (finite : ∀ (m : ℕ), n ≤ m → p m = 0) (pos : 0 < r) (sum_eq : ∀ y ∈ Metric.eball 0 r, (∑ i ∈ Finset.range n, (p i) fun x => y) = f (x + y)) : HasFiniteFPowerSeriesOnBall f p x n r
• HasFiniteFPowerSeriesOnBall.eq_partialSum' 📋 Mathlib.Analysis.Analytic.CPolynomialDef
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {n : ℕ} (hf : HasFiniteFPowerSeriesOnBall f p x n r) (y : E) : y ∈ Metric.eball x r → ∀ (m : ℕ), n ≤ m → f y = p.partialSum m (y - x)
• HasFiniteFPowerSeriesOnBall.sum 📋 Mathlib.Analysis.Analytic.CPolynomialDef
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {n : ℕ} (h : HasFiniteFPowerSeriesOnBall f p x n r) {y : E} (hy : y ∈ Metric.eball 0 r) : f (x + y) = p.sum y
• HasFiniteFPowerSeriesOnBall.eq_partialSum 📋 Mathlib.Analysis.Analytic.CPolynomialDef
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {n : ℕ} (hf : HasFiniteFPowerSeriesOnBall f p x n r) (y : E) : y ∈ Metric.eball 0 r → ∀ (m : ℕ), n ≤ m → f (x + y) = p.partialSum m y
• hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall 📋 Mathlib.Analysis.Analytic.Within
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} : HasFPowerSeriesWithinOnBall f p s x r ↔ ∃ g, Set.EqOn f g (insert x s ∩ Metric.eball x r) ∧ HasFPowerSeriesOnBall g p x r
• HasFiniteFPowerSeriesOnBall.differentiableOn 📋 Mathlib.Analysis.Calculus.FDeriv.Analytic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {n : ℕ} {f : E → F} {x : E} (h : HasFiniteFPowerSeriesOnBall f p x n r) : DifferentiableOn 𝕜 f (Metric.eball x r)
• HasFPowerSeriesOnBall.differentiableOn 📋 Mathlib.Analysis.Calculus.FDeriv.Analytic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E} [CompleteSpace F] (h : HasFPowerSeriesOnBall f p x r) : DifferentiableOn 𝕜 f (Metric.eball x r)
• HasFPowerSeriesWithinOnBall.differentiableOn 📋 Mathlib.Analysis.Calculus.FDeriv.Analytic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E} {s : Set E} [CompleteSpace F] (h : HasFPowerSeriesWithinOnBall f p s x r) : DifferentiableOn 𝕜 f (insert x s ∩ Metric.eball x r)
• HasFPowerSeriesOnBall.hasSum_iteratedFDeriv 📋 Mathlib.Analysis.Calculus.FDeriv.Analytic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} {r : ENNReal} (h : HasFPowerSeriesOnBall f p x r) [CompleteSpace F] [CharZero 𝕜] {y : E} (hy : y ∈ Metric.eball 0 r) : HasSum (fun n => (↑n.factorial)⁻¹ • (iteratedFDeriv 𝕜 n f x) fun x => y) (f (x + y))
• NormedSpace.isUnit_exp_of_mem_ball 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] [CharZero 𝕂] {x : 𝔸} (hx : x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : IsUnit (NormedSpace.exp x)
• NormedSpace.continuousOn_exp 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] [CharZero 𝕂] : ContinuousOn NormedSpace.exp (Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius)
• NormedSpace.invertibleExpOfMemBall 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] [CharZero 𝕂] {x : 𝔸} (hx : x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : Invertible (NormedSpace.exp x)
• NormedSpace.analyticAt_exp_of_mem_ball 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] [CharZero 𝕂] (x : 𝔸) (hx : x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : AnalyticAt 𝕂 NormedSpace.exp x
• NormedSpace.norm_expSeries_div_summable_of_mem_ball 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  (𝕂 : Type u_1) {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] (x : 𝔸) (hx : x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : Summable fun n => ‖x ^ n / ↑n.factorial‖
• NormedSpace.norm_expSeries_summable_of_mem_ball' 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] (x : 𝔸) (hx : x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : Summable fun n => ‖(↑n.factorial)⁻¹ • x ^ n‖
• NormedSpace.expSeries_div_summable_of_mem_ball 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  (𝕂 : Type u_1) {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (hx : x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : Summable fun n => x ^ n / ↑n.factorial
• NormedSpace.expSeries_summable_of_mem_ball' 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (hx : x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : Summable fun n => (↑n.factorial)⁻¹ • x ^ n
• NormedSpace.invOf_exp_of_mem_ball 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] [CharZero 𝕂] {x : 𝔸} (hx : x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) [Invertible (NormedSpace.exp x)] : ⅟(NormedSpace.exp x) = NormedSpace.exp (-x)
• NormedSpace.map_exp_of_mem_ball 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_2} {𝔹 : Type u_3} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedRing 𝔹] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] [Algebra 𝕂 𝔹] [CharZero 𝕂] {F : Type u_4} [FunLike F 𝔸 𝔹] [RingHomClass F 𝔸 𝔹] (f : F) (hf : Continuous ⇑f) (x : 𝔸) (hx : x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : f (NormedSpace.exp x) = NormedSpace.exp (f x)
• NormedSpace.expSeries_hasSum_exp_of_mem_ball' 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] [CharZero 𝕂] (x : 𝔸) (hx : x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : HasSum (fun n => (↑n.factorial)⁻¹ • x ^ n) (NormedSpace.exp x)
• NormedSpace.expSeries_div_hasSum_exp_of_mem_ball 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  (𝕂 : Type u_1) {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CharZero 𝕂] [CompleteSpace 𝔸] (x : 𝔸) (hx : x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : HasSum (fun n => x ^ n / ↑n.factorial) (NormedSpace.exp x)
• NormedSpace.exp_neg_of_mem_ball 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  (𝕂 : Type u_1) {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedDivisionRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CharZero 𝕂] [CompleteSpace 𝔸] {x : 𝔸} (hx : x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : NormedSpace.exp (-x) = (NormedSpace.exp x)⁻¹
• NormedSpace.exp_add_of_commute_of_mem_ball 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] [CharZero 𝕂] {x y : 𝔸} (hxy : Commute x y) (hx : x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) (hy : y ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : NormedSpace.exp (x + y) = NormedSpace.exp x * NormedSpace.exp y
• NormedSpace.norm_expSeries_summable_of_mem_ball 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] (x : 𝔸) (hx : x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : Summable fun n => ‖(NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x‖
• NormedSpace.expSeries_summable_of_mem_ball 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (hx : x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : Summable fun n => (NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x
• NormedSpace.exp_add_of_mem_ball 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedCommRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] [CharZero 𝕂] {x y : 𝔸} (hx : x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) (hy : y ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : NormedSpace.exp (x + y) = NormedSpace.exp x * NormedSpace.exp y
• NormedSpace.algebraMap_exp_comm_of_mem_ball 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CharZero 𝕂] [CompleteSpace 𝕂] (x : 𝕂) (hx : x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝕂).radius) : (algebraMap 𝕂 𝔸) (NormedSpace.exp x) = NormedSpace.exp ((algebraMap 𝕂 𝔸) x)
• NormedSpace.expSeries_hasSum_exp_of_mem_ball 📋 Mathlib.Analysis.Normed.Algebra.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] [CharZero 𝕂] (x : 𝔸) (hx : x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : HasSum (fun n => (NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x) (NormedSpace.exp x)
• hasDerivAt_exp_of_mem_ball 📋 Mathlib.Analysis.SpecialFunctions.Exponential
  {𝕂 : Type u_1} [NontriviallyNormedField 𝕂] [CompleteSpace 𝕂] [CharZero 𝕂] {x : 𝕂} (hx : x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝕂).radius) : HasDerivAt NormedSpace.exp (NormedSpace.exp x) x
• hasStrictDerivAt_exp_of_mem_ball 📋 Mathlib.Analysis.SpecialFunctions.Exponential
  {𝕂 : Type u_1} [NontriviallyNormedField 𝕂] [CompleteSpace 𝕂] [CharZero 𝕂] {x : 𝕂} (hx : x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝕂).radius) : HasStrictDerivAt NormedSpace.exp (NormedSpace.exp x) x
• hasDerivAt_exp_smul_const_of_mem_ball 📋 Mathlib.Analysis.SpecialFunctions.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_3} [NontriviallyNormedField 𝕂] [CharZero 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (t : 𝕂) (htx : t • x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : HasDerivAt (fun u => NormedSpace.exp (u • x)) (NormedSpace.exp (t • x) * x) t
• hasDerivAt_exp_smul_const_of_mem_ball' 📋 Mathlib.Analysis.SpecialFunctions.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_3} [NontriviallyNormedField 𝕂] [CharZero 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (t : 𝕂) (htx : t • x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : HasDerivAt (fun u => NormedSpace.exp (u • x)) (x * NormedSpace.exp (t • x)) t
• hasStrictDerivAt_exp_smul_const_of_mem_ball 📋 Mathlib.Analysis.SpecialFunctions.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_3} [NontriviallyNormedField 𝕂] [CharZero 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (t : 𝕂) (htx : t • x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : HasStrictDerivAt (fun u => NormedSpace.exp (u • x)) (NormedSpace.exp (t • x) * x) t
• hasStrictDerivAt_exp_smul_const_of_mem_ball' 📋 Mathlib.Analysis.SpecialFunctions.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_3} [NontriviallyNormedField 𝕂] [CharZero 𝕂] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (t : 𝕂) (htx : t • x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : HasStrictDerivAt (fun u => NormedSpace.exp (u • x)) (x * NormedSpace.exp (t • x)) t
• hasFDerivAt_exp_smul_const_of_mem_ball' 📋 Mathlib.Analysis.SpecialFunctions.Exponential
  (𝕂 : Type u_1) {𝕊 : Type u_2} {𝔸 : Type u_3} [NontriviallyNormedField 𝕂] [CharZero 𝕂] [NormedCommRing 𝕊] [NormedRing 𝔸] [NormedSpace 𝕂 𝕊] [NormedAlgebra 𝕂 𝔸] [Algebra 𝕊 𝔸] [ContinuousSMul 𝕊 𝔸] [IsScalarTower 𝕂 𝕊 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (t : 𝕊) (htx : t • x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : HasFDerivAt (fun u => NormedSpace.exp (u • x)) ((ContinuousLinearMap.smulRight 1 x).smulRight (NormedSpace.exp (t • x))) t
• hasStrictFDerivAt_exp_smul_const_of_mem_ball' 📋 Mathlib.Analysis.SpecialFunctions.Exponential
  (𝕂 : Type u_1) {𝕊 : Type u_2} {𝔸 : Type u_3} [NontriviallyNormedField 𝕂] [CharZero 𝕂] [NormedCommRing 𝕊] [NormedRing 𝔸] [NormedSpace 𝕂 𝕊] [NormedAlgebra 𝕂 𝔸] [Algebra 𝕊 𝔸] [ContinuousSMul 𝕊 𝔸] [IsScalarTower 𝕂 𝕊 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (t : 𝕊) (htx : t • x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : HasStrictFDerivAt (fun u => NormedSpace.exp (u • x)) ((ContinuousLinearMap.smulRight 1 x).smulRight (NormedSpace.exp (t • x))) t
• hasFDerivAt_exp_of_mem_ball 📋 Mathlib.Analysis.SpecialFunctions.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedCommRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] [CharZero 𝕂] {x : 𝔸} (hx : x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : HasFDerivAt NormedSpace.exp (NormedSpace.exp x • 1) x
• hasStrictFDerivAt_exp_of_mem_ball 📋 Mathlib.Analysis.SpecialFunctions.Exponential
  {𝕂 : Type u_1} {𝔸 : Type u_2} [NontriviallyNormedField 𝕂] [NormedCommRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] [CharZero 𝕂] {x : 𝔸} (hx : x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : HasStrictFDerivAt NormedSpace.exp (NormedSpace.exp x • 1) x
• hasFDerivAt_exp_smul_const_of_mem_ball 📋 Mathlib.Analysis.SpecialFunctions.Exponential
  (𝕂 : Type u_1) {𝕊 : Type u_2} {𝔸 : Type u_3} [NontriviallyNormedField 𝕂] [CharZero 𝕂] [NormedCommRing 𝕊] [NormedRing 𝔸] [NormedSpace 𝕂 𝕊] [NormedAlgebra 𝕂 𝔸] [Algebra 𝕊 𝔸] [ContinuousSMul 𝕊 𝔸] [IsScalarTower 𝕂 𝕊 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (t : 𝕊) (htx : t • x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : HasFDerivAt (fun u => NormedSpace.exp (u • x)) (NormedSpace.exp (t • x) • ContinuousLinearMap.smulRight 1 x) t
• hasStrictFDerivAt_exp_smul_const_of_mem_ball 📋 Mathlib.Analysis.SpecialFunctions.Exponential
  (𝕂 : Type u_1) {𝕊 : Type u_2} {𝔸 : Type u_3} [NontriviallyNormedField 𝕂] [CharZero 𝕂] [NormedCommRing 𝕊] [NormedRing 𝔸] [NormedSpace 𝕂 𝕊] [NormedAlgebra 𝕂 𝔸] [Algebra 𝕊 𝔸] [ContinuousSMul 𝕊 𝔸] [IsScalarTower 𝕂 𝕊 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (t : 𝕊) (htx : t • x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius) : HasStrictFDerivAt (fun u => NormedSpace.exp (u • x)) (NormedSpace.exp (t • x) • ContinuousLinearMap.smulRight 1 x) t
• Metric.isPreconnected_eball 📋 Mathlib.Analysis.Normed.Module.Connected
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ENNReal} : IsPreconnected (Metric.eball x r)
• Metric.isConnected_eball 📋 Mathlib.Analysis.Normed.Module.Connected
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ENNReal} (hr : 0 < r) : IsConnected (Metric.eball x r)
• Metric.isPathConnected_eball 📋 Mathlib.Analysis.Normed.Module.Connected
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ENNReal} (hr : 0 < r) : IsPathConnected (Metric.eball x r)
• Metric.contractibleSpace_eball 📋 Mathlib.Analysis.Normed.Module.Connected
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ENNReal} (hr : 0 < r) : ContractibleSpace ↑(Metric.eball x r)
• AnalyticOn.hasFPowerSeriesOnSubball 📋 Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall
  {𝕜 : Type u_1} [RCLike 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜} {r : ENNReal} (hr_pos : 0 < r) (h : AnalyticOn 𝕜 f (Metric.eball x r)) : r ≤ (FormalMultilinearSeries.ofScalars 𝕜 fun n => iteratedDeriv n f x / ↑n.factorial).radius → HasFPowerSeriesOnBall f (FormalMultilinearSeries.ofScalars 𝕜 fun n => iteratedDeriv n f x / ↑n.factorial) x r
• AnalyticOn.hasFPowerSeriesOnBall 📋 Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall
  {𝕜 : Type u_1} [RCLike 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜} : 0 < (FormalMultilinearSeries.ofScalars 𝕜 fun n => iteratedDeriv n f x / ↑n.factorial).radius → AnalyticOn 𝕜 f (Metric.eball x (FormalMultilinearSeries.ofScalars 𝕜 fun n => iteratedDeriv n f x / ↑n.factorial).radius) → HasFPowerSeriesOnBall f (FormalMultilinearSeries.ofScalars 𝕜 fun n => iteratedDeriv n f x / ↑n.factorial) x (FormalMultilinearSeries.ofScalars 𝕜 fun n => iteratedDeriv n f x / ↑n.factorial).radius
• Complex.taylorSeries_eq_on_eball' 📋 Mathlib.Analysis.Complex.TaylorSeries
  ⦃c : ℂ⦄ ⦃r : ENNReal⦄ ⦃z : ℂ⦄ (hz : z ∈ Metric.eball c r) {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f (Metric.eball c r)) : ∑' (n : ℕ), (↑n.factorial)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z
• Complex.hasSum_taylorSeries_on_eball 📋 Mathlib.Analysis.Complex.TaylorSeries
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] ⦃f : ℂ → E⦄ ⦃c : ℂ⦄ ⦃r : ENNReal⦄ (hf : DifferentiableOn ℂ f (Metric.eball c r)) ⦃z : ℂ⦄ (hz : z ∈ Metric.eball c r) : HasSum (fun n => (↑n.factorial)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)
• Complex.taylorSeries_eq_on_eball 📋 Mathlib.Analysis.Complex.TaylorSeries
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] ⦃f : ℂ → E⦄ ⦃c : ℂ⦄ ⦃r : ENNReal⦄ (hf : DifferentiableOn ℂ f (Metric.eball c r)) ⦃z : ℂ⦄ (hz : z ∈ Metric.eball c r) : ∑' (n : ℕ), (↑n.factorial)⁻¹ • (z - c) ^ n • iteratedDeriv n f c = f z
• Option.some_eball 📋 Mathlib.Topology.EMetricSpace.Weak
  {α : Type u} [t : TopologicalSpace α] [m : WeakPseudoEMetricSpace α] (a : α) (r : ENNReal) : some '' Metric.eball a r = Metric.eball (some a) r
• Option.ball_infty_of_pos 📋 Mathlib.Topology.EMetricSpace.Weak
  {α : Type u} [t : TopologicalSpace α] [m : WeakPseudoEMetricSpace α] {r : ENNReal} (hr : 0 < r) : Metric.eball none r = {none}
• Metric.Snowflaking.image_toSnowflaking_eball 📋 Mathlib.Topology.MetricSpace.Snowflaking
  {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [PseudoEMetricSpace X] (x : X) (r : ENNReal) : ⇑Metric.Snowflaking.toSnowflaking '' Metric.eball x r = Metric.eball (Metric.Snowflaking.toSnowflaking x) (r ^ α)
• Metric.Snowflaking.preimage_ofSnowflaking_eball 📋 Mathlib.Topology.MetricSpace.Snowflaking
  {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [PseudoEMetricSpace X] (x : X) (r : ENNReal) : ⇑Metric.Snowflaking.ofSnowflaking ⁻¹' Metric.eball x r = Metric.eball (Metric.Snowflaking.toSnowflaking x) (r ^ α)
• Metric.Snowflaking.preimage_toSnowflaking_eball 📋 Mathlib.Topology.MetricSpace.Snowflaking
  {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [PseudoEMetricSpace X] (x : Metric.Snowflaking X α hα₀ hα₁) (d : ENNReal) : ⇑Metric.Snowflaking.toSnowflaking ⁻¹' Metric.eball x d = Metric.eball (Metric.Snowflaking.ofSnowflaking x) (d ^ α⁻¹)
• Metric.Snowflaking.image_ofSnowflaking_eball 📋 Mathlib.Topology.MetricSpace.Snowflaking
  {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [PseudoEMetricSpace X] (x : Metric.Snowflaking X α hα₀ hα₁) (d : ENNReal) : ⇑Metric.Snowflaking.ofSnowflaking '' Metric.eball x d = Metric.eball (Metric.Snowflaking.ofSnowflaking x) (d ^ α⁻¹)

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