Indistinguishable processes

We build a space of equivalence classes of processes, where two processes are treated as identical if they are Indistinguishable. We form the set of equivalence classes under the relation of being indistinguishable. We consider equivalence classes of strongly adapted processes (or, equivalently, of almost everywhere strongly adapted processes.)

Notation

• α →ₚ[μ, 𝓕] β

Main statements

• The linear structure of L⁰ : Addition and scalar multiplication are defined on L⁰ in the natural way, i.e., [f] + [g] := [f + g], c • [f] := [c • f]. So defined, α →ₚ β inherits the linear structure of β. For example, if β is a module, then α →ₚ β is a module over the same ring.

  See mk_add_mk, neg_mk, mk_sub, smul_mk, coeFn_add, coeFn_neg, coeFn_sub, coeFn_smul

• The order structure of L⁰ : ≤ can be defined in a similar way: [f] ≤ [g] if f a ≤ g a for almost all a in domain. And α →ₚ β inherits the preorder and partial order of β.

  TODO: Define sup and inf on L⁰ so that it forms a lattice. It seems that β must be a linear order, since otherwise f ⊔ g may not be a measurable function.

Implementation notes

• f.cast: To find a representative of f : α →ₚ β, use the coercion (f : α → β), which is implemented as f.toFun. For each operation op in L⁰, there is a lemma called coe_fn_op, characterizing, say, (f op g : α → β).
• AEEqProcess.mk: To construct an L⁰ function α →ₚ β from an almost everywhere strongly measurable function f : α → β, use ae_eq_fun.mk
• comp: Use comp g f to get [g ∘ f] from g : β → γ and [f] : α →ₚ γ when g is continuous. Use compMeasurable if g is only measurable (this requires the target space to be second countable).
• comp₂: Use comp₂ g f₁ f₂ to get [fun a ↦ g (f₁ a) (f₂ a)]. For example, [f + g] is comp₂ (+)

@[implicit_reducible]

def MeasureTheory.Measure.aeEqSetoid' {ι : Type u_1} {α : Type u_2} (β : Type u_3) {mα : MeasurableSpace α} [Preorder ι] (𝓕 : Filtration ι mα) [TopologicalSpace β] (μ : Measure α) : Setoid { X : ι → α → β // AEStronglyAdapted X 𝓕 μ }

The equivalence relation of being almost everywhere equal for almost everywhere strongly measurable functions.

Equations

• MeasureTheory.Measure.aeEqSetoid' β 𝓕 μ = { r := fun (f g : { X : ι → α → β // MeasureTheory.AEStronglyAdapted X 𝓕 μ }) => ↑f ≡ᵐ[μ] ↑g, iseqv := ⋯ }

def MeasureTheory.AEEqProcess {ι : Type u_1} (α : Type u_2) (β : Type u_3) {mα : MeasurableSpace α} [Preorder ι] (𝓕 : Filtration ι mα) [TopologicalSpace β] (μ : Measure α) : Type (max (max u_1 u_2) u_3)

The space of equivalence classes of almost everywhere strongly measurable functions, where two strongly measurable functions are equivalent if they agree almost everywhere, i.e., they differ on a set of measure 0.

Equations

• (α →ₚ[μ, 𝓕] β) = Quotient (MeasureTheory.Measure.aeEqSetoid' β 𝓕 μ)

def MeasureTheory.«term_→ₚ[_,_]_» : Lean.TrailingParserDescr

The space of equivalence classes of almost everywhere strongly measurable functions, where two strongly measurable functions are equivalent if they agree almost everywhere, i.e., they differ on a set of measure 0.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.AEEqProcess.mk {ι : Type u_1} {α : Type u_2} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} {β : Type u_6} [TopologicalSpace β] (f : ι → α → β) (hf : AEStronglyAdapted f 𝓕 μ) : α →ₚ[μ, 𝓕] β

Construct the equivalence class [f] of an almost everywhere measurable function f, based on the equivalence relation of being almost everywhere equal.

Equations

• MeasureTheory.AEEqProcess.mk f hf = Quotient.mk'' ⟨f, hf⟩

noncomputable def MeasureTheory.AEEqProcess.cast {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] (X : α →ₚ[μ, 𝓕] β) : ι → α → β

Coercion from a space of equivalence classes of almost everywhere strongly measurable functions to functions. We ensure that if f has a constant representative, then we choose that one.

Equations

• ↑X = if h : ∃ (c : β), X = MeasureTheory.AEEqProcess.mk (fun (x : ι) (x_1 : α) => c) ⋯ then fun (x : ι) (x_1 : α) => h.choose else MeasureTheory.AEStronglyAdapted.mk ↑(Quotient.out X) ⋯

@[instance_reducible]

noncomputable instance MeasureTheory.AEEqProcess.instCoeFun {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] : CoeFun (α →ₚ[μ, 𝓕] β) fun (x : α →ₚ[μ, 𝓕] β) => ι → α → β

A measurable representative of an AEEqProcess [f]

Equations

• MeasureTheory.AEEqProcess.instCoeFun = { coe := MeasureTheory.AEEqProcess.cast }

theorem MeasureTheory.AEEqProcess.stronglyAdapted {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] (f : α →ₚ[μ, 𝓕] β) : StronglyAdapted 𝓕 ↑f

theorem MeasureTheory.AEEqProcess.aestronglyAdapted {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] (f : α →ₚ[μ, 𝓕] β) : AEStronglyAdapted (↑f) 𝓕 μ

theorem MeasureTheory.AEEqProcess.adapted {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] (f : α →ₚ[μ, 𝓕] β) : Adapted 𝓕 ↑f

@[simp]

