Mathlib.Order.Filter.Germ.Basic

Filter.const_eventuallyEq' theorem

[NeBot l] {a b : β} : (∀ᶠ _ in l, a = b) ↔ a = b

Full source

theorem const_eventuallyEq' [NeBot l] {a b : β} : (∀ᶠ _ in l, a = b) ↔ a = b :=
  eventually_const

Eventual Equality of Constants in Nontrivial Filter

Informal description

For a nontrivial filter `l` (i.e., `NeBot l`) and elements `a, b : β`, the statement that `a = b` holds eventually along `l` is equivalent to `a = b` holding unconditionally. In other words, `∀ᶠ _ in l, a = b ↔ a = b`.

Filter.const_eventuallyEq theorem

[NeBot l] {a b : β} : ((fun _ => a) =ᶠ[l] fun _ => b) ↔ a = b

Full source

theorem const_eventuallyEq [NeBot l] {a b : β} : ((fun _ => a) =ᶠ[l] fun _ => b) ↔ a = b :=
  @const_eventuallyEq' _ _ _ _ a b

Eventual Equality of Constant Functions in Nontrivial Filter

Informal description

For a nontrivial filter `l` (i.e., `NeBot l`) and elements `a, b : β`, the constant functions `fun _ => a` and `fun _ => b` are eventually equal along `l` if and only if `a = b`.

Filter.germSetoid definition

(l : Filter α) (β : Type*) : Setoid (α → β)

Full source

/-- Setoid used to define the space of germs. -/
def germSetoid (l : Filter α) (β : Type*) : Setoid (α → β) where
  r := EventuallyEq l
  iseqv := ⟨EventuallyEq.refl _, EventuallyEq.symm, EventuallyEq.trans⟩

Setoid of eventually equal functions along a filter

Informal description

The setoid structure on the type of functions `α → β` where two functions are equivalent if they are eventually equal along the filter `l`. That is, for functions `f, g : α → β`, the equivalence relation is defined by `f ≈ g` if there exists a set in the filter `l` where `f` and `g` agree everywhere on that set.

Filter.Germ definition

(l : Filter α) (β : Type*) : Type _

Full source

/-- The space of germs of functions `α → β` at a filter `l`. -/
def Germ (l : Filter α) (β : Type*) : Type _ :=
  Quotient (germSetoid l β)

Space of germs of functions at a filter

Informal description

The type `Filter.Germ l β` represents the space of germs of functions `f : α → β` at a filter `l : Filter α`. A germ is an equivalence class of functions under the relation of being eventually equal along the filter `l`, meaning two functions are equivalent if they agree on some set in the filter `l`.

Filter.productSetoid definition

(l : Filter α) (ε : α → Type*) : Setoid ((a : _) → ε a)

Full source

/-- Setoid used to define the filter product. This is a dependent version of
  `Filter.germSetoid`. -/
def productSetoid (l : Filter α) (ε : α → Type*) : Setoid ((a : _) → ε a) where
  r f g := ∀ᶠ a in l, f a = g a
  iseqv :=
    ⟨fun _ => Eventually.of_forall fun _ => rfl, fun h => h.mono fun _ => Eq.symm,
      fun h1 h2 => h1.congr (h2.mono fun _ hx => hx ▸ Iff.rfl)⟩

Filter product setoid

Informal description

The setoid (equivalence relation) used to define the filter product. For a filter `l` on a type `α` and a family of types `ε : α → Type*`, two dependent functions `f g : (a : α) → ε a` are considered equivalent if they are eventually equal along the filter `l`, i.e., `∀ᶠ a in l, f a = g a`. The relation is reflexive, symmetric, and transitive, making it a valid equivalence relation.

Filter.Product definition

(l : Filter α) (ε : α → Type*) : Type _

Full source

/-- The filter product `(a : α) → ε a` at a filter `l`. This is a dependent version of
  `Filter.Germ`. -/
def Product (l : Filter α) (ε : α → Type*) : Type _ :=
  Quotient (productSetoid l ε)

Filter product of dependent functions

Informal description

The filter product `(a : α) → ε a` at a filter `l` is the quotient of the space of dependent functions `(a : α) → ε a` by the equivalence relation of being eventually equal along the filter `l`. This generalizes the non-dependent version `Filter.Germ` to dependent functions.

Filter.Product.coeTC instance

: CoeTC ((a : _) → ε a) (l.Product ε)

Full source

instance coeTC : CoeTC ((a : _) → ε a) (l.Product ε) :=
  ⟨@Quotient.mk' _ (productSetoid _ ε)⟩

Canonical Coercion to Filter Product Space

Informal description

For any filter $l$ on a type $\alpha$ and any family of types $\varepsilon : \alpha \to \text{Type}^*$, there is a canonical coercion from the space of dependent functions $(a : \alpha) \to \varepsilon a$ to the filter product $l.\text{Product} \varepsilon$, which is the quotient space under the equivalence relation of being eventually equal along $l$.

Filter.Product.instInhabited instance

[(a : _) → Inhabited (ε a)] : Inhabited (l.Product ε)

Full source

instance instInhabited [(a : _) → Inhabited (ε a)] : Inhabited (l.Product ε) :=
  ⟨(↑fun a => (default : ε a) : l.Product ε)⟩

Inhabitedness of Filter Product Space

Informal description

For any filter $l$ on a type $\alpha$ and any family of types $\varepsilon : \alpha \to \text{Type}^*$, if each $\varepsilon a$ is inhabited, then the filter product space $l.\text{Product} \varepsilon$ is also inhabited.

Filter.Germ.ofFun definition

: (α → β) → (Germ l β)

Full source

@[coe]
def ofFun : (α → β) → (Germ l β) := @Quotient.mk' _ (germSetoid _ _)

Germ of a function at a filter

Informal description

The function `Filter.Germ.ofFun` maps a function `f : α → β` to its germ at the filter `l`, which is the equivalence class of `f` under the relation of being eventually equal along `l`. That is, two functions are in the same germ if they agree on some set in the filter `l`.

Filter.Germ.instCoeTCForall instance

: CoeTC (α → β) (Germ l β)

Full source

instance : CoeTC (α → β) (Germ l β) :=
  ⟨ofFun⟩

Canonical Coercion from Functions to Germs

Informal description

For any type $\alpha$ and filter $l$ on $\alpha$, there is a canonical coercion from the type of functions $\alpha \to \beta$ to the space of germs $\text{Germ}\, l\,\beta$. This coercion maps a function $f : \alpha \to \beta$ to its germ at the filter $l$, which is the equivalence class of $f$ under the relation of being eventually equal along $l$.

Filter.Germ.const definition

{l : Filter α} (b : β) : (Germ l β)

Full source

@[coe] -- Porting note: removed `HasLiftT` instance
def const {l : Filter α} (b : β) : (Germ l β) := ofFun fun _ => b

Germ of a constant function at a filter

Informal description

For a filter $ l $ on a type $ \alpha $ and an element $ b $ of type $ \beta $, the term `Filter.Germ.const l b` represents the germ of the constant function $ \fun x \mapsto b $ at the filter $ l $. This germ is the equivalence class of all functions that are eventually equal to the constant function $ \fun x \mapsto b $ along $ l $.

Filter.Germ.coeTC instance

: CoeTC β (Germ l β)

Full source

instance coeTC : CoeTC β (Germ l β) :=
  ⟨const⟩

Canonical Map from Elements to Constant Germs

Informal description

For any type $\beta$ and filter $l$ on a type $\alpha$, there is a canonical map from $\beta$ to the space of germs $\text{Germ}\, l\,\beta$ that sends each element $b \in \beta$ to the germ of the constant function $\fun x \mapsto b$ at the filter $l$.

Filter.Germ.IsConstant definition

{l : Filter α} (P : Germ l β) : Prop

Full source

/-- A germ `P` of functions `α → β` is constant w.r.t. `l`. -/
def IsConstant {l : Filter α} (P : Germ l β) : Prop :=
  P.liftOn (fun f ↦ ∃ b : β, f =ᶠ[l] (fun _ ↦ b)) <| by
    suffices ∀ f g : α → β, ∀ b : β, f =ᶠ[l] g → (f =ᶠ[l] fun _ ↦ b) → (g =ᶠ[l] fun _ ↦ b) from
      fun f g h ↦ propext ⟨fun ⟨b, hb⟩ ↦ ⟨b, this f g b h hb⟩, fun ⟨b, hb⟩ ↦ ⟨b, h.trans hb⟩⟩
    exact fun f g b hfg hf ↦ (hfg.symm).trans hf

Constant germ of functions at a filter

Informal description

A germ $ P $ of functions $ \alpha \to \beta $ at a filter $ l $ is called *constant* if there exists a constant function $ \fun x \mapsto b $ for some $ b \in \beta $ such that $ P $ is equivalent to the germ of this constant function under the equivalence relation of being eventually equal along $ l $. In other words, $ P $ is constant if there exists $ b \in \beta $ such that for any representative $ f $ of $ P $, $ f(x) = b $ for all $ x $ in some set belonging to the filter $ l $.

Filter.Germ.isConstant_coe theorem

{l : Filter α} {b} (h : ∀ x', f x' = b) : (↑f : Germ l β).IsConstant

Full source

theorem isConstant_coe {l : Filter α} {b} (h : ∀ x', f x' = b) : (↑f : Germ l β).IsConstant :=
  ⟨b, Eventually.of_forall h⟩

Germ of a Constant Function is Constant

Informal description

For any filter $l$ on a type $\alpha$ and any function $f : \alpha \to \beta$ that is constant (i.e., $f(x) = b$ for all $x \in \alpha$ and some $b \in \beta$), the germ of $f$ at $l$ is constant.

Filter.Germ.isConstant_coe_const theorem

{l : Filter α} {b : β} : (fun _ : α ↦ b : Germ l β).IsConstant

Full source

@[simp]
theorem isConstant_coe_const {l : Filter α} {b : β} : (fun _ : α ↦ b : Germ l β).IsConstant := by
  use b

Germ of a Constant Function is Constant

Informal description

For any filter $l$ on a type $\alpha$ and any element $b \in \beta$, the germ at $l$ of the constant function $f(x) = b$ is constant.

Filter.Germ.isConstant_comp theorem

{l : Filter α} {f : α → β} {g : β → γ} (h : (f : Germ l β).IsConstant) : ((g ∘ f) : Germ l γ).IsConstant

Full source

/-- If `f : α → β` is constant w.r.t. `l` and `g : β → γ`, then `g ∘ f : α → γ` also is. -/
lemma isConstant_comp {l : Filter α} {f : α → β} {g : β → γ}
    (h : (f : Germ l β).IsConstant) : ((g ∘ f) : Germ l γ).IsConstant := by
  obtain ⟨b, hb⟩ := h
  exact ⟨g b, hb.fun_comp g⟩

Composition Preserves Constant Germs

Informal description

Let $l$ be a filter on a type $\alpha$, and let $f : \alpha \to \beta$ and $g : \beta \to \gamma$ be functions. If the germ of $f$ at $l$ is constant, then the germ of the composition $g \circ f$ at $l$ is also constant.

Filter.Germ.quot_mk_eq_coe theorem

(l : Filter α) (f : α → β) : Quot.mk _ f = (f : Germ l β)

Full source

@[simp]
theorem quot_mk_eq_coe (l : Filter α) (f : α → β) : Quot.mk _ f = (f : Germ l β) :=
  rfl

Equivalence of Quotient Construction and Germ Coercion

Informal description

For any filter $l$ on a type $\alpha$ and any function $f : \alpha \to \beta$, the equivalence class of $f$ under the relation of being eventually equal along $l$ (constructed via `Quot.mk`) is equal to the germ of $f$ at $l$ (denoted by the coercion $(f : \text{Germ}_l \beta)$).

Filter.Germ.mk'_eq_coe theorem

(l : Filter α) (f : α → β) : @Quotient.mk' _ (germSetoid _ _) f = (f : Germ l β)

Full source

@[simp]
theorem mk'_eq_coe (l : Filter α) (f : α → β) :
    @Quotient.mk' _ (germSetoid _ _) f = (f : Germ l β) :=
  rfl

Equivalence of Quotient Construction and Germ Coercion

Informal description