theorem MeasureTheory.AEEqProcess.quot_mk_eq_mk {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] (f : ι → α → β) (hf : AEStronglyAdapted f 𝓕 μ) : Quot.mk ⇑(Measure.aeEqSetoid' β 𝓕 μ) ⟨f, hf⟩ = mk f hf

@[simp]

theorem MeasureTheory.AEEqProcess.mk_eq_mk {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] {f g : ι → α → β} {hf : AEStronglyAdapted f 𝓕 μ} {hg : AEStronglyAdapted g 𝓕 μ} : mk f hf = mk g hg ↔ f ≡ᵐ[μ] g

@[simp]

theorem MeasureTheory.AEEqProcess.mk_coeFn {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] (f : α →ₚ[μ, 𝓕] β) : mk ↑f ⋯ = f

theorem MeasureTheory.AEEqProcess.ext {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] {f g : α →ₚ[μ, 𝓕] β} (h : ↑f ≡ᵐ[μ] ↑g) : f = g

theorem MeasureTheory.AEEqProcess.ext_iff {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] {f g : α →ₚ[μ, 𝓕] β} : f = g ↔ ↑f ≡ᵐ[μ] ↑g

theorem MeasureTheory.AEEqProcess.coeFn_mk {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] (f : ι → α → β) (hf : AEStronglyAdapted f 𝓕 μ) : ↑(mk f hf) ≡ᵐ[μ] f

theorem MeasureTheory.AEEqProcess.induction_on {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] (f : α →ₚ[μ, 𝓕] β) {p : (α →ₚ[μ, 𝓕] β) → Prop} (H : ∀ (f : ι → α → β) (hf : AEStronglyAdapted f 𝓕 μ), p (mk f hf)) : p f

theorem MeasureTheory.AEEqProcess.induction_on₂ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] {α' : Type u_6} {β' : Type u_7} {ι' : Type u_8} {mα' : MeasurableSpace α'} [TopologicalSpace β'] {μ' : Measure α'} [Preorder ι'] {𝓕' : Filtration ι' mα'} (f : α →ₚ[μ, 𝓕] β) (f' : α' →ₚ[μ', 𝓕'] β') {p : (α →ₚ[μ, 𝓕] β) → (α' →ₚ[μ', 𝓕'] β') → Prop} (H : ∀ (f : ι → α → β) (hf : AEStronglyAdapted f 𝓕 μ) (f' : ι' → α' → β') (hf' : AEStronglyAdapted f' 𝓕' μ'), p (mk f hf) (mk f' hf')) : p f f'

theorem MeasureTheory.AEEqProcess.induction_on₃ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] {α' : Type u_6} {β' : Type u_7} {ι' : Type u_8} {mα' : MeasurableSpace α'} [TopologicalSpace β'] {μ' : Measure α'} [Preorder ι'] {𝓕' : Filtration ι' mα'} {α'' : Type u_9} {β'' : Type u_10} {ι'' : Type u_11} {mα'' : MeasurableSpace α''} [TopologicalSpace β''] {μ'' : Measure α''} [Preorder ι''] {𝓕'' : Filtration ι'' mα''} (f : α →ₚ[μ, 𝓕] β) (f' : α' →ₚ[μ', 𝓕'] β') (f'' : α'' →ₚ[μ'', 𝓕''] β'') {p : (α →ₚ[μ, 𝓕] β) → (α' →ₚ[μ', 𝓕'] β') → (α'' →ₚ[μ'', 𝓕''] β'') → Prop} (H : ∀ (f : ι → α → β) (hf : AEStronglyAdapted f 𝓕 μ) (f' : ι' → α' → β') (hf' : AEStronglyAdapted f' 𝓕' μ') (f'' : ι'' → α'' → β'') (hf'' : AEStronglyAdapted f'' 𝓕'' μ''), p (mk f hf) (mk f' hf') (mk f'' hf'')) : p f f' f''

def MeasureTheory.AEEqProcess.comp {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] [TopologicalSpace γ] (g : β → γ) (hg : Continuous g) (f : α →ₚ[μ, 𝓕] β) : α →ₚ[μ, 𝓕] γ

Given a continuous function g : β → γ, and an almost everywhere equal function [f] : α →ₚ β, return the equivalence class of g ∘ f, i.e., the almost everywhere equal function [g ∘ f] : α →ₚ γ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MeasureTheory.AEEqProcess.comp_mk {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] [TopologicalSpace γ] (g : β → γ) (hg : Continuous g) (f : ι → α → β) (hf : AEStronglyAdapted f 𝓕 μ) : comp g hg (mk f hf) = mk (fun (t : ι) => g ∘ f t) ⋯

@[simp]

theorem MeasureTheory.AEEqProcess.comp_id {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] (f : α →ₚ[μ, 𝓕] β) : comp id ⋯ f = f

@[simp]

theorem MeasureTheory.AEEqProcess.comp_comp {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace δ] [TopologicalSpace β] [TopologicalSpace γ] (g : γ → δ) (g' : β → γ) (hg : Continuous g) (hg' : Continuous g') (f : α →ₚ[μ, 𝓕] β) : comp g hg (comp g' hg' f) = comp (g ∘ g') ⋯ f

theorem MeasureTheory.AEEqProcess.comp_eq_mk {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] [TopologicalSpace γ] (g : β → γ) (hg : Continuous g) (f : α →ₚ[μ, 𝓕] β) : comp g hg f = mk (fun (t : ι) => g ∘ ↑f t) ⋯

theorem MeasureTheory.AEEqProcess.coeFn_comp {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] [TopologicalSpace γ] (g : β → γ) (hg : Continuous g) (f : α →ₚ[μ, 𝓕] β) : ↑(comp g hg f) ≡ᵐ[μ] fun (t : ι) => g ∘ ↑f t

def MeasureTheory.AEEqProcess.pair {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] [TopologicalSpace γ] (f : α →ₚ[μ, 𝓕] β) (g : α →ₚ[μ, 𝓕] γ) : α →ₚ[μ, 𝓕] β × γ

The class of x ↦ (f x, g x).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MeasureTheory.AEEqProcess.pair_mk_mk {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] [TopologicalSpace γ] (f : ι → α → β) (hf : AEStronglyAdapted f 𝓕 μ) (g : ι → α → γ) (hg : AEStronglyAdapted g 𝓕 μ) : (mk f hf).pair (mk g hg) = mk (fun (t : ι) (ω : α) => (f t ω, g t ω)) ⋯

theorem MeasureTheory.AEEqProcess.pair_eq_mk {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] [TopologicalSpace γ] (f : α →ₚ[μ, 𝓕] β) (g : α →ₚ[μ, 𝓕] γ) : f.pair g = mk (fun (t : ι) (ω : α) => (↑f t ω, ↑g t ω)) ⋯

theorem MeasureTheory.AEEqProcess.coeFn_pair {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] [TopologicalSpace γ] (f : α →ₚ[μ, 𝓕] β) (g : α →ₚ[μ, 𝓕] γ) : ↑(f.pair g) ≡ᵐ[μ] fun (t : ι) (ω : α) => (↑f t ω, ↑g t ω)

def MeasureTheory.AEEqProcess.comp₂ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace δ] [TopologicalSpace β] [TopologicalSpace γ] (g : β → γ → δ) (hg : Continuous (Function.uncurry g)) (f₁ : α →ₚ[μ, 𝓕] β) (f₂ : α →ₚ[μ, 𝓕] γ) : α →ₚ[μ, 𝓕] δ

Given a continuous function g : β → γ → δ, and almost everywhere equal functions [f₁] : α →ₚ β and [f₂] : α →ₚ γ, return the equivalence class of the function fun a => g (f₁ a) (f₂ a), i.e., the almost everywhere equal function [fun a => g (f₁ a) (f₂ a)] : α →ₚ γ

Equations

• MeasureTheory.AEEqProcess.comp₂ g hg f₁ f₂ = MeasureTheory.AEEqProcess.comp (Function.uncurry g) hg (f₁.pair f₂)

@[simp]

theorem MeasureTheory.AEEqProcess.comp₂_mk_mk {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace δ] [TopologicalSpace β] [TopologicalSpace γ] (g : β → γ → δ) (hg : Continuous (Function.uncurry g)) (f₁ : ι → α → β) (f₂ : ι → α → γ) (hf₁ : AEStronglyAdapted f₁ 𝓕 μ) (hf₂ : AEStronglyAdapted f₂ 𝓕 μ) : comp₂ g hg (mk f₁ hf₁) (mk f₂ hf₂) = mk (fun (t : ι) (ω : α) => g (f₁ t ω) (f₂ t ω)) ⋯

theorem MeasureTheory.AEEqProcess.comp₂_eq_pair {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace δ] [TopologicalSpace β] [TopologicalSpace γ] (g : β → γ → δ) (hg : Continuous (Function.uncurry g)) (f₁ : α →ₚ[μ, 𝓕] β) (f₂ : α →ₚ[μ, 𝓕] γ) : comp₂ g hg f₁ f₂ = comp (Function.uncurry g) hg (f₁.pair f₂)

theorem MeasureTheory.AEEqProcess.comp₂_eq_mk {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace δ] [TopologicalSpace β] [TopologicalSpace γ] (g : β → γ → δ) (hg : Continuous (Function.uncurry g)) (f₁ : α →ₚ[μ, 𝓕] β) (f₂ : α →ₚ[μ, 𝓕] γ) : comp₂ g hg f₁ f₂ = mk (fun (t : ι) (ω : α) => g (↑f₁ t ω) (↑f₂ t ω)) ⋯

theorem MeasureTheory.AEEqProcess.coeFn_comp₂ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace δ] [TopologicalSpace β] [TopologicalSpace γ] (g : β → γ → δ) (hg : Continuous (Function.uncurry g)) (f₁ : α →ₚ[μ, 𝓕] β) (f₂ : α →ₚ[μ, 𝓕] γ) : ↑(comp₂ g hg f₁ f₂) ≡ᵐ[μ] fun (t : ι) (ω : α) => g (↑f₁ t ω) (↑f₂ t ω)

def MeasureTheory.AEEqProcess.toGerm {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] (f : α →ₚ[μ, 𝓕] β) : (ae μ).Germ (ι → β)

Interpret f : α →ₚ[μ, 𝓕] β as a germ at ae μ forgetting that f is almost everywhere strongly measurable.

Equations

• f.toGerm = Quotient.liftOn' f (fun (f : { X : ι → α → β // MeasureTheory.AEStronglyAdapted X 𝓕 μ }) => ↑fun (ω : α) (t : ι) => ↑f t ω) ⋯

@[simp]

theorem MeasureTheory.AEEqProcess.mk_toGerm {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] (f : ι → α → β) (hf : AEStronglyAdapted f 𝓕 μ) : (mk f hf).toGerm = ↑fun (ω : α) (t : ι) => f t ω

theorem MeasureTheory.AEEqProcess.toGerm_eq {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] (f : α →ₚ[μ, 𝓕] β) : f.toGerm = ↑fun (ω : α) (t : ι) => ↑f t ω

theorem MeasureTheory.AEEqProcess.toGerm_injective {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] : Function.Injective toGerm