For any filter $l$ on a type $\alpha$ and any function $f : \alpha \to \beta$, the equivalence class of $f$ under the relation of being eventually equal along $l$ (denoted by $\text{Quotient.mk'}$) is equal to the germ of $f$ at $l$ (denoted by $(f : \text{Germ}_l \beta)$).

Filter.Germ.inductionOn theorem

(f : Germ l β) {p : Germ l β → Prop} (h : ∀ f : α → β, p f) : p f

Full source

@[elab_as_elim]
theorem inductionOn (f : Germ l β) {p : Germ l β → Prop} (h : ∀ f : α → β, p f) : p f :=
  Quotient.inductionOn' f h

Induction Principle for Germs of Functions at a Filter

Informal description

Let $f$ be a germ of functions from $\alpha$ to $\beta$ at a filter $l$ on $\alpha$. To prove a property $p$ holds for $f$, it suffices to show that $p$ holds for every function $g : \alpha \to \beta$ when considered as a germ in $\text{Germ}_l \beta$.

Filter.Germ.inductionOn₂ theorem

 (f : Germ l β) (g : Germ l γ) {p : Germ l β → Germ l γ → Prop} (h : ∀ (f : α → β) (g : α → γ), p f g) : p f g

Full source

@[elab_as_elim]
theorem inductionOn₂ (f : Germ l β) (g : Germ l γ) {p : Germ l β → Germ l γ → Prop}
    (h : ∀ (f : α → β) (g : α → γ), p f g) : p f g :=
  Quotient.inductionOn₂' f g h

Double Induction Principle for Germs of Functions at a Filter

Informal description

Let $f$ and $g$ be germs of functions from $\alpha$ to $\beta$ and $\alpha$ to $\gamma$ respectively, at a filter $l$ on $\alpha$. To prove a property $p(f, g)$ holds for these germs, it suffices to show that $p$ holds for all pairs of functions $(f_0 : \alpha \to \beta, g_0 : \alpha \to \gamma)$ when considered as germs in $\text{Germ}_l \beta$ and $\text{Germ}_l \gamma$.

Filter.Germ.inductionOn₃ theorem

 (f : Germ l β) (g : Germ l γ) (h : Germ l δ) {p : Germ l β → Germ l γ → Germ l δ → Prop}
  (H : ∀ (f : α → β) (g : α → γ) (h : α → δ), p f g h) : p f g h

Full source

@[elab_as_elim]
theorem inductionOn₃ (f : Germ l β) (g : Germ l γ) (h : Germ l δ)
    {p : Germ l β → Germ l γ → Germ l δ → Prop}
    (H : ∀ (f : α → β) (g : α → γ) (h : α → δ), p f g h) : p f g h :=
  Quotient.inductionOn₃' f g h H

Triple Induction Principle for Germs of Functions at a Filter

Informal description

Let $f$, $g$, and $h$ be germs of functions from $\alpha$ to $\beta$, $\gamma$, and $\delta$ respectively, at a filter $l$ on $\alpha$. To prove a property $p(f, g, h)$ holds for these germs, it suffices to show that $p$ holds for all triples of functions $(f_0 : \alpha \to \beta, g_0 : \alpha \to \gamma, h_0 : \alpha \to \delta)$ when considered as germs in $\text{Germ}_l \beta$, $\text{Germ}_l \gamma$, and $\text{Germ}_l \delta$.

Filter.Germ.map' definition

 {lc : Filter γ} (F : (α → β) → γ → δ) (hF : (l.EventuallyEq ⇒ lc.EventuallyEq) F F) : Germ l β → Germ lc δ

Full source

/-- Given a map `F : (α → β) → (γ → δ)` that sends functions eventually equal at `l` to functions
eventually equal at `lc`, returns a map from `Germ l β` to `Germ lc δ`. -/
def map' {lc : Filter γ} (F : (α → β) → γ → δ) (hF : (l.EventuallyEq ⇒ lc.EventuallyEq) F F) :
    Germ l β → Germ lc δ :=
  Quotient.map' F hF

Lifting a function to germs of functions respecting eventual equality

Informal description

Given a map $ F : (\alpha \to \beta) \to (\gamma \to \delta) $ that sends functions eventually equal at a filter $ l $ to functions eventually equal at another filter $ lc $, the function `Filter.Germ.map'` lifts $ F $ to a map from the space of germs $ \text{Germ } l \beta $ to the space of germs $ \text{Germ } lc \delta $. Specifically, if two functions $ f, g : \alpha \to \beta $ are eventually equal along $ l $, then $ F f $ and $ F g $ are eventually equal along $ lc $, and this induces a well-defined map on the corresponding germs.

Filter.Germ.liftOn definition

{γ : Sort*} (f : Germ l β) (F : (α → β) → γ) (hF : (l.EventuallyEq ⇒ (· = ·)) F F) : γ

Full source

/-- Given a germ `f : Germ l β` and a function `F : (α → β) → γ` sending eventually equal functions
to the same value, returns the value `F` takes on functions having germ `f` at `l`. -/
def liftOn {γ : Sort*} (f : Germ l β) (F : (α → β) → γ) (hF : (l.EventuallyEq ⇒ (· = ·)) F F) :
    γ :=
  Quotient.liftOn' f F hF

Lifting a function to operate on germs of functions

Informal description

Given a germ `f : Germ l β` and a function `F : (α → β) → γ` that respects the equivalence relation of being eventually equal along the filter `l` (i.e., `F` yields the same output for functions that are eventually equal along `l`), the function `liftOn` lifts `F` to operate on the germ `f`, producing a value in `γ`. This is done by applying `F` to any representative function of the germ `f`, with the guarantee that the result is independent of the choice of representative due to `hF`.

Filter.Germ.map'_coe theorem

 {lc : Filter γ} (F : (α → β) → γ → δ) (hF : (l.EventuallyEq ⇒ lc.EventuallyEq) F F) (f : α → β) : map' F hF f = F f

Full source

@[simp]
theorem map'_coe {lc : Filter γ} (F : (α → β) → γ → δ) (hF : (l.EventuallyEq ⇒ lc.EventuallyEq) F F)
    (f : α → β) : map' F hF f = F f :=
  rfl

Commutativity of Germ Lifting with Function Application

Informal description

For any filters `l` on `α` and `lc` on `γ`, a function `F : (α → β) → (γ → δ)` that respects eventual equality (i.e., if two functions are eventually equal along `l`, then their images under `F` are eventually equal along `lc`), and a function `f : α → β`, the germ of `F f` at `lc` is equal to the image under `map'` of the germ of `f` at `l`. In other words, the diagram commutes when lifting `F` to germs.

Filter.Germ.coe_eq theorem

: (f : Germ l β) = g ↔ f =ᶠ[l] g

Full source

@[simp, norm_cast]
theorem coe_eq : (f : Germ l β) = g ↔ f =ᶠ[l] g :=
  Quotient.eq''

Equality of Germs via Eventual Equality

Informal description

Two germs $f$ and $g$ in $\text{Germ}_l(\beta)$ are equal if and only if their representatives are eventually equal along the filter $l$, i.e., $f = g \leftrightarrow \forall^l x, f(x) = g(x)$.

Filter.Germ.map definition

(op : β → γ) : Germ l β → Germ l γ

Full source

/-- Lift a function `β → γ` to a function `Germ l β → Germ l γ`. -/
def map (op : β → γ) : Germ l β → Germ l γ :=
  map' (op ∘ ·) fun _ _ H => H.mono fun _ H => congr_arg op H

Lifting a function to germs of functions

Informal description

Given a function $ \text{op} : \beta \to \gamma $, the function `Filter.Germ.map` lifts $ \text{op} $ to a function between spaces of germs, sending a germ $ f $ in $ \text{Germ}_l(\beta) $ to the germ of the composition $ \text{op} \circ f $ in $ \text{Germ}_l(\gamma) $. This operation is well-defined because if two functions $ f $ and $ g $ are eventually equal along the filter $ l $, then their compositions $ \text{op} \circ f $ and $ \text{op} \circ g $ are also eventually equal along $ l $.

Filter.Germ.map_coe theorem

(op : β → γ) (f : α → β) : map op (f : Germ l β) = op ∘ f

Full source

@[simp]
theorem map_coe (op : β → γ) (f : α → β) : map op (f : Germ l β) = op ∘ f :=
  rfl

Lifted Map on Germs Equals Composition of Functions

Informal description

For any function $F \colon \beta \to \gamma$ and any function $f \colon \alpha \to \beta$, the germ of the composition $F \circ f$ at filter $l$ is equal to the result of applying the lifted map operation to the germ of $f$ at $l$, i.e., \[ \text{map } F (f) = F \circ f. \]

Filter.Germ.map_id theorem

: map id = (id : Germ l β → Germ l β)

Full source

@[simp]
theorem map_id : map id = (id : Germ l β → Germ l β) := by
  ext ⟨f⟩
  rfl

Identity Map on Germs is Identity Function

Informal description

The map operation applied to the identity function on germs is equal to the identity function on germs, i.e., $\text{map id} = \text{id}$ as functions from $\text{Germ}_l(\beta)$ to itself.

Filter.Germ.map_map theorem

(op₁ : γ → δ) (op₂ : β → γ) (f : Germ l β) : map op₁ (map op₂ f) = map (op₁ ∘ op₂) f

Full source

theorem map_map (op₁ : γ → δ) (op₂ : β → γ) (f : Germ l β) :
    map op₁ (map op₂ f) = map (op₁ ∘ op₂) f :=
  inductionOn f fun _ => rfl

Composition of Lifted Maps on Germs

Informal description

For any functions $F \colon \gamma \to \delta$ and $G \colon \beta \to \gamma$, and any germ $f \in \text{Germ}_l(\beta)$, the composition of the lifted maps satisfies: \[ \text{map } F (\text{map } G f) = \text{map } (F \circ G) f. \]

Filter.Germ.map₂ definition

(op : β → γ → δ) : Germ l β → Germ l γ → Germ l δ

Full source

/-- Lift a binary function `β → γ → δ` to a function `Germ l β → Germ l γ → Germ l δ`. -/
def map₂ (op : β → γ → δ) : Germ l β → Germ l γ → Germ l δ :=
  Quotient.map₂ (fun f g x => op (f x) (g x)) fun f f' Hf g g' Hg =>
    Hg.mp <| Hf.mono fun x Hf Hg => by simp only [Hf, Hg]

Lifting a binary operation to germs of functions at a filter

Informal description

Given a binary function $F : \beta \to \gamma \to \delta$, the function `Filter.Germ.map₂` lifts $F$ to a binary operation on the space of germs $\text{Germ } l \beta \to \text{Germ } l \gamma \to \text{Germ } l \delta$. Specifically, for germs $f$ and $g$, the result is the germ of the function $x \mapsto F (f x) (g x)$ at the filter $l$.

Filter.Germ.map₂_coe theorem

(op : β → γ → δ) (f : α → β) (g : α → γ) : map₂ op (f : Germ l β) g = fun x => op (f x) (g x)

Full source

@[simp]
theorem map₂_coe (op : β → γ → δ) (f : α → β) (g : α → γ) :
    map₂ op (f : Germ l β) g = fun x => op (f x) (g x) :=
  rfl

Lifted Binary Operation on Germs Equals Pointwise Operation

Informal description

Given a binary operation $F : \beta \to \gamma \to \delta$ and functions $f : \alpha \to \beta$, $g : \alpha \to \gamma$, the germ of the function $x \mapsto F(f(x), g(x))$ at the filter $l$ is equal to the application of the lifted operation $\text{map}_2 F$ to the germs of $f$ and $g$ at $l$. In other words, $\text{map}_2 F (f, g) = \lambda x, F(f(x), g(x))$ as germs in $\text{Germ}_l \delta$.

Filter.Germ.Tendsto definition

(f : Germ l β) (lb : Filter β) : Prop

Full source

/-- A germ at `l` of maps from `α` to `β` tends to `lb : Filter β` if it is represented by a map
which tends to `lb` along `l`. -/
protected def Tendsto (f : Germ l β) (lb : Filter β) : Prop :=
  liftOn f (fun f => Tendsto f l lb) fun _f _g H => propext (tendsto_congr' H)

Convergence of a germ at a filter

Informal description

A germ $ f $ at a filter $ l $ of functions from $ \alpha $ to $ \beta $ tends to a filter $ lb $ on $ \beta $ if there exists a representative function $ g $ of $ f $ such that $ g $ tends to $ lb $ along $ l $. In other words, $ f $ tends to $ lb $ if for some (equivalently, any) representative $ g $ of $ f $, the limit of $ g $ along $ l $ is in $ lb $.

Filter.Germ.coe_tendsto theorem

{f : α → β} {lb : Filter β} : (f : Germ l β).Tendsto lb ↔ Tendsto f l lb

Full source

@[simp, norm_cast]
theorem coe_tendsto {f : α → β} {lb : Filter β} : (f : Germ l β).Tendsto lb ↔ Tendsto f l lb :=
  Iff.rfl

Equivalence of Germ Tendency and Function Tendency at a Filter

Informal description

For a function $f \colon \alpha \to \beta$ and a filter $lb$ on $\beta$, the germ of $f$ at a filter $l$ tends to $lb$ if and only if the function $f$ tends to $lb$ along the filter $l$. In other words, $(f : \text{Germ}_l \beta).\text{Tendsto} \, lb \leftrightarrow \text{Tendsto} \, f \, l \, lb$.

Filter.Germ.compTendsto' definition

(f : Germ l β) {lc : Filter γ} (g : Germ lc α) (hg : g.Tendsto l) : Germ lc β

Full source

/-- Given two germs `f : Germ l β`, and `g : Germ lc α`, where `l : Filter α`, if `g` tends to `l`,
then the composition `f ∘ g` is well-defined as a germ at `lc`. -/
def compTendsto' (f : Germ l β) {lc : Filter γ} (g : Germ lc α) (hg : g.Tendsto l) : Germ lc β :=
  liftOn f (fun f => g.map f) fun _f₁ _f₂ hF =>
    inductionOn g (fun _g hg => coe_eq.2 <| hg.eventually hF) hg

Composition of a germ with a germ tending to a filter

Informal description

Given a germ $ f $ of functions from $ \alpha $ to $ \beta $ at a filter $ l $, and a germ $ g $ of functions from $ \gamma $ to $ \alpha $ at a filter $ lc $, if $ g $ tends to $ l $ (i.e., its representatives tend to $ l $ along $ lc $), then the composition $ f \circ g $ is well-defined as a germ at $ lc $. This is constructed by lifting the map operation to the germ $ f $ and applying it to $ g $, ensuring the result is independent of the choice of representatives.

Filter.Germ.coe_compTendsto' theorem

(f : α → β) {lc : Filter γ} {g : Germ lc α} (hg : g.Tendsto l) : (f : Germ l β).compTendsto' g hg = g.map f

Full source

@[simp]
theorem coe_compTendsto' (f : α → β) {lc : Filter γ} {g : Germ lc α} (hg : g.Tendsto l) :
    (f : Germ l β).compTendsto' g hg = g.map f :=
  rfl

Composition of Germ with Tendsto Germ Equals Mapping

Informal description

For any function $f \colon \alpha \to \beta$, any filter $lc$ on $\gamma$, and any germ $g$ of functions from $\gamma$ to $\alpha$ at $lc$ that tends to $l$, the composition of the germ of $f$ at $l$ with $g$ is equal to the germ obtained by mapping $f$ over $g$. In symbols: $(f : \text{Germ}_l \beta).\text{compTendsto}' \, g \, hg = g.\text{map} \, f$.

Filter.Germ.compTendsto definition

(f : Germ l β) {lc : Filter γ} (g : γ → α) (hg : Tendsto g lc l) : Germ lc β

Full source

/-- Given a germ `f : Germ l β` and a function `g : γ → α`, where `l : Filter α`, if `g` tends
to `l` along `lc : Filter γ`, then the composition `f ∘ g` is well-defined as a germ at `lc`. -/
def compTendsto (f : Germ l β) {lc : Filter γ} (g : γ → α) (hg : Tendsto g lc l) : Germ lc β :=
  f.compTendsto' _ hg.germ_tendsto

Composition of a germ with a function tending to a filter

Informal description

Given a germ $ f $ of functions from $ \alpha $ to $ \beta $ at a filter $ l $, and a function $ g : \gamma \to \alpha $, if $ g $ tends to $ l $ along a filter $ lc $ on $ \gamma $, then the composition $ f \circ g $ is well-defined as a germ at $ lc $. This is constructed by first converting $ g $ to a germ at $ lc $ and then using the composition operation for germs.

Filter.Germ.coe_compTendsto theorem

(f : α → β) {lc : Filter γ} {g : γ → α} (hg : Tendsto g lc l) : (f : Germ l β).compTendsto g hg = f ∘ g

Full source

@[simp]
theorem coe_compTendsto (f : α → β) {lc : Filter γ} {g : γ → α} (hg : Tendsto g lc l) :
    (f : Germ l β).compTendsto g hg = f ∘ g :=
  rfl

Germ Composition with Tendsto Function Equals Pointwise Composition

Informal description

For any function $f \colon \alpha \to \beta$, any filter $lc$ on $\gamma$, and any function $g \colon \gamma \to \alpha$ that tends to $l$ along $lc$, the composition of the germ of $f$ at $l$ with $g$ is equal to the germ of the pointwise composition $f \circ g$ at $lc$. In symbols: $(f : \text{Germ}_l \beta).\text{compTendsto} \, g \, hg = (f \circ g : \text{Germ}_{lc} \beta)$.

Filter.Germ.compTendsto'_coe theorem

 (f : Germ l β) {lc : Filter γ} {g : γ → α} (hg : Tendsto g lc l) :
  f.compTendsto' _ hg.germ_tendsto = f.compTendsto g hg

Full source

@[simp, nolint simpNF]
theorem compTendsto'_coe (f : Germ l β) {lc : Filter γ} {g : γ → α} (hg : Tendsto g lc l) :
    f.compTendsto' _ hg.germ_tendsto = f.compTendsto g hg :=
  rfl

Equality of Germ Compositions via `compTendsto'` and `compTendsto`

Informal description

Let $f$ be a germ of functions from $\alpha$ to $\beta$ at a filter $l$, and let $g \colon \gamma \to \alpha$ be a function that tends to $l$ along a filter $lc$ on $\gamma$. Then the composition of $f$ with the germ of $g$ at $lc$ (via `compTendsto'`) is equal to the composition of $f$ with $g$ (via `compTendsto`). In symbols: $f.\text{compTendsto}' \, \overline{g} \, hg.\text{germ\_tendsto} = f.\text{compTendsto} \, g \, hg$, where $\overline{g}$ denotes the germ of $g$ at $lc$.

Filter.Germ.Filter.Tendsto.congr_germ theorem

 {f g : β → γ} {l : Filter α} {l' : Filter β} (h : f =ᶠ[l'] g) {φ : α → β} (hφ : Tendsto φ l l') :
  (f ∘ φ : Germ l γ) = g ∘ φ

Full source

theorem Filter.Tendsto.congr_germ {f g : β → γ} {l : Filter α} {l' : Filter β} (h : f =ᶠ[l'] g)
    {φ : α → β} (hφ : Tendsto φ l l') : (f ∘ φ : Germ l γ) = g ∘ φ :=
  EventuallyEq.germ_eq (h.comp_tendsto hφ)

Germ Equality under Composition with Tendsto Function

Informal description

Let $f, g : \beta \to \gamma$ be functions, $l$ a filter on $\alpha$, and $l'$ a filter on $\beta$. If $f$ and $g$ are eventually equal along $l'$ (i.e., $f =_{l'} g$), and $\varphi : \alpha \to \beta$ is a function such that $\varphi$ tends to $l'$ along $l$, then the germs of $f \circ \varphi$ and $g \circ \varphi$ at $l$ are equal.

Filter.Germ.isConstant_comp_tendsto theorem

 {lc : Filter γ} {g : γ → α} (hf : (f : Germ l β).IsConstant) (hg : Tendsto g lc l) : IsConstant (f ∘ g : Germ lc β)

Full source

lemma isConstant_comp_tendsto {lc : Filter γ} {g : γ → α}
    (hf : (f : Germ l β).IsConstant) (hg : Tendsto g lc l) : IsConstant (f ∘ g : Germ lc β) := by
  rcases hf with ⟨b, hb⟩
  exact ⟨b, hb.comp_tendsto hg⟩

Composition with a Tendsto Function Preserves Constant Germs

Informal description

Let $l$ be a filter on a type $\alpha$, and let $f$ be a germ of functions $\alpha \to \beta$ at $l$. If $f$ is constant (i.e., represented by a constant function on some set in $l$), then for any filter $l_c$ on a type $\gamma$ and any function $g : \gamma \to \alpha$ such that $g$ tends to $l$ along $l_c$, the composition germ $f \circ g$ at $l_c$ is also constant.

Filter.Germ.isConstant_compTendsto theorem

 {f : Germ l β} {lc : Filter γ} {g : γ → α} (hf : f.IsConstant) (hg : Tendsto g lc l) : (f.compTendsto g hg).IsConstant

Full source

/-- If a germ `f : Germ l β` is constant, where `l : Filter α`,
and a function `g : γ → α` tends to `l` along `lc : Filter γ`,
the germ of the composition `f ∘ g` is also constant. -/
lemma isConstant_compTendsto {f : Germ l β} {lc : Filter γ} {g : γ → α}
    (hf : f.IsConstant) (hg : Tendsto g lc l) : (f.compTendsto g hg).IsConstant := by
  induction f using Quotient.inductionOn with | _ f => ?_
  exact isConstant_comp_tendsto hf hg

Composition with a Tendsto Function Preserves Constant Germs

Informal description

Let $l$ be a filter on a type $\alpha$, and let $f$ be a germ of functions $\alpha \to \beta$ at $l$. If $f$ is constant (i.e., there exists $b \in \beta$ such that $f$ is the germ of the constant function $x \mapsto b$ at $l$), then for any filter $l_c$ on a type $\gamma$ and any function $g : \gamma \to \alpha$ such that $g$ tends to $l$ along $l_c$, the composition germ $f \circ g$ at $l_c$ is also constant.

Filter.Germ.const_inj theorem

[NeBot l] {a b : β} : (↑a : Germ l β) = ↑b ↔ a = b

Full source

@[simp, norm_cast]
theorem const_inj [NeBot l] {a b : β} : (↑a : Germ l β) = ↑b ↔ a = b :=
  coe_eq.trans const_eventuallyEq

Injectivity of Constant Germs in Nontrivial Filter

Informal description

For a nontrivial filter $l$ (i.e., $l$ does not contain the empty set) and any elements $a, b \in \beta$, the germs of the constant functions $a$ and $b$ in $\mathrm{Germ}_l(\beta)$ are equal if and only if $a = b$.

Filter.Germ.map_const theorem

(l : Filter α) (a : β) (f : β → γ) : (↑a : Germ l β).map f = ↑(f a)

Full source

@[simp]
theorem map_const (l : Filter α) (a : β) (f : β → γ) : (↑a : Germ l β).map f = ↑(f a) :=
  rfl

Mapping a Constant Germ Yields a Constant Germ: $f \circ (\text{const}_l a) = \text{const}_l (f a)$

Informal description

For any filter $l$ on a type $\alpha$, element $a \in \beta$, and function $f : \beta \to \gamma$, the germ of the constant function $a$ at $l$ mapped under $f$ is equal to the germ of the constant function $f(a)$ at $l$. In other words, the following equality holds in the space of germs: \[ f \circ (\text{const}_l a) = \text{const}_l (f a). \]

Filter.Germ.map₂_const theorem

(l : Filter α) (b : β) (c : γ) (f : β → γ → δ) : map₂ f (↑b : Germ l β) ↑c = ↑(f b c)

Full source

@[simp]
theorem map₂_const (l : Filter α) (b : β) (c : γ) (f : β → γ → δ) :
    map₂ f (↑b : Germ l β) ↑c = ↑(f b c) :=
  rfl

Lifted Binary Operation on Constant Germs Yields Constant Germ

Informal description

For any filter $l$ on a type $\alpha$, elements $b \in \beta$ and $c \in \gamma$, and a binary function $f : \beta \to \gamma \to \delta$, the germ of the constant function $x \mapsto f(b, c)$ at $l$ is equal to the result of applying the lifted binary operation $\mathrm{map}_2 f$ to the germs of the constant functions $b$ and $c$ at $l$. In other words, \[ \mathrm{map}_2 f \, (\mathrm{const}_l b) \, (\mathrm{const}_l c) = \mathrm{const}_l (f b c). \]

Filter.Germ.const_compTendsto theorem

 {l : Filter α} (b : β) {lc : Filter γ} {g : γ → α} (hg : Tendsto g lc l) : (↑b : Germ l β).compTendsto g hg = ↑b

Full source

@[simp]
theorem const_compTendsto {l : Filter α} (b : β) {lc : Filter γ} {g : γ → α} (hg : Tendsto g lc l) :
    (↑b : Germ l β).compTendsto g hg = ↑b :=
  rfl

Composition of Constant Germ with Function Tending to Filter Preserves Constancy

Informal description

Let $l$ be a filter on a type $\alpha$, $b$ an element of type $\beta$, $lc$ a filter on a type $\gamma$, and $g : \gamma \to \alpha$ a function such that $g$ tends to $l$ along $lc$. Then the composition of the constant germ $\uparrow b$ (the germ of the constant function $x \mapsto b$) with $g$ is equal to the constant germ $\uparrow b$ at $lc$. In other words, $(\text{const}_l b) \circ g = \text{const}_{lc} b$.

Filter.Germ.const_compTendsto' theorem

 {l : Filter α} (b : β) {lc : Filter γ} {g : Germ lc α} (hg : g.Tendsto l) : (↑b : Germ l β).compTendsto' g hg = ↑b

Full source

@[simp]
theorem const_compTendsto' {l : Filter α} (b : β) {lc : Filter γ} {g : Germ lc α}
    (hg : g.Tendsto l) : (↑b : Germ l β).compTendsto' g hg = ↑b :=
  inductionOn g (fun _ _ => rfl) hg

Composition of Constant Germ with Germ Tending to Filter Preserves Constancy

Informal description

Let $l$ be a filter on a type $\alpha$, $b$ an element of type $\beta$, $lc$ a filter on a type $\gamma$, and $g$ a germ of functions from $\gamma$ to $\alpha$ at $lc$ such that $g$ tends to $l$. Then the composition of the constant germ $\uparrow b$ (the germ of the constant function $x \mapsto b$) with $g$ is equal to the constant germ $\uparrow b$ at $lc$.

Filter.Germ.LiftPred definition

(p : β → Prop) (f : Germ l β) : Prop

Full source

/-- Lift a predicate on `β` to `Germ l β`. -/
def LiftPred (p : β → Prop) (f : Germ l β) : Prop :=
  liftOn f (fun f => ∀ᶠ x in l, p (f x)) fun _f _g H =>
    propext <| eventually_congr <| H.mono fun _x hx => hx ▸ Iff.rfl

Lifting a predicate to germs of functions

Informal description

Given a predicate `p : β → Prop` and a germ `f : Germ l β`, the predicate `LiftPred p f` holds if and only if for some (equivalently, any) representative function `f'` of the germ `f`, the predicate `p (f' x)` holds for all `x` in some set belonging to the filter `l`. In other words, `p` holds for the values of `f` eventually along the filter `l`.

Filter.Germ.liftPred_coe theorem

{p : β → Prop} {f : α → β} : LiftPred p (f : Germ l β) ↔ ∀ᶠ x in l, p (f x)

Full source

@[simp]
theorem liftPred_coe {p : β → Prop} {f : α → β} : LiftPredLiftPred p (f : Germ l β) ↔ ∀ᶠ x in l, p (f x) :=
  Iff.rfl

Characterization of Lifted Predicate on Function Germs

Informal description

For any predicate $p : \beta \to \text{Prop}$ and any function $f : \alpha \to \beta$, the lifted predicate $\text{LiftPred}\, p$ holds for the germ of $f$ at filter $l$ if and only if $p(f(x))$ holds for all $x$ in some set belonging to $l$.

Filter.Germ.liftPred_const theorem

{p : β → Prop} {x : β} (hx : p x) : LiftPred p (↑x : Germ l β)

Full source

theorem liftPred_const {p : β → Prop} {x : β} (hx : p x) : LiftPred p (↑x : Germ l β) :=
  Eventually.of_forall fun _y => hx

Lifted Predicate Holds for Germ of Constant Function

Informal description

For any predicate $p : \beta \to \text{Prop}$ and any element $x \in \beta$ satisfying $p(x)$, the germ of the constant function $x$ at a filter $l$ satisfies the lifted predicate $\text{LiftPred}\, p$.

Filter.Germ.liftPred_const_iff theorem

[NeBot l] {p : β → Prop} {x : β} : LiftPred p (↑x : Germ l β) ↔ p x

Full source

@[simp]
theorem liftPred_const_iff [NeBot l] {p : β → Prop} {x : β} : LiftPredLiftPred p (↑x : Germ l β) ↔ p x :=
  @eventually_const _ _ _ (p x)

Characterization of Lifted Predicate on Constant Germs for Nontrivial Filters

Informal description

For a nontrivial filter $l$ (i.e., $l$ is not the bottom filter), a predicate $p : \beta \to \text{Prop}$, and an element $x \in \beta$, the lifted predicate $\text{LiftPred}\, p$ holds for the germ of the constant function $x$ at $l$ if and only if $p(x)$ holds.

Filter.Germ.LiftRel definition

(r : β → γ → Prop) (f : Germ l β) (g : Germ l γ) : Prop

Full source

/-- Lift a relation `r : β → γ → Prop` to `Germ l β → Germ l γ → Prop`. -/
def LiftRel (r : β → γ → Prop) (f : Germ l β) (g : Germ l γ) : Prop :=
  Quotient.liftOn₂' f g (fun f g => ∀ᶠ x in l, r (f x) (g x)) fun _f _g _f' _g' Hf Hg =>
    propext <| eventually_congr <| Hg.mp <| Hf.mono fun _x hf hg => hf ▸ hg ▸ Iff.rfl

Lifting a relation to germs of functions at a filter

Informal description

Given a relation $ r : \beta \to \gamma \to \text{Prop} $, the function `LiftRel` lifts $ r $ to a relation on germs of functions at a filter $ l $. Specifically, for germs $ f : \text{Germ}\, l\, \beta $ and $ g : \text{Germ}\, l\, \gamma $, the relation $ \text{LiftRel}\, r\, f\, g $ holds if and only if there exists a set in the filter $ l $ on which the representatives of $ f $ and $ g $ are related by $ r $ pointwise. More formally, if $ f $ and $ g $ are equivalence classes of functions under the relation of being eventually equal along $ l $, then $ \text{LiftRel}\, r\, f\, g $ means that for any representatives $ f' $ of $ f $ and $ g' $ of $ g $, the relation $ r(f'(x), g'(x)) $ holds for all $ x $ in some set belonging to the filter $ l $.

Filter.Germ.liftRel_coe theorem

{r : β → γ → Prop} {f : α → β} {g : α → γ} : LiftRel r (f : Germ l β) g ↔ ∀ᶠ x in l, r (f x) (g x)

Full source

@[simp]
theorem liftRel_coe {r : β → γ → Prop} {f : α → β} {g : α → γ} :
    LiftRelLiftRel r (f : Germ l β) g ↔ ∀ᶠ x in l, r (f x) (g x) :=
  Iff.rfl

Characterization of Lifted Relation on Function Germs via Eventual Equality

Informal description

For any relation $r : \beta \to \gamma \to \text{Prop}$ and functions $f : \alpha \to \beta$, $g : \alpha \to \gamma$, the lifted relation $\text{LiftRel}\, r$ holds between the germ of $f$ at filter $l$ and the germ of $g$ if and only if $r(f(x), g(x))$ holds for all $x$ in some set belonging to the filter $l$. In other words, $\text{LiftRel}\, r\, [f]\, [g] \leftrightarrow \forall^l x, r(f(x), g(x))$, where $[f]$ denotes the germ of $f$ at $l$.

Filter.Germ.liftRel_const theorem

{r : β → γ → Prop} {x : β} {y : γ} (h : r x y) : LiftRel r (↑x : Germ l β) ↑y

Full source

theorem liftRel_const {r : β → γ → Prop} {x : β} {y : γ} (h : r x y) :
    LiftRel r (↑x : Germ l β) ↑y :=
  Eventually.of_forall fun _ => h

Lifted Relation Holds for Constant Germs When Base Relation Holds

Informal description

For any relation $r : \beta \to \gamma \to \text{Prop}$ and elements $x \in \beta$, $y \in \gamma$ such that $r(x, y)$ holds, the lifted relation $\text{LiftRel}\, r$ holds between the germs of the constant functions $x$ and $y$ at the filter $l$. That is, if $r(x, y)$ is true, then $\text{LiftRel}\, r\, [x]\, [y]$ holds, where $[x]$ and $[y]$ denote the germs of the constant functions $x$ and $y$ at $l$ respectively.

Filter.Germ.liftRel_const_iff theorem

[NeBot l] {r : β → γ → Prop} {x : β} {y : γ} : LiftRel r (↑x : Germ l β) ↑y ↔ r x y

Full source

@[simp]
theorem liftRel_const_iff [NeBot l] {r : β → γ → Prop} {x : β} {y : γ} :
    LiftRelLiftRel r (↑x : Germ l β) ↑y ↔ r x y :=
  @eventually_const _ _ _ (r x y)

Lifted Relation on Constant Germs Characterization: $\text{LiftRel}\, r\, [x]\, [y] \leftrightarrow r(x, y)$ for Nontrivial Filter

Informal description

For a nontrivial filter $l$ (i.e., $l$ is not the bottom filter), a relation $r : \beta \to \gamma \to \text{Prop}$, and elements $x \in \beta$, $y \in \gamma$, the lifted relation $\text{LiftRel}\, r$ holds between the germs of the constant functions $x$ and $y$ at $l$ if and only if $r(x, y)$ holds.

Filter.Germ.instInhabited instance

[Inhabited β] : Inhabited (Germ l β)

Full source

instance instInhabited [Inhabited β] : Inhabited (Germ l β) := ⟨↑(default : β)⟩

Inhabitedness of Germ Space for Inhabited Types

Informal description

For any inhabited type $\beta$ and any filter $l$ on a type $\alpha$, the space of germs $\text{Germ } l \beta$ is also inhabited. Specifically, the germ of any constant function from $\alpha$ to $\beta$ at $l$ serves as an inhabitant of $\text{Germ } l \beta$.

Filter.Germ.instMul instance

[Mul M] : Mul (Germ l M)

Full source

@[to_additive] instance instMul [Mul M] : Mul (Germ l M) := ⟨map₂ (· * ·)⟩

Multiplication on Germs of Functions

Informal description

For any type $M$ with a multiplication operation, the space of germs $\text{Germ } l M$ inherits a multiplication operation defined pointwise. That is, for two germs $f$ and $g$ in $\text{Germ } l M$, their product is the germ of the function $x \mapsto f(x) * g(x)$ at the filter $l$.

Filter.Germ.coe_mul theorem

[Mul M] (f g : α → M) : ↑(f * g) = (f * g : Germ l M)

Full source

@[to_additive (attr := simp, norm_cast)]
theorem coe_mul [Mul M] (f g : α → M) : ↑(f * g) = (f * g : Germ l M) :=
  rfl

Germ of Product Equals Product of Germs

Informal description

For any type $M$ with a multiplication operation and any functions $f, g : \alpha \to M$, the germ of the pointwise product function $f * g$ at the filter $l$ is equal to the product of the germs of $f$ and $g$ in $\text{Germ } l M$. That is, $\overline{f * g} = \overline{f} * \overline{g}$, where $\overline{f}$ denotes the germ of $f$ at $l$.

Filter.Germ.instOne instance

[One M] : One (Germ l M)

Full source

@[to_additive] instance instOne [One M] : One (Germ l M) := ⟨↑(1 : M)⟩

Germ of the Constant One Function

Informal description

For any type $M$ with a distinguished element $1$, the space of germs $\text{Germ}_l M$ at a filter $l$ has a distinguished element given by the germ of the constant function $x \mapsto 1$.

Filter.Germ.coe_one theorem

[One M] : ↑(1 : α → M) = (1 : Germ l M)

Full source

@[to_additive (attr := simp, norm_cast)]
theorem coe_one [One M] : ↑(1 : α → M) = (1 : Germ l M) :=
  rfl

Germ of Constant One Function Equals Identity in Germ Space

Informal description

For any type $M$ with a multiplicative identity element $1$, the germ at filter $l$ of the constant function $x \mapsto 1$ is equal to the multiplicative identity in the space of germs $\text{Germ}_l M$.

Filter.Germ.instSemigroup instance

[Semigroup M] : Semigroup (Germ l M)

Full source

@[to_additive]
instance instSemigroup [Semigroup M] : Semigroup (Germ l M) :=
  { mul_assoc := fun a b c => Quotient.inductionOn₃' a b c
      fun _ _ _ => congrArg ofFun <| mul_assoc .. }

Semigroup Structure on Germs of Functions

Informal description

For any semigroup $M$, the space of germs $\text{Germ}_l M$ at a filter $l$ inherits a semigroup structure, where the multiplication operation is defined pointwise. That is, for two germs $f$ and $g$ in $\text{Germ}_l M$, their product is the germ of the function $x \mapsto f(x) \cdot g(x)$ at the filter $l$, and this operation is associative.

Filter.Germ.instCommSemigroup instance

[CommSemigroup M] : CommSemigroup (Germ l M)

Full source

@[to_additive]
instance instCommSemigroup [CommSemigroup M] : CommSemigroup (Germ l M) :=
  { mul_comm := Quotient.ind₂' fun _ _ => congrArg ofFun <| mul_comm .. }

Commutative Semigroup Structure on Germs of Functions

Informal description

For any commutative semigroup $M$, the space of germs $\text{Germ}_l M$ at a filter $l$ inherits a commutative semigroup structure, where the multiplication operation is defined pointwise. That is, for two germs $f$ and $g$ in $\text{Germ}_l M$, their product is the germ of the function $x \mapsto f(x) \cdot g(x)$ at the filter $l$, and this operation is associative and commutative.

Filter.Germ.instIsLeftCancelMul instance

[Mul M] [IsLeftCancelMul M] : IsLeftCancelMul (Germ l M)

Full source

@[to_additive]
instance instIsLeftCancelMul [Mul M] [IsLeftCancelMul M] : IsLeftCancelMul (Germ l M) where
  mul_left_cancel f₁ f₂ f₃ :=
    inductionOn₃ f₁ f₂ f₃ fun _f₁ _f₂ _f₃ H =>
      coe_eq.2 ((coe_eq.1 H).mono fun _x => mul_left_cancel)

Left-Cancellative Multiplication on Germs of Functions

Informal description

For any type $M$ with a left-cancellative multiplication operation, the space of germs $\text{Germ}_l M$ at a filter $l$ also inherits a left-cancellative multiplication operation. That is, if $M$ satisfies $a \cdot b = a \cdot c \implies b = c$ for all $a, b, c \in M$, then for any germs $f, g, h \in \text{Germ}_l M$, the equality $f \cdot g = f \cdot h$ implies $g = h$.

Filter.Germ.instIsRightCancelMul instance

[Mul M] [IsRightCancelMul M] : IsRightCancelMul (Germ l M)

Full source

@[to_additive]
instance instIsRightCancelMul [Mul M] [IsRightCancelMul M] : IsRightCancelMul (Germ l M) where
  mul_right_cancel f₁ f₂ f₃ :=
    inductionOn₃ f₁ f₂ f₃ fun _f₁ _f₂ _f₃ H =>
      coe_eq.2 <| (coe_eq.1 H).mono fun _x => mul_right_cancel

Right-Cancellative Multiplication on Germs of Functions

Informal description

For any type $M$ with a right-cancellative multiplication operation, the space of germs $\text{Germ}_l M$ at a filter $l$ also inherits a right-cancellative multiplication operation. That is, if $M$ satisfies $a \cdot c = b \cdot c \implies a = b$ for all $a, b, c \in M$, then for any germs $f, g, h \in \text{Germ}_l M$, the equality $f \cdot h = g \cdot h$ implies $f = g$.

Filter.Germ.instIsCancelMul instance

[Mul M] [IsCancelMul M] : IsCancelMul (Germ l M)

Full source

@[to_additive]
instance instIsCancelMul [Mul M] [IsCancelMul M] : IsCancelMul (Germ l M) where

Cancellative Multiplication on Germs of Functions

Informal description

For any type $M$ with a cancellative multiplication operation, the space of germs $\text{Germ}_l M$ at a filter $l$ also inherits a cancellative multiplication operation. That is, if $M$ satisfies both left and right cancellation properties for multiplication, then for any germs $f, g, h \in \text{Germ}_l M$, the equalities $f \cdot g = f \cdot h$ and $g \cdot f = h \cdot f$ imply $g = h$.

Filter.Germ.instLeftCancelSemigroup instance

[LeftCancelSemigroup M] : LeftCancelSemigroup (Germ l M)

Full source

@[to_additive]
instance instLeftCancelSemigroup [LeftCancelSemigroup M] : LeftCancelSemigroup (Germ l M) where
  mul_left_cancel _ _ _ := mul_left_cancel

Left Cancellative Semigroup Structure on Germs of Functions

Informal description

For any left cancellative semigroup $M$, the space of germs $\text{Germ}_l M$ at a filter $l$ inherits a left cancellative semigroup structure, where the multiplication operation is defined pointwise. That is, for any germs $f, g, h \in \text{Germ}_l M$, if $f \cdot g = f \cdot h$, then $g = h$.

Filter.Germ.instRightCancelSemigroup instance

[RightCancelSemigroup M] : RightCancelSemigroup (Germ l M)

Full source

@[to_additive]
instance instRightCancelSemigroup [RightCancelSemigroup M] : RightCancelSemigroup (Germ l M) where
  mul_right_cancel _ _ _ := mul_right_cancel

Right-Cancellative Semigroup Structure on Germs of Functions

Informal description

For any right-cancellative semigroup $M$, the space of germs $\text{Germ}_l M$ at a filter $l$ inherits a right-cancellative semigroup structure, where the multiplication operation is defined pointwise. That is, for any germs $f, g, h \in \text{Germ}_l M$, if $f \cdot g = h \cdot g$, then $f = h$.

Filter.Germ.instMulOneClass instance

[MulOneClass M] : MulOneClass (Germ l M)

Full source

@[to_additive]
instance instMulOneClass [MulOneClass M] : MulOneClass (Germ l M) :=
  { one_mul := Quotient.ind' fun _ => congrArg ofFun <| one_mul _
    mul_one := Quotient.ind' fun _ => congrArg ofFun <| mul_one _ }

Multiplicative Structure with Identity on Germs of Functions

Informal description

For any type $M$ with a multiplicative structure with identity (i.e., a multiplication operation and a multiplicative identity element $1$ satisfying $1 \cdot a = a$ and $a \cdot 1 = a$ for all $a \in M$), the space of germs $\mathrm{Germ}_l M$ at a filter $l$ inherits a multiplicative structure with identity. The multiplication of two germs is defined pointwise, and the identity element is the germ of the constant function $x \mapsto 1$.

Filter.Germ.instSMul instance

[SMul M G] : SMul M (Germ l G)

Full source

@[to_additive]
instance instSMul [SMul M G] : SMul M (Germ l G) where smul n := map (n • ·)

Scalar Multiplication on Germs of Functions

Informal description

For any type $M$ with a scalar multiplication operation $\cdot : M \to G \to G$, the space of germs $\text{Germ}_l(G)$ inherits a scalar multiplication operation from $G$, defined by lifting the operation pointwise to germs.

Filter.Germ.instPow instance

[Pow G M] : Pow (Germ l G) M

Full source

@[to_additive existing instSMul]
instance instPow [Pow G M] : Pow (Germ l G) M where pow f n := map (· ^ n) f

Power Operation on Germs of Functions

Informal description

For any types $G$ and $M$ equipped with a power operation $\mathrm{Pow}\,G\,M$, the space of germs $\mathrm{Germ}_l(G)$ inherits a power operation from $G$, defined by lifting the operation pointwise to germs. That is, for a germ $f \in \mathrm{Germ}_l(G)$ and $n \in M$, the power $f^n$ is the germ of the function $x \mapsto (f(x))^n$.

Filter.Germ.coe_smul theorem

[SMul M G] (n : M) (f : α → G) : ↑(n • f) = n • (f : Germ l G)

Full source

@[to_additive (attr := simp, norm_cast)]
theorem coe_smul [SMul M G] (n : M) (f : α → G) : ↑(n • f) = n • (f : Germ l G) :=
  rfl

Scalar Multiplication Commutes with Germ Formation

Informal description

For any type $M$ with a scalar multiplication operation $\cdot : M \to G \to G$, any scalar $n \in M$, and any function $f : \alpha \to G$, the germ of the scalar multiple function $n \cdot f$ at the filter $l$ is equal to the scalar multiple of the germ of $f$ at $l$. In symbols, $\overline{n \cdot f} = n \cdot \overline{f}$, where $\overline{f}$ denotes the germ of $f$ at $l$.

Filter.Germ.const_smul theorem

[SMul M G] (n : M) (a : G) : (↑(n • a) : Germ l G) = n • (↑a : Germ l G)

Full source

@[to_additive (attr := simp, norm_cast)]
theorem const_smul [SMul M G] (n : M) (a : G) : (↑(n • a) : Germ l G) = n • (↑a : Germ l G) :=
  rfl

Scalar Multiplication of Constant Germs: $\overline{n \cdot a} = n \cdot \overline{a}$

Informal description

For any scalar multiplication operation $\cdot : M \to G \to G$, a scalar $n : M$, and an element $a : G$, the germ of the constant function $x \mapsto n \cdot a$ at a filter $l$ is equal to the scalar multiplication of $n$ with the germ of the constant function $x \mapsto a$ at $l$. In symbols, $\overline{n \cdot a} = n \cdot \overline{a}$, where $\overline{f}$ denotes the germ of $f$ at $l$.

Filter.Germ.coe_pow theorem

[Pow G M] (f : α → G) (n : M) : ↑(f ^ n) = (f : Germ l G) ^ n

Full source

@[to_additive (attr := simp, norm_cast)]
theorem coe_pow [Pow G M] (f : α → G) (n : M) : ↑(f ^ n) = (f : Germ l G) ^ n :=
  rfl

Power Operation on Germs: $[f^n] = [f]^n$

Informal description

For any types $G$ and $M$ equipped with a power operation, and for any function $f : \alpha \to G$ and exponent $n : M$, the germ of the function $f^n$ at the filter $l$ is equal to the $n$-th power of the germ of $f$ at $l$. In symbols, if $[f^n]$ denotes the germ of $f^n$, then $[f^n] = [f]^n$.

Filter.Germ.const_pow theorem

[Pow G M] (a : G) (n : M) : (↑(a ^ n) : Germ l G) = (↑a : Germ l G) ^ n

Full source

@[to_additive (attr := simp, norm_cast)]
theorem const_pow [Pow G M] (a : G) (n : M) : (↑(a ^ n) : Germ l G) = (↑a : Germ l G) ^ n :=
  rfl

Power of Constant Germ Equals Germ of Power

Informal description

For a type $G$ equipped with a power operation $\mathrm{Pow}\,G\,M$, a filter $l$ on a type $\alpha$, an element $a \in G$, and an exponent $n \in M$, the germ of the constant function $x \mapsto a^n$ at $l$ is equal to the $n$-th power of the germ of the constant function $x \mapsto a$ at $l$. In symbols: $$ \overline{a^n} = (\overline{a})^n $$ where $\overline{f}$ denotes the germ of a function $f$ at $l$.

Filter.Germ.instMonoid instance

[Monoid M] : Monoid (Germ l M)

Full source

@[to_additive]
instance instMonoid [Monoid M] : Monoid (Germ l M) :=
  { Function.Surjective.monoid ofFun Quot.mk_surjective (by rfl)
      (fun _ _ => by rfl) fun _ _ => by rfl with
    toSemigroup := instSemigroup
    toOne := instOne
    npow := fun n a => a ^ n }

Monoid Structure on Germs of Functions

Informal description

For any monoid $M$ and filter $l$ on a type $\alpha$, the space of germs $\mathrm{Germ}_l M$ inherits a monoid structure, where the multiplication and identity are defined pointwise from $M$. That is, the product of two germs $f$ and $g$ is the germ of the function $x \mapsto f(x) \cdot g(x)$, and the identity is the germ of the constant function $x \mapsto 1$.

Filter.Germ.coeMulHom definition

[Monoid M] (l : Filter α) : (α → M) →* Germ l M

Full source

/-- Coercion from functions to germs as a monoid homomorphism. -/
@[to_additive "Coercion from functions to germs as an additive monoid homomorphism."]
def coeMulHom [Monoid M] (l : Filter α) : (α → M) →* Germ l M where
  toFun := ofFun; map_one' := rfl; map_mul' _ _ := rfl

Monoid homomorphism from functions to germs

Informal description

The function `Filter.Germ.coeMulHom` is a monoid homomorphism from the space of functions `α → M` to the space of germs `Germ l M`, where `M` is a monoid and `l` is a filter on `α`. It maps a function `f : α → M` to its germ at the filter `l`, preserves the multiplicative identity, and satisfies `coeMulHom l (f * g) = coeMulHom l f * coeMulHom l g` for any functions `f, g : α → M`.

Filter.Germ.coe_coeMulHom theorem

[Monoid M] : (coeMulHom l : (α → M) → Germ l M) = ofFun

Full source

@[to_additive (attr := simp)]
theorem coe_coeMulHom [Monoid M] : (coeMulHom l : (α → M) → Germ l M) = ofFun :=
  rfl

Equality of Monoid Homomorphism and Germ Construction for Function Spaces

Informal description

For any monoid $M$ and filter $l$ on a type $\alpha$, the monoid homomorphism $\mathrm{coeMulHom}_l$ from the space of functions $\alpha \to M$ to the space of germs $\mathrm{Germ}_l M$ coincides with the germ construction map $\mathrm{ofFun}$. That is, $\mathrm{coeMulHom}_l = \mathrm{ofFun}$ as maps from $\alpha \to M$ to $\mathrm{Germ}_l M$.

Filter.Germ.instCommMonoid instance

[CommMonoid M] : CommMonoid (Germ l M)

Full source

@[to_additive]
instance instCommMonoid [CommMonoid M] : CommMonoid (Germ l M) :=
  { mul_comm := mul_comm }

Commutative Monoid Structure on Germs of Functions

Informal description

For any commutative monoid $M$ and any filter $l$ on a type $\alpha$, the space of germs $\mathrm{Germ}_l M$ inherits a commutative monoid structure, where the multiplication and identity are defined pointwise from $M$. That is, the product of two germs $f$ and $g$ is the germ of the function $x \mapsto f(x) \cdot g(x)$, and the identity is the germ of the constant function $x \mapsto 1$.

Filter.Germ.instNatCast instance

[NatCast M] : NatCast (Germ l M)

Full source

instance instNatCast [NatCast M] : NatCast (Germ l M) where natCast n := (n : α → M)

Natural Number Casting on Germs

Informal description

For any type $M$ with a natural number casting operation and any filter $l$ on a type $\alpha$, the space of germs $\text{Germ}\, l\, M$ inherits a natural number casting operation where the germ of the constant function with value $n$ is identified with $n$ itself.

Filter.Germ.natCast_def theorem

[NatCast M] (n : ℕ) : ((fun _ ↦ n : α → M) : Germ l M) = n

Full source

@[simp]
theorem natCast_def [NatCast M] (n : ℕ) : ((fun _ ↦ n : α → M) : Germ l M) = n := rfl

Germ of Constant Function Equals Its Value

Informal description

For any type $M$ with a natural number casting operation and any natural number $n$, the germ at filter $l$ of the constant function $\lambda \_ \mapsto n$ (from $\alpha$ to $M$) is equal to $n$ in the space of germs $\text{Germ}\, l\, M$.

Filter.Germ.const_nat theorem

[NatCast M] (n : ℕ) : ((n : M) : Germ l M) = n

Full source

@[simp, norm_cast]
theorem const_nat [NatCast M] (n : ℕ) : ((n : M) : Germ l M) = n := rfl

Germ of Constant Natural Number Equals Its Value

Informal description

For any type $M$ with a natural number casting operation and any natural number $n$, the germ at filter $l$ of the constant function with value $n$ (viewed as an element of $M$) is equal to $n$ in the space of germs $\text{Germ}\, l\, M$.

Filter.Germ.coe_ofNat theorem

[NatCast M] (n : ℕ) [n.AtLeastTwo] : ((ofNat(n) : α → M) : Germ l M) = OfNat.ofNat n

Full source

@[simp, norm_cast]
theorem coe_ofNat [NatCast M] (n : ℕ) [n.AtLeastTwo] :
    ((ofNat(n) : α → M) : Germ l M) = OfNat.ofNat n :=
  rfl

Germ of Constant Function Equals Canonical Element for Numerals ≥ 2

Informal description

For any type $M$ with a natural number casting operation, any natural number $n \geq 2$, and any filter $l$ on a type $\alpha$, the germ at $l$ of the constant function $\lambda x \mapsto n$ (from $\alpha$ to $M$) is equal to the canonical element $n$ in the space of germs $\text{Germ}\, l\, M$.

Filter.Germ.const_ofNat theorem

[NatCast M] (n : ℕ) [n.AtLeastTwo] : ((ofNat(n) : M) : Germ l M) = OfNat.ofNat n

Full source

@[simp, norm_cast]
theorem const_ofNat [NatCast M] (n : ℕ) [n.AtLeastTwo] :
    ((ofNat(n) : M) : Germ l M) = OfNat.ofNat n :=
  rfl

Germ of Constant Function Equals Canonical Element for Numerals ≥ 2

Informal description

For any type $M$ with a natural number casting operation, any natural number $n \geq 2$, and any filter $l$ on a type $\alpha$, the germ of the constant function $\lambda x \mapsto n$ (from $\alpha$ to $M$) at $l$ is equal to the canonical element $n$ in the space of germs $\text{Germ}\, l\, M$.

Filter.Germ.instIntCast instance

[IntCast M] : IntCast (Germ l M)

Full source

instance instIntCast [IntCast M] : IntCast (Germ l M) where intCast n := (n : α → M)

Integer Casting on Germs

Informal description

For any type $M$ with an integer casting operation and any filter $l$ on a type $\alpha$, the space of germs $\text{Germ}\, l\, M$ inherits an integer casting operation from $M$.

Filter.Germ.intCast_def theorem

[IntCast M] (n : ℤ) : ((fun _ ↦ n : α → M) : Germ l M) = n

Full source

@[simp]
theorem intCast_def [IntCast M] (n : ℤ) : ((fun _ ↦ n : α → M) : Germ l M) = n := rfl

Germ of Constant Integer Function Equals Integer Itself

Informal description

For any type $M$ with an integer casting operation and any filter $l$ on a type $\alpha$, the germ of the constant function $\lambda \_ \mapsto n$ (where $n$ is an integer) in $\text{Germ}\, l\, M$ is equal to $n$ itself. In other words, the germ of the constant function with value $n$ is identified with the integer $n$ in the space of germs.

Filter.Germ.instAddMonoidWithOne instance

[AddMonoidWithOne M] : AddMonoidWithOne (Germ l M)

Full source

instance instAddMonoidWithOne [AddMonoidWithOne M] : AddMonoidWithOne (Germ l M) where
  natCast_zero := congrArg ofFun <| by simp; rfl
  natCast_succ _ := congrArg ofFun <| by simp [Function.comp]; rfl

Additive Monoid with One Structure on Germs

Informal description

For any additive monoid with one $M$ and any filter $l$ on a type $\alpha$, the space of germs $\text{Germ}_l M$ inherits an additive monoid with one structure from $M$. This means that $\text{Germ}_l M$ has a distinguished element $1$, an addition operation, and a canonical homomorphism from the natural numbers, all defined pointwise on representatives.

Filter.Germ.instAddCommMonoidWithOne instance

[AddCommMonoidWithOne M] : AddCommMonoidWithOne (Germ l M)

Full source

instance instAddCommMonoidWithOne [AddCommMonoidWithOne M] : AddCommMonoidWithOne (Germ l M) :=
  { add_comm := add_comm }

Additive Commutative Monoid with One Structure on Germs

Informal description

For any additive commutative monoid with one $M$ and any filter $l$ on a type $\alpha$, the space of germs $\text{Germ}_l M$ inherits an additive commutative monoid with one structure from $M$. This means that $\text{Germ}_l M$ has a distinguished element $1$, an addition operation that is commutative, and a canonical homomorphism from the natural numbers, all defined pointwise on representatives.

Filter.Germ.instInv instance

[Inv G] : Inv (Germ l G)

Full source

@[to_additive] instance instInv [Inv G] : Inv (Germ l G) := ⟨map Inv.inv⟩

Inversion Operation on Germs of Functions

Informal description

For any type $G$ with an inversion operation and any filter $l$ on a type $\alpha$, the space of germs $\text{Germ}_l G$ inherits an inversion operation from $G$. Specifically, if $[G]$ has an inversion operation, then the inversion of a germ $f \in \text{Germ}_l G$ is defined as the germ of the pointwise inversion of any representative function of $f$.

Filter.Germ.coe_inv theorem

[Inv G] (f : α → G) : ↑f⁻¹ = (f⁻¹ : Germ l G)

Full source

@[to_additive (attr := simp, norm_cast)]
theorem coe_inv [Inv G] (f : α → G) : ↑f⁻¹ = (f⁻¹ : Germ l G) :=
  rfl

Germ of Inverse Equals Inverse of Germ

Informal description

For any type $G$ with an inversion operation and any function $f : \alpha \to G$, the germ of the pointwise inverse function $f^{-1}$ at a filter $l$ is equal to the inverse of the germ of $f$ at $l$, i.e., $\overline{f^{-1}} = (\overline{f})^{-1}$ in $\text{Germ}_l G$.

Filter.Germ.const_inv theorem

[Inv G] (a : G) : (↑(a⁻¹) : Germ l G) = (↑a)⁻¹

Full source

@[to_additive (attr := simp, norm_cast)]
theorem const_inv [Inv G] (a : G) : (↑(a⁻¹) : Germ l G) = (↑a)⁻¹ :=
  rfl

Inversion of Constant Germ Equals Germ of Inverted Constant

Informal description

For any type $G$ with an inversion operation and any element $a \in G$, the germ of the constant function $x \mapsto a^{-1}$ at a filter $l$ is equal to the inversion of the germ of the constant function $x \mapsto a$ at $l$. In other words, $\overline{a^{-1}} = (\overline{a})^{-1}$ in the space of germs $\text{Germ}_l G$.

Filter.Germ.instDiv instance

[Div M] : Div (Germ l M)

Full source

@[to_additive] instance instDiv [Div M] : Div (Germ l M) := ⟨map₂ (· / ·)⟩

Division Operation on Germs of Functions at a Filter

Informal description

For any type $M$ equipped with a division operation and any filter $l$ on a type $\alpha$, the space of germs $\text{Germ } l M$ inherits a division operation. Specifically, for two germs $f$ and $g$ in $\text{Germ } l M$, their division $f / g$ is defined as the germ of the function $x \mapsto f(x) / g(x)$ at the filter $l$.

Filter.Germ.coe_div theorem

[Div M] (f g : α → M) : ↑(f / g) = (f / g : Germ l M)

Full source

@[to_additive (attr := simp, norm_cast)]
theorem coe_div [Div M] (f g : α → M) : ↑(f / g) = (f / g : Germ l M) :=
  rfl

Germ of Pointwise Division Equals Division of Germs

Informal description

For any type $M$ with a division operation and any functions $f, g : \alpha \to M$, the germ of the pointwise division function $f / g$ at a filter $l$ is equal to the division of the germs of $f$ and $g$ in $\text{Germ } l M$. That is, $\overline{f / g} = \overline{f} / \overline{g}$ where $\overline{\cdot}$ denotes the germ construction.

Filter.Germ.const_div theorem

[Div M] (a b : M) : (↑(a / b) : Germ l M) = ↑a / ↑b

Full source

@[to_additive (attr := simp, norm_cast)]
theorem const_div [Div M] (a b : M) : (↑(a / b) : Germ l M) = ↑a / ↑b :=
  rfl

Germ of Constant Division Equals Division of Constant Germs

Informal description

For any type $M$ with a division operation and any elements $a, b \in M$, the germ of the constant function $x \mapsto a / b$ at a filter $l$ is equal to the division of the germs of the constant functions $x \mapsto a$ and $x \mapsto b$ in the space of germs $\text{Germ } l M$. That is, $\overline{a / b} = \overline{a} / \overline{b}$ where $\overline{\cdot}$ denotes the germ construction.

Filter.Germ.instInvolutiveInv instance

[InvolutiveInv G] : InvolutiveInv (Germ l G)

Full source

@[to_additive]
instance instInvolutiveInv [InvolutiveInv G] : InvolutiveInv (Germ l G) :=
  { inv_inv := Quotient.ind' fun _ => congrArg ofFun<| inv_inv _ }

Involutive Inversion on Germs of Functions

Informal description

For any type $G$ with an involutive inversion operation and any filter $l$ on a type $\alpha$, the space of germs $\mathrm{Germ}_l G$ inherits an involutive inversion operation from $G$. That is, for any germ $f \in \mathrm{Germ}_l G$, we have $(f^{-1})^{-1} = f$.

Filter.Germ.instHasDistribNeg instance

[Mul G] [HasDistribNeg G] : HasDistribNeg (Germ l G)

Full source

instance instHasDistribNeg [Mul G] [HasDistribNeg G] : HasDistribNeg (Germ l G) :=
  { neg_mul := Quotient.ind₂' fun _ _ => congrArg ofFun <| neg_mul ..
    mul_neg := Quotient.ind₂' fun _ _ => congrArg ofFun <| mul_neg .. }

Negation Distributes over Multiplication in Germs of Functions

Informal description

For any type $G$ with a multiplication operation and a negation operation that distributes over multiplication, the space of germs $\mathrm{Germ}_l G$ at a filter $l$ inherits a negation operation that distributes over multiplication. That is, for any germs $f$ and $g$ in $\mathrm{Germ}_l G$, we have $-(f * g) = (-f) * g = f * (-g)$.

Filter.Germ.instInvOneClass instance

[InvOneClass G] : InvOneClass (Germ l G)

Full source

@[to_additive]
instance instInvOneClass [InvOneClass G] : InvOneClass (Germ l G) :=
  ⟨congr_arg ofFun inv_one⟩

Inverse of One is One in Germs of Functions

Informal description

For any type $G$ with an inversion operation and a multiplicative identity element satisfying $1^{-1} = 1$, the space of germs $\text{Germ}_l G$ at a filter $l$ also satisfies $1^{-1} = 1$.

Filter.Germ.instDivInvMonoid instance

[DivInvMonoid G] : DivInvMonoid (Germ l G)

Full source

@[to_additive subNegMonoid]
instance instDivInvMonoid [DivInvMonoid G] : DivInvMonoid (Germ l G) where
  zpow z f := f ^ z
  zpow_zero' := Quotient.ind' fun _ => congrArg ofFun <|
    funext fun _ => DivInvMonoid.zpow_zero' _
  zpow_succ' _ := Quotient.ind' fun _ => congrArg ofFun <|
    funext fun _ => DivInvMonoid.zpow_succ' ..
  zpow_neg' _ := Quotient.ind' fun _ => congrArg ofFun <|
    funext fun _ => DivInvMonoid.zpow_neg' ..
  div_eq_mul_inv := Quotient.ind₂' fun _ _ ↦ congrArg ofFun <| div_eq_mul_inv ..

Division-Inversion Monoid Structure on Germs of Functions

Informal description

For any type $G$ equipped with a division-inversion monoid structure and any filter $l$ on a type $\alpha$, the space of germs $\mathrm{Germ}_l G$ inherits a division-inversion monoid structure. Specifically, the division and inversion operations on germs are defined pointwise from those on $G$, and the integer power operation is lifted accordingly.

Filter.Germ.instDivisionMonoid instance

[DivisionMonoid G] : DivisionMonoid (Germ l G)

Full source

@[to_additive]
instance instDivisionMonoid [DivisionMonoid G] : DivisionMonoid (Germ l G) where
  inv_inv := inv_inv
  mul_inv_rev x y := inductionOn₂ x y fun _ _ ↦ congr_arg ofFun <| mul_inv_rev _ _
  inv_eq_of_mul x y := inductionOn₂ x y fun _ _ h ↦ coe_eq.2 <| (coe_eq.1 h).mono fun _ ↦
    DivisionMonoid.inv_eq_of_mul _ _

Division Monoid Structure on Germs of Functions

Informal description

For any division monoid $G$ and any filter $l$ on a type $\alpha$, the space of germs $\mathrm{Germ}_l G$ inherits a division monoid structure. The division and inversion operations on germs are defined pointwise from those on $G$, and the integer power operation is lifted accordingly.

Filter.Germ.instGroup instance

[Group G] : Group (Germ l G)

Full source

@[to_additive]
instance instGroup [Group G] : Group (Germ l G) :=
  { inv_mul_cancel := Quotient.ind' fun _ => congrArg ofFun <| inv_mul_cancel _ }

Group Structure on Germs of Functions

Informal description

For any group $G$ and any filter $l$ on a type $\alpha$, the space of germs $\mathrm{Germ}_l G$ inherits a group structure. The multiplication, inversion, and division operations on germs are defined pointwise from those on $G$.

Filter.Germ.instCommGroup instance

[CommGroup G] : CommGroup (Germ l G)

Full source

@[to_additive]
instance instCommGroup [CommGroup G] : CommGroup (Germ l G) :=
  { mul_comm := mul_comm }

Commutative Group Structure on Germs of Functions

Informal description

For any commutative group $G$ and any filter $l$ on a type $\alpha$, the space of germs $\mathrm{Germ}_l G$ inherits a commutative group structure. The multiplication, inversion, and division operations on germs are defined pointwise from those on $G$, and the commutativity of the operation is preserved.

Filter.Germ.instAddGroupWithOne instance

[AddGroupWithOne G] : AddGroupWithOne (Germ l G)

Full source

instance instAddGroupWithOne [AddGroupWithOne G] : AddGroupWithOne (Germ l G) where
  __ := instAddMonoidWithOne
  __ := instAddGroup
  intCast_ofNat _ := congrArg ofFun <| by simp
  intCast_negSucc _ := congrArg ofFun <| by simp [Function.comp_def]; rfl

Additive Group with One Structure on Germs

Informal description

For any additive group with one $G$ and any filter $l$ on a type $\alpha$, the space of germs $\mathrm{Germ}_l G$ inherits an additive group with one structure from $G$. This includes a zero element, addition, negation, and a canonical homomorphism from the integers, all defined pointwise on representatives.

Filter.Germ.instNontrivial instance

[Nontrivial R] [NeBot l] : Nontrivial (Germ l R)

Full source

instance instNontrivial [Nontrivial R] [NeBot l] : Nontrivial (Germ l R) :=
  let ⟨x, y, h⟩ := exists_pair_ne R
  ⟨⟨↑x, ↑y, mt const_inj.1 h⟩⟩

Nontriviality of Germs at a Nontrivial Filter

Informal description

For any nontrivial type $R$ and any nontrivial filter $l$ on a type $\alpha$, the space of germs $\mathrm{Germ}_l(R)$ is also nontrivial.

Filter.Germ.instMulZeroClass instance

[MulZeroClass R] : MulZeroClass (Germ l R)

Full source

instance instMulZeroClass [MulZeroClass R] : MulZeroClass (Germ l R) :=
  { zero_mul := Quotient.ind' fun _ => congrArg ofFun <| zero_mul _
    mul_zero := Quotient.ind' fun _ => congrArg ofFun <| mul_zero _ }

MulZeroClass Structure on Germs of Functions

Informal description

For any type $R$ with a multiplication operation and a zero element satisfying the properties of a `MulZeroClass`, the space of germs $\text{Germ } l R$ inherits a `MulZeroClass` structure. This means that the multiplication operation on germs is defined pointwise and satisfies the properties of a `MulZeroClass`, including $0 * f = 0$ and $f * 0 = 0$ for any germ $f$.

Filter.Germ.instMulZeroOneClass instance

[MulZeroOneClass R] : MulZeroOneClass (Germ l R)

Full source

instance instMulZeroOneClass [MulZeroOneClass R] : MulZeroOneClass (Germ l R) where
  __ := instMulZeroClass
  __ := instMulOneClass

MulZeroOneClass Structure on Germs of Functions

Informal description

For any type $R$ with a multiplicative structure that includes a zero element and a multiplicative identity (i.e., a `MulZeroOneClass`), the space of germs $\mathrm{Germ}_l R$ at a filter $l$ inherits a `MulZeroOneClass` structure. This means that the multiplication of germs is defined pointwise, with the zero germ acting as an absorbing element and the germ of the constant function $x \mapsto 1$ acting as the multiplicative identity.

Filter.Germ.instMonoidWithZero instance

[MonoidWithZero R] : MonoidWithZero (Germ l R)

Full source

instance instMonoidWithZero [MonoidWithZero R] : MonoidWithZero (Germ l R) where
  __ := instMonoid
  __ := instMulZeroClass

Monoid with Zero Structure on Germs of Functions

Informal description

For any monoid with zero $R$ and filter $l$ on a type $\alpha$, the space of germs $\mathrm{Germ}_l R$ inherits a monoid with zero structure, where the multiplication, identity, and zero are defined pointwise from $R$.

Filter.Germ.instDistrib instance

[Distrib R] : Distrib (Germ l R)

Full source

instance instDistrib [Distrib R] : Distrib (Germ l R) where
  left_distrib a b c := Quotient.inductionOn₃' a b c fun _ _ _ ↦ congrArg ofFun <| left_distrib ..
  right_distrib a b c := Quotient.inductionOn₃' a b c fun _ _ _ ↦ congrArg ofFun <| right_distrib ..

Distributive Structure on Germs of Functions

Informal description

For any type $R$ with a distributive structure (i.e., equipped with addition and multiplication operations satisfying left and right distributivity), the space of germs $\text{Germ } l R$ inherits a distributive structure, where addition and multiplication are defined pointwise.

Filter.Germ.instNonUnitalNonAssocSemiring instance

[NonUnitalNonAssocSemiring R] : NonUnitalNonAssocSemiring (Germ l R)

Full source

instance instNonUnitalNonAssocSemiring [NonUnitalNonAssocSemiring R] :
    NonUnitalNonAssocSemiring (Germ l R) where
  __ := instAddCommMonoid
  __ := instDistrib
  __ := instMulZeroClass

Non-Unital Non-Associative Semiring Structure on Germs

Informal description

For any type $R$ with a non-unital non-associative semiring structure, the space of germs $\mathrm{Germ}_l R$ inherits a non-unital non-associative semiring structure, where addition and multiplication are defined pointwise.

Filter.Germ.instNonUnitalSemiring instance

[NonUnitalSemiring R] : NonUnitalSemiring (Germ l R)

Full source

instance instNonUnitalSemiring [NonUnitalSemiring R] : NonUnitalSemiring (Germ l R) :=
  { mul_assoc := mul_assoc }

Non-Unital Semiring Structure on Germs of Functions

Informal description

For any non-unital semiring $R$, the space of germs $\mathrm{Germ}_l R$ inherits a non-unital semiring structure, where addition and multiplication are defined pointwise.

Filter.Germ.instNonAssocSemiring instance

[NonAssocSemiring R] : NonAssocSemiring (Germ l R)

Full source

instance instNonAssocSemiring [NonAssocSemiring R] : NonAssocSemiring (Germ l R) where
  __ := instNonUnitalNonAssocSemiring
  __ := instMulZeroOneClass
  __ := instAddMonoidWithOne

Non-Associative Semiring Structure on Germs of Functions

Informal description

For any non-associative semiring $R$ and any filter $l$ on a type $\alpha$, the space of germs $\mathrm{Germ}_l R$ inherits a non-associative semiring structure, where addition and multiplication are defined pointwise.

Filter.Germ.instNonUnitalNonAssocRing instance

[NonUnitalNonAssocRing R] : NonUnitalNonAssocRing (Germ l R)

Full source

instance instNonUnitalNonAssocRing [NonUnitalNonAssocRing R] :
    NonUnitalNonAssocRing (Germ l R) where
  __ := instAddCommGroup
  __ := instNonUnitalNonAssocSemiring

Non-Unital Non-Associative Ring Structure on Germs of Functions

Informal description

For any non-unital non-associative ring $R$, the space of germs $\mathrm{Germ}_l R$ inherits a non-unital non-associative ring structure, where addition and multiplication are defined pointwise.

Filter.Germ.instNonUnitalRing instance

[NonUnitalRing R] : NonUnitalRing (Germ l R)

Full source

instance instNonUnitalRing [NonUnitalRing R] : NonUnitalRing (Germ l R) :=
  { mul_assoc := mul_assoc }

Non-Unital Ring Structure on Germs of Functions

Informal description

For any non-unital ring $R$ and any filter $l$ on a type $\alpha$, the space of germs $\mathrm{Germ}_l R$ inherits a non-unital ring structure, where addition and multiplication are defined pointwise.

Filter.Germ.instNonAssocRing instance

[NonAssocRing R] : NonAssocRing (Germ l R)

Full source

instance instNonAssocRing [NonAssocRing R] : NonAssocRing (Germ l R) where
  __ := instNonUnitalNonAssocRing
  __ := instNonAssocSemiring
  __ := instAddGroupWithOne

Non-Associative Ring Structure on Germs of Functions

Informal description

For any non-associative ring $R$ and any filter $l$ on a type $\alpha$, the space of germs $\mathrm{Germ}_l R$ inherits a non-associative ring structure, where addition and multiplication are defined pointwise on representatives.

Filter.Germ.instSemiring instance

[Semiring R] : Semiring (Germ l R)

Full source

instance instSemiring [Semiring R] : Semiring (Germ l R) where
  __ := instNonUnitalSemiring
  __ := instNonAssocSemiring
  __ := instMonoidWithZero

Semiring Structure on Germs of Functions

Informal description

For any semiring $R$ and any filter $l$ on a type $\alpha$, the space of germs $\mathrm{Germ}_l R$ inherits a semiring structure, where addition and multiplication are defined pointwise.

Filter.Germ.instRing instance

[Ring R] : Ring (Germ l R)

Full source

instance instRing [Ring R] : Ring (Germ l R) where
  __ := instSemiring
  __ := instAddCommGroup
  __ := instNonAssocRing

Ring Structure on Germs of Functions

Informal description

For any ring $R$ and any filter $l$ on a type $\alpha$, the space of germs $\mathrm{Germ}_l R$ inherits a ring structure, where addition and multiplication are defined pointwise on representatives.

Filter.Germ.instNonUnitalCommSemiring instance

[NonUnitalCommSemiring R] : NonUnitalCommSemiring (Germ l R)

Full source

instance instNonUnitalCommSemiring [NonUnitalCommSemiring R] :
    NonUnitalCommSemiring (Germ l R) :=
  { mul_comm := mul_comm }

Non-Unital Commutative Semiring Structure on Germs of Functions

Informal description

For any non-unital commutative semiring $R$, the space of germs $\mathrm{Germ}_l R$ inherits a non-unital commutative semiring structure, where addition and multiplication are defined pointwise.

Filter.Germ.instCommSemiring instance

[CommSemiring R] : CommSemiring (Germ l R)

Full source

instance instCommSemiring [CommSemiring R] : CommSemiring (Germ l R) :=
  { mul_comm := mul_comm }

Commutative Semiring Structure on Germs of Functions

Informal description

For any commutative semiring $R$ and any filter $l$ on a type $\alpha$, the space of germs $\mathrm{Germ}_l R$ inherits a commutative semiring structure, where addition and multiplication are defined pointwise.

Filter.Germ.instNonUnitalCommRing instance

[NonUnitalCommRing R] : NonUnitalCommRing (Germ l R)

Full source

instance instNonUnitalCommRing [NonUnitalCommRing R] : NonUnitalCommRing (Germ l R) where
  __ := instNonUnitalRing
  __ := instCommSemigroup

Non-Unital Commutative Ring Structure on Germs of Functions

Informal description

For any non-unital commutative ring $R$, the space of germs $\mathrm{Germ}_l R$ at a filter $l$ inherits a non-unital commutative ring structure, where addition and multiplication are defined pointwise.

Filter.Germ.instCommRing instance

[CommRing R] : CommRing (Germ l R)

Full source

instance instCommRing [CommRing R] : CommRing (Germ l R) :=
  { mul_comm := mul_comm }

Commutative Ring Structure on Germs of Functions at a Filter

Informal description

For any commutative ring $R$ and any filter $l$ on a type $\alpha$, the space of germs $\mathrm{Germ}_l R$ inherits a commutative ring structure, where addition and multiplication are defined pointwise on representatives.

Filter.Germ.coeRingHom definition

[Semiring R] (l : Filter α) : (α → R) →+* Germ l R

Full source

/-- Coercion `(α → R) → Germ l R` as a `RingHom`. -/
def coeRingHom [Semiring R] (l : Filter α) : (α → R) →+* Germ l R :=
  { (coeMulHom l : _ →* Germ l R), (coeAddHom l : _ →+ Germ l R) with toFun := ofFun }

Ring homomorphism from functions to germs at a filter

Informal description

The function `Filter.Germ.coeRingHom` is a ring homomorphism from the space of functions `α → R` to the space of germs `Germ l R`, where `R` is a semiring and `l` is a filter on `α`. It maps a function `f : α → R` to its germ at the filter `l`, preserving both the additive and multiplicative structures. Specifically, it satisfies: - `coeRingHom l (f + g) = coeRingHom l f + coeRingHom l g` - `coeRingHom l (f * g) = coeRingHom l f * coeRingHom l g` - `coeRingHom l 1 = 1` - `coeRingHom l 0 = 0`

Filter.Germ.coe_coeRingHom theorem

[Semiring R] : (coeRingHom l : (α → R) → Germ l R) = ofFun

Full source

@[simp]
theorem coe_coeRingHom [Semiring R] : (coeRingHom l : (α → R) → Germ l R) = ofFun :=
  rfl

Equality of Ring Homomorphism and Germ Construction for Semiring-Valued Functions

Informal description

For any semiring $R$ and any filter $l$ on a type $\alpha$, the ring homomorphism $\mathrm{coeRingHom}_l$ from the space of functions $\alpha \to R$ to the space of germs $\mathrm{Germ}_l R$ coincides with the germ construction map $\mathrm{ofFun}$. That is, $\mathrm{coeRingHom}_l = \mathrm{ofFun}$.

Filter.Germ.instSMul' instance

[SMul M β] : SMul (Germ l M) (Germ l β)

Full source

@[to_additive]
instance instSMul' [SMul M β] : SMul (Germ l M) (Germ l β) :=
  ⟨map₂ (· • ·)⟩

Scalar Multiplication on Germs

Informal description

For any type $M$ with a scalar multiplication operation on a type $\beta$, the space of germs $\text{Germ } l \beta$ inherits a scalar multiplication operation from $\text{Germ } l M$.

Filter.Germ.coe_smul' theorem

[SMul M β] (c : α → M) (f : α → β) : ↑(c • f) = (c : Germ l M) • (f : Germ l β)

Full source

@[to_additive (attr := simp, norm_cast)]
theorem coe_smul' [SMul M β] (c : α → M) (f : α → β) : ↑(c • f) = (c : Germ l M) • (f : Germ l β) :=
  rfl

Germ of scalar product equals scalar product of germs

Informal description

For any scalar multiplication operation between types $M$ and $\beta$, and for any functions $c : \alpha \to M$ and $f : \alpha \to \beta$, the germ of the pointwise scalar product $c \cdot f$ at filter $l$ is equal to the scalar product of the germs of $c$ and $f$ at $l$. In other words, $\overline{c \cdot f} = \overline{c} \cdot \overline{f}$ in $\text{Germ}_l \beta$, where $\overline{\cdot}$ denotes the germ of a function at $l$.

Filter.Germ.instMulAction instance

[Monoid M] [MulAction M β] : MulAction M (Germ l β)

Full source

@[to_additive]
instance instMulAction [Monoid M] [MulAction M β] : MulAction M (Germ l β) where
  one_smul f :=
    inductionOn f fun f => by
      norm_cast
      simp [one_smul]
  mul_smul c₁ c₂ f :=
    inductionOn f fun f => by
      norm_cast
      simp [mul_smul]

Multiplicative Action on Germs of Functions

Informal description

For any monoid $M$ acting on a type $\beta$, the space of germs $\text{Germ}_l \beta$ inherits a multiplicative action structure from $M$, where the action is defined pointwise on representatives.

Filter.Germ.instMulAction' instance

[Monoid M] [MulAction M β] : MulAction (Germ l M) (Germ l β)

Full source

@[to_additive]
instance instMulAction' [Monoid M] [MulAction M β] : MulAction (Germ l M) (Germ l β) where
  one_smul f := inductionOn f fun f => by simp only [← coe_one, ← coe_smul', one_smul]
  mul_smul c₁ c₂ f :=
    inductionOn₃ c₁ c₂ f fun c₁ c₂ f => by
      norm_cast
      simp [mul_smul]

Multiplicative Action on Germs of Functions via Germs of Monoids

Informal description

For any monoid $M$ acting on a type $\beta$, the space of germs $\mathrm{Germ}_l \beta$ inherits a multiplicative action structure from the space of germs $\mathrm{Germ}_l M$, where the action is defined pointwise on representatives.

Filter.Germ.instDistribMulAction instance

[Monoid M] [AddMonoid N] [DistribMulAction M N] : DistribMulAction M (Germ l N)

Full source

instance instDistribMulAction [Monoid M] [AddMonoid N] [DistribMulAction M N] :
    DistribMulAction M (Germ l N) where
  smul_add c f g :=
    inductionOn₂ f g fun f g => by
      norm_cast
      simp [smul_add]
  smul_zero c := by simp only [← coe_zero, ← coe_smul, smul_zero]

Distributive Multiplicative Action on Germs of Functions

Informal description

For any monoid $M$ and additive monoid $N$ equipped with a distributive multiplicative action of $M$ on $N$, the space of germs $\text{Germ}_l N$ inherits a distributive multiplicative action structure from $M$, where the action is defined pointwise on representatives.

Filter.Germ.instDistribMulAction' instance

[Monoid M] [AddMonoid N] [DistribMulAction M N] : DistribMulAction (Germ l M) (Germ l N)

Full source

instance instDistribMulAction' [Monoid M] [AddMonoid N] [DistribMulAction M N] :
    DistribMulAction (Germ l M) (Germ l N) where
  smul_add c f g :=
    inductionOn₃ c f g fun c f g => by
      norm_cast
      simp [smul_add]
  smul_zero c := inductionOn c fun c => by simp only [← coe_zero, ← coe_smul', smul_zero]

Distributive Multiplicative Action on Germs of Functions via Germs of Monoids

Informal description

For any monoid $M$, additive monoid $N$, and distributive multiplicative action of $M$ on $N$, the space of germs $\mathrm{Germ}_l N$ inherits a distributive multiplicative action structure from the space of germs $\mathrm{Germ}_l M$, where the action is defined pointwise on representatives.

Filter.Germ.instModule instance

[Semiring R] [AddCommMonoid M] [Module R M] : Module R (Germ l M)

Full source

instance instModule [Semiring R] [AddCommMonoid M] [Module R M] : Module R (Germ l M) where
  add_smul c₁ c₂ f :=
    inductionOn f fun f => by
      norm_cast
      simp [add_smul]
  zero_smul f :=
    inductionOn f fun f => by
      norm_cast
      simp [zero_smul, coe_zero]

Module Structure on Germs of Functions

Informal description

For any semiring $R$ and additive commutative monoid $M$ equipped with a module structure of $R$ over $M$, the space of germs $\text{Germ}_l M$ inherits a module structure from $R$, where the scalar multiplication is defined pointwise on representatives.

Filter.Germ.instModule' instance

[Semiring R] [AddCommMonoid M] [Module R M] : Module (Germ l R) (Germ l M)

Full source

instance instModule' [Semiring R] [AddCommMonoid M] [Module R M] :
    Module (Germ l R) (Germ l M) where
  add_smul c₁ c₂ f :=
    inductionOn₃ c₁ c₂ f fun c₁ c₂ f => by
      norm_cast
      simp [add_smul]
  zero_smul f := inductionOn f fun f => by simp only [← coe_zero, ← coe_smul', zero_smul]

Module Structure on Germs of Functions via Germs of Semirings

Informal description

For any semiring $R$, additive commutative monoid $M$, and module structure of $R$ over $M$, the space of germs $\mathrm{Germ}_l M$ inherits a module structure from the space of germs $\mathrm{Germ}_l R$, where the scalar multiplication is defined pointwise on representatives.

Filter.Germ.instLE instance

[LE β] : LE (Germ l β)

Full source

instance instLE [LE β] : LE (Germ l β) := ⟨LiftRel (· ≤ ·)⟩

Preorder Structure on Germs of Functions

Informal description

For any type $\beta$ with a preorder structure $\leq$, the space of germs $\text{Germ}\, l\, \beta$ inherits a preorder structure where $f \leq g$ if and only if $f(x) \leq g(x)$ for all $x$ in some set belonging to the filter $l$.

Filter.Germ.le_def theorem

[LE β] : ((· ≤ ·) : Germ l β → Germ l β → Prop) = LiftRel (· ≤ ·)

Full source

theorem le_def [LE β] : ((· ≤ ·) : Germ l β → Germ l β → Prop) = LiftRel (· ≤ ·) :=
  rfl

Definition of Inequality on Germs via Lifted Relation

Informal description

For any type $\beta$ with a preorder relation $\leq$, the inequality relation on the space of germs $\text{Germ}\, l\, \beta$ is defined as the lifting of the relation $\leq$ via $\text{LiftRel}$. That is, for any two germs $f, g \in \text{Germ}\, l\, \beta$, we have $f \leq g$ if and only if $\text{LiftRel}\, (\leq)\, f\, g$ holds.

Filter.Germ.coe_le theorem

[LE β] : (f : Germ l β) ≤ g ↔ f ≤ᶠ[l] g

Full source

@[simp]
theorem coe_le [LE β] : (f : Germ l β) ≤ g ↔ f ≤ᶠ[l] g :=
  Iff.rfl

Inequality of Germs via Eventual Inequality

Informal description

For any type $\beta$ with a preorder relation $\leq$, and for any two germs $f, g \in \text{Germ}\, l\, \beta$, the inequality $f \leq g$ holds if and only if the functions $f$ and $g$ satisfy $f(x) \leq g(x)$ for all $x$ in some set belonging to the filter $l$.

Filter.Germ.coe_nonneg theorem

[LE β] [Zero β] {f : α → β} : 0 ≤ (f : Germ l β) ↔ ∀ᶠ x in l, 0 ≤ f x

Full source

theorem coe_nonneg [LE β] [Zero β] {f : α → β} : 0 ≤ (f : Germ l β) ↔ ∀ᶠ x in l, 0 ≤ f x :=
  Iff.rfl

Non-Negativity of a Germ via Eventual Non-Negativity of the Function

Informal description

For a type $\beta$ equipped with a preorder relation $\leq$ and a zero element $0$, and for any function $f : \alpha \to \beta$, the germ of $f$ at a filter $l$ is non-negative (i.e., $0 \leq f$ in $\text{Germ}\, l\, \beta$) if and only if the function $f$ is eventually non-negative along $l$, meaning there exists a set in $l$ where $0 \leq f(x)$ for all $x$ in that set.

Filter.Germ.const_le theorem

[LE β] {x y : β} : x ≤ y → (↑x : Germ l β) ≤ ↑y

Full source

theorem const_le [LE β] {x y : β} : x ≤ y → (↑x : Germ l β) ≤ ↑y :=
  liftRel_const

Germ Inequality for Constant Functions: $x \leq y \Rightarrow [x] \leq [y]$

Informal description

For any type $\beta$ equipped with a preorder relation $\leq$ and elements $x, y \in \beta$, if $x \leq y$, then the germ of the constant function $x$ at the filter $l$ is less than or equal to the germ of the constant function $y$ at the same filter. That is, $x \leq y$ implies $[x] \leq [y]$, where $[x]$ and $[y]$ denote the germs of the constant functions $x$ and $y$ at $l$ respectively.

Filter.Germ.const_le_iff theorem

[LE β] [NeBot l] {x y : β} : (↑x : Germ l β) ≤ ↑y ↔ x ≤ y

Full source

@[simp, norm_cast]
theorem const_le_iff [LE β] [NeBot l] {x y : β} : (↑x : Germ l β) ≤ ↑y ↔ x ≤ y :=
  liftRel_const_iff

Comparison of Constant Germs in a Nontrivial Filter

Informal description

For a nontrivial filter $l$ on a type $\alpha$ and elements $x, y$ in a type $\beta$ equipped with a preorder $\leq$, the germ of the constant function $x$ at $l$ is less than or equal to the germ of the constant function $y$ at $l$ if and only if $x \leq y$ in $\beta$. In other words, $[x] \leq [y]$ in $\text{Germ}\, l\, \beta$ holds precisely when $x \leq y$ in $\beta$.

Filter.Germ.instPreorder instance

[Preorder β] : Preorder (Germ l β)

Full source

instance instPreorder [Preorder β] : Preorder (Germ l β) where
  le := (· ≤ ·)
  le_refl f := inductionOn f <| EventuallyLE.refl l
  le_trans f₁ f₂ f₃ := inductionOn₃ f₁ f₂ f₃ fun _ _ _ => EventuallyLE.trans

Preorder Structure on Germs of Functions

Informal description

For any type $\beta$ with a preorder structure, the space of germs $\text{Germ}\, l\, \beta$ inherits a preorder structure where $f \leq g$ if and only if $f(x) \leq g(x)$ for all $x$ in some set belonging to the filter $l$.

Filter.Germ.instPartialOrder instance

[PartialOrder β] : PartialOrder (Germ l β)

Full source

instance instPartialOrder [PartialOrder β] : PartialOrder (Germ l β) where
  le_antisymm f g := inductionOn₂ f g fun _ _ h₁ h₂ ↦ (EventuallyLE.antisymm h₁ h₂).germ_eq

Partial Order Structure on Germs of Functions

Informal description

For any type $\beta$ with a partial order structure, the space of germs $\text{Germ}\, l\, \beta$ inherits a partial order structure where $f \leq g$ if and only if $f(x) \leq g(x)$ for all $x$ in some set belonging to the filter $l$.

Filter.Germ.instBot instance

[Bot β] : Bot (Germ l β)

Full source

instance instBot [Bot β] : Bot (Germ l β) := ⟨↑(⊥ : β)⟩

Bottom Element in the Space of Germs

Informal description

For any type $\beta$ with a bottom element $\bot$ and any filter $l$ on a type $\alpha$, the space of germs $\text{Germ}\, l\, \beta$ inherits a bottom element, which is the germ of the constant function $\fun x \mapsto \bot$.

Filter.Germ.instTop instance

[Top β] : Top (Germ l β)

Full source

instance instTop [Top β] : Top (Germ l β) := ⟨↑(⊤ : β)⟩

Top Element in the Space of Germs

Informal description

For any type $\beta$ with a top element $\top$ and any filter $l$ on a type $\alpha$, the space of germs $\text{Germ}\, l\, \beta$ inherits a top element, which is the germ of the constant function $\fun x \mapsto \top$.

Filter.Germ.const_bot theorem

[Bot β] : (↑(⊥ : β) : Germ l β) = ⊥

Full source

@[simp, norm_cast]
theorem const_bot [Bot β] : (↑(⊥ : β) : Germ l β) = ⊥ :=
  rfl

Germ of the Bottom Constant Function Equals Bottom Germ

Informal description

For any type $\beta$ with a bottom element $\bot$, the germ of the constant function $\fun x \mapsto \bot$ at a filter $l$ is equal to the bottom element in the space of germs $\text{Germ}\, l\, \beta$.

Filter.Germ.const_top theorem

[Top β] : (↑(⊤ : β) : Germ l β) = ⊤

Full source

@[simp, norm_cast]
theorem const_top [Top β] : (↑(⊤ : β) : Germ l β) = ⊤ :=
  rfl

Germ of Constant Top Function is Top Element

Informal description

For any type $\beta$ with a top element $\top$ and any filter $l$ on a type $\alpha$, the germ of the constant function $\fun x \mapsto \top$ at $l$ is equal to the top element in the space of germs $\text{Germ}\, l\, \beta$.

Filter.Germ.instOrderBot instance

[LE β] [OrderBot β] : OrderBot (Germ l β)

Full source

instance instOrderBot [LE β] [OrderBot β] : OrderBot (Germ l β) where
  bot_le f := inductionOn f fun _ => Eventually.of_forall fun _ => bot_le

Order with Bottom Element on Germs of Functions

Informal description

For any type $\beta$ with a preorder and a bottom element $\bot$, the space of germs $\text{Germ}\, l\, \beta$ inherits an order with a bottom element, where the bottom element is the germ of the constant function $\fun x \mapsto \bot$.

Filter.Germ.instOrderTop instance

[LE β] [OrderTop β] : OrderTop (Germ l β)

Full source

instance instOrderTop [LE β] [OrderTop β] : OrderTop (Germ l β) where
  le_top f := inductionOn f fun _ => Eventually.of_forall fun _ => le_top

Order-Top Structure on Germs of Functions

Informal description

For any type $\beta$ with a preorder structure $\leq$ and a top element $\top$, the space of germs $\text{Germ}\, l\, \beta$ inherits an order-top structure, where the top element is the germ of the constant function $x \mapsto \top$.

Filter.Germ.instBoundedOrder instance

[LE β] [BoundedOrder β] : BoundedOrder (Germ l β)

Full source

instance instBoundedOrder [LE β] [BoundedOrder β] : BoundedOrder (Germ l β) where
  __ := instOrderBot
  __ := instOrderTop

Bounded Order Structure on Germs of Functions

Informal description

For any type $\beta$ with a bounded order structure (i.e., a partial order with both a greatest element $\top$ and a least element $\bot$), the space of germs $\text{Germ}\, l\, \beta$ inherits a bounded order structure. The top and bottom elements in $\text{Germ}\, l\, \beta$ are the germs of the constant functions $x \mapsto \top$ and $x \mapsto \bot$ respectively.

Filter.Germ.instSup instance

[Max β] : Max (Germ l β)

Full source

instance instSup [Max β] : Max (Germ l β) := ⟨map₂ (· ⊔ ·)⟩

Maximum Operation on Germs of Functions at a Filter

Informal description

For any type $\beta$ equipped with a maximum operation $\sqcup$, the space of germs $\text{Germ } l \beta$ inherits a maximum operation, where the maximum of two germs is defined as the germ of the pointwise maximum of their representatives.

Filter.Germ.instInf instance

[Min β] : Min (Germ l β)

Full source

instance instInf [Min β] : Min (Germ l β) := ⟨map₂ (· ⊓ ·)⟩

Minimum Operation on Germs

Informal description

For any type $\beta$ with a minimum operation $\sqcap$, the space of germs $\text{Germ } l \beta$ inherits a minimum operation, where the minimum of two germs is defined as the germ of the pointwise minimum of their representatives.

Filter.Germ.const_sup theorem

[Max β] (a b : β) : ↑(a ⊔ b) = (↑a ⊔ ↑b : Germ l β)

Full source

@[simp, norm_cast]
theorem const_sup [Max β] (a b : β) : ↑(a ⊔ b) = (↑a ⊔ ↑b : Germ l β) :=
  rfl

Germ of Maximum Equals Maximum of Germs for Constant Functions

Informal description

For any type $\beta$ with a maximum operation $\sqcup$ and elements $a, b \in \beta$, the germ of the constant function $x \mapsto a \sqcup b$ at a filter $l$ is equal to the maximum of the germs of the constant functions $x \mapsto a$ and $x \mapsto b$ in the space of germs $\text{Germ } l \beta$. In other words, $\uparrow(a \sqcup b) = \uparrow a \sqcup \uparrow b$ in $\text{Germ } l \beta$.

Filter.Germ.const_inf theorem

[Min β] (a b : β) : ↑(a ⊓ b) = (↑a ⊓ ↑b : Germ l β)

Full source

@[simp, norm_cast]
theorem const_inf [Min β] (a b : β) : ↑(a ⊓ b) = (↑a ⊓ ↑b : Germ l β) :=
  rfl

Germ of Minimum Equals Minimum of Germs for Constant Functions

Informal description

For any type $\beta$ equipped with a minimum operation $\sqcap$ and elements $a, b \in \beta$, the germ of the constant function $x \mapsto a \sqcap b$ at a filter $l$ is equal to the minimum of the germs of the constant functions $x \mapsto a$ and $x \mapsto b$ in the space of germs $\text{Germ } l \beta$. In other words, $\uparrow(a \sqcap b) = \uparrow a \sqcap \uparrow b$ in $\text{Germ } l \beta$.

Filter.Germ.instSemilatticeSup instance

[SemilatticeSup β] : SemilatticeSup (Germ l β)

Full source

instance instSemilatticeSup [SemilatticeSup β] : SemilatticeSup (Germ l β) where
  sup := max
  le_sup_left f g := inductionOn₂ f g fun _f _g => Eventually.of_forall fun _x ↦ le_sup_left
  le_sup_right f g := inductionOn₂ f g fun _f _g ↦ Eventually.of_forall fun _x ↦ le_sup_right
  sup_le f₁ f₂ g := inductionOn₃ f₁ f₂ g fun _f₁ _f₂ _g h₁ h₂ ↦ h₂.mp <| h₁.mono fun _x ↦ sup_le

Join-Semilattice Structure on Germs of Functions

Informal description

For any type $\beta$ with a join-semilattice structure, the space of germs $\text{Germ}\, l\, \beta$ inherits a join-semilattice structure where the join operation is defined pointwise. Specifically, for two germs $f$ and $g$ in $\text{Germ}\, l\, \beta$, their join $f \sqcup g$ is the germ of the function $x \mapsto f(x) \sqcup g(x)$.

Filter.Germ.instSemilatticeInf instance

[SemilatticeInf β] : SemilatticeInf (Germ l β)

Full source

instance instSemilatticeInf [SemilatticeInf β] : SemilatticeInf (Germ l β) where
  inf := min
  inf_le_left f g := inductionOn₂ f g fun _f _g ↦ Eventually.of_forall fun _x ↦ inf_le_left
  inf_le_right f g := inductionOn₂ f g fun _f _g ↦ Eventually.of_forall fun _x ↦ inf_le_right
  le_inf f₁ f₂ g := inductionOn₃ f₁ f₂ g fun _f₁ _f₂ _g h₁ h₂ ↦ h₂.mp <| h₁.mono fun _x ↦ le_inf

Meet-Semilattice Structure on Germs of Functions

Informal description

For any meet-semilattice $\beta$, the space of germs $\text{Germ}\, l\, \beta$ inherits a meet-semilattice structure, where the meet of two germs is defined as the germ of the pointwise meet of their representatives. That is, for germs $f$ and $g$ in $\text{Germ}\, l\, \beta$, the meet $f \sqcap g$ is the germ of the function $x \mapsto f(x) \sqcap g(x)$.

Filter.Germ.instLattice instance

[Lattice β] : Lattice (Germ l β)

Full source

instance instLattice [Lattice β] : Lattice (Germ l β) where
  __ := instSemilatticeSup
  __ := instSemilatticeInf

Lattice Structure on Germs of Functions at a Filter

Informal description

For any lattice $\beta$, the space of germs $\text{Germ}\, l\, \beta$ at a filter $l$ inherits a lattice structure, where the join and meet operations are defined pointwise. That is, for two germs $f$ and $g$ in $\text{Germ}\, l\, \beta$, their join $f \sqcup g$ is the germ of the function $x \mapsto f(x) \sqcup g(x)$, and their meet $f \sqcap g$ is the germ of the function $x \mapsto f(x) \sqcap g(x)$.

Filter.Germ.instDistribLattice instance

[DistribLattice β] : DistribLattice (Germ l β)

Full source

instance instDistribLattice [DistribLattice β] : DistribLattice (Germ l β) where
  le_sup_inf f g h := inductionOn₃ f g h fun _f _g _h ↦ Eventually.of_forall fun _ ↦ le_sup_inf

Distributive Lattice Structure on Germs of Functions at a Filter

Informal description

For any distributive lattice $\beta$, the space of germs $\text{Germ}\, l\, \beta$ at a filter $l$ inherits a distributive lattice structure, where the join and meet operations are defined pointwise. That is, for two germs $f$ and $g$ in $\text{Germ}\, l\, \beta$, their join $f \sqcup g$ is the germ of the function $x \mapsto f(x) \sqcup g(x)$, and their meet $f \sqcap g$ is the germ of the function $x \mapsto f(x) \sqcap g(x)$. The distributivity property is preserved under this construction.

Filter.Germ.instExistsMulOfLE instance

[Mul β] [LE β] [ExistsMulOfLE β] : ExistsMulOfLE (Germ l β)

Full source

@[to_additive]
instance instExistsMulOfLE [Mul β] [LE β] [ExistsMulOfLE β] : ExistsMulOfLE (Germ l β) where
  exists_mul_of_le {x y} := inductionOn₂ x y fun f g (h : f ≤ᶠ[l] g) ↦ by
    classical
    choose c hc using fun x (hx : f x ≤ g x) ↦ exists_mul_of_le hx
    refine ⟨ofFun fun x ↦ if hx : f x ≤ g x then c x hx else f x, coe_eq.2 ?_⟩
    filter_upwards [h] with x hx
    rw [dif_pos hx, hc]

Existence of Multiplicative Factors for Germs in Ordered Commutative Monoids

Informal description

For any type $\beta$ equipped with a multiplication operation and a preorder relation $\leq$ satisfying the property that for any elements $a \leq b$ there exists $c$ such that $a \cdot c = b$, the space of germs $\text{Germ}_l \beta$ at a filter $l$ inherits the same property. That is, for any germs $f \leq g$ in $\text{Germ}_l \beta$, there exists a germ $h$ such that $f \cdot h = g$.

Mathlib.Order.Filter.Germ.Basic

Main definitions

Tags