theorem MeasureTheory.AEEqProcess.comp_toGerm {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] [TopologicalSpace γ] (g : β → γ) (hg : Continuous g) (f : α →ₚ[μ, 𝓕] β) : (comp g hg f).toGerm = Filter.Germ.map (fun (f : ι → β) (t : ι) => g (f t)) f.toGerm

theorem MeasureTheory.AEEqProcess.comp₂_toGerm {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace δ] [TopologicalSpace β] [TopologicalSpace γ] (g : β → γ → δ) (hg : Continuous (Function.uncurry g)) (f₁ : α →ₚ[μ, 𝓕] β) (f₂ : α →ₚ[μ, 𝓕] γ) : (comp₂ g hg f₁ f₂).toGerm = Filter.Germ.map₂ (fun (f : ι → β) (h : ι → γ) (t : ι) => g (f t) (h t)) f₁.toGerm f₂.toGerm

def MeasureTheory.AEEqProcess.LiftPred {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] (p : (ι → β) → Prop) (f : α →ₚ[μ, 𝓕] β) : Prop

Given a predicate p and an equivalence class [f], return true if p holds of f a for almost all a

Equations

• MeasureTheory.AEEqProcess.LiftPred p f = Filter.Germ.LiftPred p f.toGerm

def MeasureTheory.AEEqProcess.LiftRel {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] [TopologicalSpace γ] (r : (ι → β) → (ι → γ) → Prop) (f : α →ₚ[μ, 𝓕] β) (g : α →ₚ[μ, 𝓕] γ) : Prop

Given a relation r and equivalence class [f] and [g], return true if r holds of (f a, g a) for almost all a

Equations

• MeasureTheory.AEEqProcess.LiftRel r f g = Filter.Germ.LiftRel r f.toGerm g.toGerm

theorem MeasureTheory.AEEqProcess.liftRel_mk_mk {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] [TopologicalSpace γ] {r : (ι → β) → (ι → γ) → Prop} {f : ι → α → β} {g : ι → α → γ} {hf : AEStronglyAdapted f 𝓕 μ} {hg : AEStronglyAdapted g 𝓕 μ} : LiftRel r (mk f hf) (mk g hg) ↔ ∀ᵐ (a : α) ∂μ, r (fun (x : ι) => f x a) fun (x : ι) => g x a

theorem MeasureTheory.AEEqProcess.liftRel_iff_coeFn {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] [TopologicalSpace γ] {r : (ι → β) → (ι → γ) → Prop} {f : α →ₚ[μ, 𝓕] β} {g : α →ₚ[μ, 𝓕] γ} : LiftRel r f g ↔ ∀ᵐ (a : α) ∂μ, r (fun (x : ι) => ↑f x a) fun (x : ι) => ↑g x a

def MeasureTheory.AEEqProcess.const {ι : Type u_1} (α : Type u_2) {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] (b : β) : α →ₚ[μ, 𝓕] β

The equivalence class of a constant function: [fun _ : α => b], based on the equivalence relation of being almost everywhere equal

Equations

• MeasureTheory.AEEqProcess.const α b = MeasureTheory.AEEqProcess.mk (fun (x : ι) (x_1 : α) => b) ⋯

theorem MeasureTheory.AEEqProcess.coeFn_const {ι : Type u_1} (α : Type u_2) {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] (b : β) : ↑(const α b) ≡ᵐ[μ] fun (x : ι) (x_1 : α) => b

@[simp]

theorem MeasureTheory.AEEqProcess.coeFn_const_eq {ι : Type u_1} (α : Type u_2) {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] [NeZero μ] (b : β) (t : ι) (x : α) : ↑(const α b) t x = b

If the measure is nonzero, we can strengthen coeFn_const to get an equality.

theorem MeasureTheory.AEEqProcess.coeFn_const_eq' {ι : Type u_1} (α : Type u_2) {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] (b : β) : ∃ (b' : α → β), ↑(const α b) = fun (x : ι) => b'

@[instance_reducible]

instance MeasureTheory.AEEqProcess.instInhabited {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] [Inhabited β] : Inhabited (α →ₚ[μ, 𝓕] β)

Equations

• MeasureTheory.AEEqProcess.instInhabited = { default := MeasureTheory.AEEqProcess.const α default }

@[instance_reducible]

instance MeasureTheory.AEEqProcess.instOne {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] [One β] : One (α →ₚ[μ, 𝓕] β)

Equations

• MeasureTheory.AEEqProcess.instOne = { one := MeasureTheory.AEEqProcess.const α 1 }

@[instance_reducible]

instance MeasureTheory.AEEqProcess.instZero {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] [Zero β] : Zero (α →ₚ[μ, 𝓕] β)

Equations

• MeasureTheory.AEEqProcess.instZero = { zero := MeasureTheory.AEEqProcess.const α 0 }

theorem MeasureTheory.AEEqProcess.one_def {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] [One β] : 1 = mk (fun (x : ι) (x_1 : α) => 1) ⋯

theorem MeasureTheory.AEEqProcess.zero_def {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] [Zero β] : 0 = mk (fun (x : ι) (x_1 : α) => 0) ⋯

theorem MeasureTheory.AEEqProcess.coeFn_one {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] [One β] : ↑1 ≡ᵐ[μ] 1

theorem MeasureTheory.AEEqProcess.coeFn_zero {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] [Zero β] : ↑0 ≡ᵐ[μ] 0

@[simp]

theorem MeasureTheory.AEEqProcess.coeFn_one_eq {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] [NeZero μ] [One β] {t : ι} {x : α} : ↑1 t x = 1

@[simp]

theorem MeasureTheory.AEEqProcess.coeFn_zero_eq {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] [NeZero μ] [Zero β] {t : ι} {x : α} : ↑0 t x = 0

@[simp]

theorem MeasureTheory.AEEqProcess.one_toGerm {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] [One β] : toGerm 1 = 1

@[simp]

theorem MeasureTheory.AEEqProcess.zero_toGerm {ι : Type u_1} {α : Type u_2} {β : Type u_3} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace β] [Zero β] : toGerm 0 = 0

@[instance_reducible]

instance MeasureTheory.AEEqProcess.instSMul {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] {𝕜 : Type u_6} [SMul 𝕜 γ] [ContinuousConstSMul 𝕜 γ] : SMul 𝕜 (α →ₚ[μ, 𝓕] γ)

Equations

• MeasureTheory.AEEqProcess.instSMul = { smul := fun (c : 𝕜) (f : α →ₚ[μ, 𝓕] γ) => MeasureTheory.AEEqProcess.comp (fun (x : γ) => c • x) ⋯ f }

@[simp]

theorem MeasureTheory.AEEqProcess.smul_mk {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] {𝕜 : Type u_6} [SMul 𝕜 γ] [ContinuousConstSMul 𝕜 γ] (c : 𝕜) (f : ι → α → γ) (hf : AEStronglyAdapted f 𝓕 μ) : c • mk f hf = mk (c • f) ⋯

theorem MeasureTheory.AEEqProcess.coeFn_smul {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] {𝕜 : Type u_6} [SMul 𝕜 γ] [ContinuousConstSMul 𝕜 γ] (c : 𝕜) (f : α →ₚ[μ, 𝓕] γ) : ↑(c • f) ≡ᵐ[μ] c • ↑f

theorem MeasureTheory.AEEqProcess.smul_toGerm {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] {𝕜 : Type u_6} [SMul 𝕜 γ] [ContinuousConstSMul 𝕜 γ] (c : 𝕜) (f : α →ₚ[μ, 𝓕] γ) : (c • f).toGerm = c • f.toGerm

instance MeasureTheory.AEEqProcess.instSMulCommClass {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] {𝕜 : Type u_6} {𝕜' : Type u_7} [SMul 𝕜 γ] [ContinuousConstSMul 𝕜 γ] [SMul 𝕜' γ] [ContinuousConstSMul 𝕜' γ] [SMulCommClass 𝕜 𝕜' γ] : SMulCommClass 𝕜 𝕜' (α →ₚ[μ, 𝓕] γ)

instance MeasureTheory.AEEqProcess.instIsScalarTower {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] {𝕜 : Type u_6} {𝕜' : Type u_7} [SMul 𝕜 γ] [ContinuousConstSMul 𝕜 γ] [SMul 𝕜' γ] [ContinuousConstSMul 𝕜' γ] [SMul 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' γ] : IsScalarTower 𝕜 𝕜' (α →ₚ[μ, 𝓕] γ)

instance MeasureTheory.AEEqProcess.instIsCentralScalar {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] {𝕜 : Type u_6} [SMul 𝕜 γ] [ContinuousConstSMul 𝕜 γ] [SMul 𝕜ᵐᵒᵖ γ] [IsCentralScalar 𝕜 γ] : IsCentralScalar 𝕜 (α →ₚ[μ, 𝓕] γ)

@[instance_reducible]

instance MeasureTheory.AEEqProcess.instMul {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [Mul γ] [ContinuousMul γ] : Mul (α →ₚ[μ, 𝓕] γ)

Equations

• MeasureTheory.AEEqProcess.instMul = { mul := MeasureTheory.AEEqProcess.comp₂ (fun (x1 x2 : γ) => x1 * x2) ⋯ }

@[instance_reducible]

instance MeasureTheory.AEEqProcess.instAdd {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [Add γ] [ContinuousAdd γ] : Add (α →ₚ[μ, 𝓕] γ)

Equations

• MeasureTheory.AEEqProcess.instAdd = { add := MeasureTheory.AEEqProcess.comp₂ (fun (x1 x2 : γ) => x1 + x2) ⋯ }

@[simp]

theorem MeasureTheory.AEEqProcess.mk_mul_mk {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [Mul γ] [ContinuousMul γ] (f g : ι → α → γ) (hf : AEStronglyAdapted f 𝓕 μ) (hg : AEStronglyAdapted g 𝓕 μ) : mk f hf * mk g hg = mk (f * g) ⋯

@[simp]

theorem MeasureTheory.AEEqProcess.mk_add_mk {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [Add γ] [ContinuousAdd γ] (f g : ι → α → γ) (hf : AEStronglyAdapted f 𝓕 μ) (hg : AEStronglyAdapted g 𝓕 μ) : mk f hf + mk g hg = mk (f + g) ⋯

theorem MeasureTheory.AEEqProcess.coeFn_mul {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [Mul γ] [ContinuousMul γ] (f g : α →ₚ[μ, 𝓕] γ) : ↑(f * g) ≡ᵐ[μ] ↑f * ↑g

theorem MeasureTheory.AEEqProcess.coeFn_add {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [Add γ] [ContinuousAdd γ] (f g : α →ₚ[μ, 𝓕] γ) : ↑(f + g) ≡ᵐ[μ] ↑f + ↑g

@[simp]

theorem MeasureTheory.AEEqProcess.mul_toGerm {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [Mul γ] [ContinuousMul γ] (f g : α →ₚ[μ, 𝓕] γ) : (f * g).toGerm = f.toGerm * g.toGerm

@[simp]

theorem MeasureTheory.AEEqProcess.add_toGerm {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [Add γ] [ContinuousAdd γ] (f g : α →ₚ[μ, 𝓕] γ) : (f + g).toGerm = f.toGerm + g.toGerm

@[instance_reducible]

instance MeasureTheory.AEEqProcess.instAddMonoid {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [AddMonoid γ] [ContinuousAdd γ] : AddMonoid (α →ₚ[μ, 𝓕] γ)

Equations

• MeasureTheory.AEEqProcess.instAddMonoid = Function.Injective.addMonoid MeasureTheory.AEEqProcess.toGerm ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

instance MeasureTheory.AEEqProcess.instAddCommMonoid {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [AddCommMonoid γ] [ContinuousAdd γ] : AddCommMonoid (α →ₚ[μ, 𝓕] γ)

Equations

• MeasureTheory.AEEqProcess.instAddCommMonoid = Function.Injective.addCommMonoid MeasureTheory.AEEqProcess.toGerm ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

instance MeasureTheory.AEEqProcess.instPowNat {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [Monoid γ] [ContinuousMul γ] : Pow (α →ₚ[μ, 𝓕] γ) ℕ

Equations

• MeasureTheory.AEEqProcess.instPowNat = { pow := fun (f : α →ₚ[μ, 𝓕] γ) (n : ℕ) => MeasureTheory.AEEqProcess.comp (fun (a : γ) => a ^ n) ⋯ f }

@[simp]

theorem MeasureTheory.AEEqProcess.mk_pow {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [Monoid γ] [ContinuousMul γ] (f : ι → α → γ) (hf : AEStronglyAdapted f 𝓕 μ) (n : ℕ) : mk f hf ^ n = mk (f ^ n) ⋯

theorem MeasureTheory.AEEqProcess.coeFn_pow {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [Monoid γ] [ContinuousMul γ] (f : α →ₚ[μ, 𝓕] γ) (n : ℕ) : ↑(f ^ n) ≡ᵐ[μ] ↑f ^ n

@[simp]

theorem MeasureTheory.AEEqProcess.pow_toGerm {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [Monoid γ] [ContinuousMul γ] (f : α →ₚ[μ, 𝓕] γ) (n : ℕ) : (f ^ n).toGerm = f.toGerm ^ n

@[instance_reducible]

instance MeasureTheory.AEEqProcess.instMonoid {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [Monoid γ] [ContinuousMul γ] : Monoid (α →ₚ[μ, 𝓕] γ)

Equations

• MeasureTheory.AEEqProcess.instMonoid = Function.Injective.monoid MeasureTheory.AEEqProcess.toGerm ⋯ ⋯ ⋯ ⋯

def MeasureTheory.AEEqProcess.toGermMonoidHom {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [Monoid γ] [ContinuousMul γ] : (α →ₚ[μ, 𝓕] γ) →* (ae μ).Germ (ι → γ)

AEEqProcess.toGerm as a MonoidHom.

Equations

• MeasureTheory.AEEqProcess.toGermMonoidHom = { toFun := MeasureTheory.AEEqProcess.toGerm, map_one' := ⋯, map_mul' := ⋯ }

def MeasureTheory.AEEqProcess.toGermAddMonoidHom {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [AddMonoid γ] [ContinuousAdd γ] : (α →ₚ[μ, 𝓕] γ) →+ (ae μ).Germ (ι → γ)

AEEqProcess.toGerm as an AddMonoidHom.

Equations

• MeasureTheory.AEEqProcess.toGermAddMonoidHom = { toFun := MeasureTheory.AEEqProcess.toGerm, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem MeasureTheory.AEEqProcess.toGermAddMonoidHom_apply {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [AddMonoid γ] [ContinuousAdd γ] (f : α →ₚ[μ, 𝓕] γ) : toGermAddMonoidHom f = f.toGerm

@[simp]

theorem MeasureTheory.AEEqProcess.toGermMonoidHom_apply {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [Monoid γ] [ContinuousMul γ] (f : α →ₚ[μ, 𝓕] γ) : toGermMonoidHom f = f.toGerm

@[instance_reducible]

instance MeasureTheory.AEEqProcess.instCommMonoid {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [CommMonoid γ] [ContinuousMul γ] : CommMonoid (α →ₚ[μ, 𝓕] γ)

Equations

• MeasureTheory.AEEqProcess.instCommMonoid = Function.Injective.commMonoid MeasureTheory.AEEqProcess.toGerm ⋯ ⋯ ⋯ ⋯

theorem MeasureTheory.AEEqProcess.coeFn_finsetProd {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [CommMonoid γ] [ContinuousMul γ] {η : Type u_6} (s : Finset η) (f : η → α →ₚ[μ, 𝓕] γ) : ↑(∏ i ∈ s, f i) ≡ᵐ[μ] ∏ i ∈ s, ↑(f i)

theorem MeasureTheory.AEEqProcess.coeFn_finsetSum {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [AddCommMonoid γ] [ContinuousAdd γ] {η : Type u_6} (s : Finset η) (f : η → α →ₚ[μ, 𝓕] γ) : ↑(∑ i ∈ s, f i) ≡ᵐ[μ] ∑ i ∈ s, ↑(f i)

theorem MeasureTheory.AEEqProcess.coeFn_fun_finsetProd {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [CommMonoid γ] [ContinuousMul γ] {ι✝ : Type u_6} (s : Finset ι✝) (f : ι✝ → α →ₚ[μ, 𝓕] γ) : ↑(∏ i ∈ s, f i) ≡ᵐ[μ] fun (x : ι) => ∏ i ∈ s, ↑(f i) x

theorem MeasureTheory.AEEqProcess.coeFn_fun_finsetSum {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [AddCommMonoid γ] [ContinuousAdd γ] {ι✝ : Type u_6} (s : Finset ι✝) (f : ι✝ → α →ₚ[μ, 𝓕] γ) : ↑(∑ i ∈ s, f i) ≡ᵐ[μ] fun (x : ι) => ∑ i ∈ s, ↑(f i) x

@[instance_reducible]

instance MeasureTheory.AEEqProcess.instInv {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [Group γ] [IsTopologicalGroup γ] : Inv (α →ₚ[μ, 𝓕] γ)

Equations

• MeasureTheory.AEEqProcess.instInv = { inv := MeasureTheory.AEEqProcess.comp Inv.inv ⋯ }

@[instance_reducible]

instance MeasureTheory.AEEqProcess.instNeg {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [AddGroup γ] [IsTopologicalAddGroup γ] : Neg (α →ₚ[μ, 𝓕] γ)

Equations

• MeasureTheory.AEEqProcess.instNeg = { neg := MeasureTheory.AEEqProcess.comp Neg.neg ⋯ }

@[simp]

theorem MeasureTheory.AEEqProcess.inv_mk {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [Group γ] [IsTopologicalGroup γ] (f : ι → α → γ) (hf : AEStronglyAdapted f 𝓕 μ) : (mk f hf)⁻¹ = mk f⁻¹ ⋯

@[simp]

theorem MeasureTheory.AEEqProcess.neg_mk {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [AddGroup γ] [IsTopologicalAddGroup γ] (f : ι → α → γ) (hf : AEStronglyAdapted f 𝓕 μ) : -mk f hf = mk (-f) ⋯

theorem MeasureTheory.AEEqProcess.coeFn_inv {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [Group γ] [IsTopologicalGroup γ] (f : α →ₚ[μ, 𝓕] γ) : ↑f⁻¹ ≡ᵐ[μ] (↑f)⁻¹

theorem MeasureTheory.AEEqProcess.coeFn_neg {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [AddGroup γ] [IsTopologicalAddGroup γ] (f : α →ₚ[μ, 𝓕] γ) : ↑(-f) ≡ᵐ[μ] -↑f

theorem MeasureTheory.AEEqProcess.inv_toGerm {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [Group γ] [IsTopologicalGroup γ] (f : α →ₚ[μ, 𝓕] γ) : f⁻¹.toGerm = f.toGerm⁻¹

theorem MeasureTheory.AEEqProcess.neg_toGerm {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [AddGroup γ] [IsTopologicalAddGroup γ] (f : α →ₚ[μ, 𝓕] γ) : (-f).toGerm = -f.toGerm

@[instance_reducible]

instance MeasureTheory.AEEqProcess.instDiv {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [Group γ] [IsTopologicalGroup γ] : Div (α →ₚ[μ, 𝓕] γ)

Equations

• MeasureTheory.AEEqProcess.instDiv = { div := MeasureTheory.AEEqProcess.comp₂ Div.div ⋯ }

@[instance_reducible]

instance MeasureTheory.AEEqProcess.instSub {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [AddGroup γ] [IsTopologicalAddGroup γ] : Sub (α →ₚ[μ, 𝓕] γ)

Equations

• MeasureTheory.AEEqProcess.instSub = { sub := MeasureTheory.AEEqProcess.comp₂ Sub.sub ⋯ }

@[simp]

theorem MeasureTheory.AEEqProcess.mk_div {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [Group γ] [IsTopologicalGroup γ] (f g : ι → α → γ) (hf : AEStronglyAdapted f 𝓕 μ) (hg : AEStronglyAdapted g 𝓕 μ) : mk (f / g) ⋯ = mk f hf / mk g hg

@[simp]

theorem MeasureTheory.AEEqProcess.mk_sub {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [AddGroup γ] [IsTopologicalAddGroup γ] (f g : ι → α → γ) (hf : AEStronglyAdapted f 𝓕 μ) (hg : AEStronglyAdapted g 𝓕 μ) : mk (f - g) ⋯ = mk f hf - mk g hg

theorem MeasureTheory.AEEqProcess.coeFn_div {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [Group γ] [IsTopologicalGroup γ] (f g : α →ₚ[μ, 𝓕] γ) : ↑(f / g) ≡ᵐ[μ] ↑f / ↑g

theorem MeasureTheory.AEEqProcess.coeFn_sub {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [AddGroup γ] [IsTopologicalAddGroup γ] (f g : α →ₚ[μ, 𝓕] γ) : ↑(f - g) ≡ᵐ[μ] ↑f - ↑g

theorem MeasureTheory.AEEqProcess.div_toGerm {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [Group γ] [IsTopologicalGroup γ] (f g : α →ₚ[μ, 𝓕] γ) : (f / g).toGerm = f.toGerm / g.toGerm

theorem MeasureTheory.AEEqProcess.sub_toGerm {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [AddGroup γ] [IsTopologicalAddGroup γ] (f g : α →ₚ[μ, 𝓕] γ) : (f - g).toGerm = f.toGerm - g.toGerm

@[instance_reducible]

instance MeasureTheory.AEEqProcess.instPowInt {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [Group γ] [IsTopologicalGroup γ] : Pow (α →ₚ[μ, 𝓕] γ) ℤ

Equations

• MeasureTheory.AEEqProcess.instPowInt = { pow := fun (f : α →ₚ[μ, 𝓕] γ) (n : ℤ) => MeasureTheory.AEEqProcess.comp (fun (a : γ) => a ^ n) ⋯ f }

@[simp]

theorem MeasureTheory.AEEqProcess.mk_zpow {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [Group γ] [IsTopologicalGroup γ] (f : ι → α → γ) (hf : AEStronglyAdapted f 𝓕 μ) (n : ℤ) : mk f hf ^ n = mk (f ^ n) ⋯

theorem MeasureTheory.AEEqProcess.coeFn_zpow {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [Group γ] [IsTopologicalGroup γ] (f : α →ₚ[μ, 𝓕] γ) (n : ℤ) : ↑(f ^ n) ≡ᵐ[μ] ↑f ^ n

@[simp]

theorem MeasureTheory.AEEqProcess.zpow_toGerm {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [Group γ] [IsTopologicalGroup γ] (f : α →ₚ[μ, 𝓕] γ) (n : ℤ) : (f ^ n).toGerm = f.toGerm ^ n

@[instance_reducible]

instance MeasureTheory.AEEqProcess.instAddGroup {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [AddGroup γ] [IsTopologicalAddGroup γ] : AddGroup (α →ₚ[μ, 𝓕] γ)

Equations

• MeasureTheory.AEEqProcess.instAddGroup = Function.Injective.addGroup MeasureTheory.AEEqProcess.toGerm ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

instance MeasureTheory.AEEqProcess.instAddCommGroup {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [AddCommGroup γ] [IsTopologicalAddGroup γ] : AddCommGroup (α →ₚ[μ, 𝓕] γ)

Equations

• MeasureTheory.AEEqProcess.instAddCommGroup = { toAddGroup := MeasureTheory.AEEqProcess.instAddGroup, add_comm := ⋯ }

@[instance_reducible]

instance MeasureTheory.AEEqProcess.instGroup {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [Group γ] [IsTopologicalGroup γ] : Group (α →ₚ[μ, 𝓕] γ)

Equations

• MeasureTheory.AEEqProcess.instGroup = Function.Injective.group MeasureTheory.AEEqProcess.toGerm ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

instance MeasureTheory.AEEqProcess.instCommGroup {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] [CommGroup γ] [IsTopologicalGroup γ] : CommGroup (α →ₚ[μ, 𝓕] γ)

Equations

• MeasureTheory.AEEqProcess.instCommGroup = { toGroup := MeasureTheory.AEEqProcess.instGroup, mul_comm := ⋯ }

@[instance_reducible]

instance MeasureTheory.AEEqProcess.instMulAction {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] {𝕜 : Type u_6} [Monoid 𝕜] [MulAction 𝕜 γ] [ContinuousConstSMul 𝕜 γ] : MulAction 𝕜 (α →ₚ[μ, 𝓕] γ)

Equations

• MeasureTheory.AEEqProcess.instMulAction = Function.Injective.mulAction MeasureTheory.AEEqProcess.toGerm ⋯ ⋯

@[instance_reducible]

instance MeasureTheory.AEEqProcess.instDistribMulAction {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] {𝕜 : Type u_6} [Monoid 𝕜] [AddMonoid γ] [ContinuousAdd γ] [DistribMulAction 𝕜 γ] [ContinuousConstSMul 𝕜 γ] : DistribMulAction 𝕜 (α →ₚ[μ, 𝓕] γ)

Equations

• MeasureTheory.AEEqProcess.instDistribMulAction = Function.Injective.distribMulAction MeasureTheory.AEEqProcess.toGermAddMonoidHom ⋯ ⋯

@[instance_reducible]

instance MeasureTheory.AEEqProcess.instModule {ι : Type u_1} {α : Type u_2} {γ : Type u_4} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} [TopologicalSpace γ] {𝕜 : Type u_6} [Semiring 𝕜] [AddCommMonoid γ] [ContinuousAdd γ] [Module 𝕜 γ] [ContinuousConstSMul 𝕜 γ] : Module 𝕜 (α →ₚ[μ, 𝓕] γ)

Equations

• MeasureTheory.AEEqProcess.instModule = Function.Injective.module 𝕜 MeasureTheory.AEEqProcess.toGermAddMonoidHom ⋯ ⋯

@[instance_reducible]

instance MeasureTheory.AEEqProcess.instStarOfContinuousStar {ι : Type u_1} {α : Type u_2} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} {R : Type u_6} [TopologicalSpace R] [Star R] [ContinuousStar R] : Star (α →ₚ[μ, 𝓕] R)

Equations

• MeasureTheory.AEEqProcess.instStarOfContinuousStar = { star := fun (f : α →ₚ[μ, 𝓕] R) => MeasureTheory.AEEqProcess.comp star ⋯ f }

theorem MeasureTheory.AEEqProcess.coeFn_star {ι : Type u_1} {α : Type u_2} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} {R : Type u_6} [TopologicalSpace R] [Star R] [ContinuousStar R] (f : α →ₚ[μ, 𝓕] R) : ↑(star f) ≡ᵐ[μ] star ↑f

@[instance_reducible]

instance MeasureTheory.AEEqProcess.instInvolutiveStarOfContinuousStar {ι : Type u_1} {α : Type u_2} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} {R : Type u_6} [TopologicalSpace R] [InvolutiveStar R] [ContinuousStar R] : InvolutiveStar (α →ₚ[μ, 𝓕] R)

Equations

• MeasureTheory.AEEqProcess.instInvolutiveStarOfContinuousStar = { toStar := MeasureTheory.AEEqProcess.instStarOfContinuousStar, star_involutive := ⋯ }

instance MeasureTheory.AEEqProcess.instTrivialStar {ι : Type u_1} {α : Type u_2} {mα : MeasurableSpace α} {μ : Measure α} [Preorder ι] {𝓕 : Filtration ι mα} {R : Type u_6} [TopologicalSpace R] [Star R] [TrivialStar R] [ContinuousStar R] : TrivialStar (α →ₚ[μ, 𝓕] R)