feat(measure_theory/lattice): define typeclasses for measurability of lattice operations, define a lattice on ae_eq_fun (#10591)

As was previously done for measurability of arithmetic operations, I define typeclasses for the measurability of sup and inf in a lattice. In the borel_space file, instances of these are provided when the lattice operations are continuous.
Finally I've put a lattice structure on `ae_eq_fun`.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Author: RemyDegenne

src/analysis/normed_space/lattice_ordered_group.lean

@@ -147,6 +147,12 @@ begin
   simp,
 end
 
+@[priority 100] -- see Note [lower instance priority]
+instance normed_lattice_add_comm_group_has_continuous_sup {α : Type*}
+  [normed_lattice_add_comm_group α] :
+  has_continuous_sup α :=
+order_dual.has_continuous_sup (order_dual α)
+
 /--
 Let `α` be a normed lattice ordered group. Then `α` is a topological lattice in the norm topology.
 -/

src/measure_theory/constructions/borel_space.lean

@@ -7,11 +7,13 @@ import measure_theory.function.ae_measurable_sequence
 import analysis.complex.basic
 import analysis.normed_space.finite_dimension
 import measure_theory.group.arithmetic
+import measure_theory.lattice
 import topology.algebra.ordered.liminf_limsup
 import topology.continuous_function.basic
 import topology.instances.ereal
 import topology.G_delta
 import topology.semicontinuous
+import topology.order.lattice
 
 /-!
 # Borel (measurable) space
@@ -167,6 +169,18 @@ the `σ`-algebra of measurable sets is exactly the `σ`-algebra generated by ope
 class borel_space (α : Type*) [topological_space α] [measurable_space α] : Prop :=
 (measurable_eq : ‹measurable_space α› = borel α)
 
+@[priority 100]
+instance order_dual.opens_measurable_space {α : Type*} [topological_space α] [measurable_space α]
+  [h : opens_measurable_space α] :
+  opens_measurable_space (order_dual α) :=
+{ borel_le := h.borel_le }
+
+@[priority 100]
+instance order_dual.borel_space {α : Type*} [topological_space α] [measurable_space α]
+  [h : borel_space α] :
+  borel_space (order_dual α) :=
+{ measurable_eq := h.measurable_eq }
+
 /-- In a `borel_space` all open sets are measurable. -/
 @[priority 100]
 instance borel_space.opens_measurable {α : Type*} [topological_space α] [measurable_space α]
@@ -705,6 +719,34 @@ instance has_continuous_smul.has_measurable_smul {M α} [topological_space M]
 ⟨λ c, (continuous_const.smul continuous_id).measurable,
   λ y, (continuous_id.smul continuous_const).measurable⟩
 
+section lattice
+
+@[priority 100]
+instance has_continuous_sup.has_measurable_sup [has_sup γ] [has_continuous_sup γ] :
+  has_measurable_sup γ :=
+{ measurable_const_sup := λ c, (continuous_const.sup continuous_id).measurable,
+  measurable_sup_const := λ c, (continuous_id.sup continuous_const).measurable }
+
+@[priority 100]
+instance has_continuous_sup.has_measurable_sup₂ [second_countable_topology γ] [has_sup γ]
+  [has_continuous_sup γ] :
+  has_measurable_sup₂ γ :=
+⟨continuous_sup.measurable⟩
+
+@[priority 100]
+instance has_continuous_inf.has_measurable_inf [has_inf γ] [has_continuous_inf γ] :
+  has_measurable_inf γ :=
+{ measurable_const_inf := λ c, (continuous_const.inf continuous_id).measurable,
+  measurable_inf_const := λ c, (continuous_id.inf continuous_const).measurable }
+
+@[priority 100]
+instance has_continuous_inf.has_measurable_inf₂ [second_countable_topology γ] [has_inf γ]
+  [has_continuous_inf γ] :
+  has_measurable_inf₂ γ :=
+⟨continuous_inf.measurable⟩
+
+end lattice
+
 section homeomorph
 
 @[measurability] protected lemma homeomorph.measurable (h : α ≃ₜ γ) : measurable h :=

src/measure_theory/function/ae_eq_fun.lean

@@ -277,12 +277,68 @@ lift_rel_iff_coe_fn.symm
 instance [partial_order β] : partial_order (α →ₘ[μ] β) :=
 partial_order.lift to_germ to_germ_injective
 
-/- TODO: Prove `L⁰` space is a lattice if β is linear order.
-         What if β is only a lattice? -/
+section lattice
 
--- instance [linear_order β] : semilattice_sup (α →ₘ β) :=
--- { sup := comp₂ (⊔) (_),
---    .. ae_eq_fun.partial_order }
+section sup
+variables [semilattice_sup β] [has_measurable_sup₂ β]
+
+instance : has_sup (α →ₘ[μ] β) := { sup := λ f g, ae_eq_fun.comp₂ (⊔) measurable_sup f g }
+
+lemma coe_fn_sup (f g : α →ₘ[μ] β) : ⇑(f ⊔ g) =ᵐ[μ] λ x, f x ⊔ g x := coe_fn_comp₂ _ _ _ _
+
+protected lemma le_sup_left (f g : α →ₘ[μ] β) : f ≤ f ⊔ g :=
+by { rw ← coe_fn_le, filter_upwards [coe_fn_sup f g], intros a ha,  rw ha, exact le_sup_left, }
+
+protected lemma le_sup_right (f g : α →ₘ[μ] β) : g ≤ f ⊔ g :=
+by { rw ← coe_fn_le, filter_upwards [coe_fn_sup f g], intros a ha,  rw ha, exact le_sup_right, }
+
+protected lemma sup_le (f g f' : α →ₘ[μ] β) (hf : f ≤ f') (hg : g ≤ f') : f ⊔ g ≤ f' :=
+begin
+  rw ← coe_fn_le at hf hg ⊢,
+  filter_upwards [hf, hg, coe_fn_sup f g],
+  intros a haf hag ha_sup,
+  rw ha_sup,
+  exact sup_le haf hag,
+end
+
+end sup
+
+section inf
+variables [semilattice_inf β] [has_measurable_inf₂ β]
+
+instance : has_inf (α →ₘ[μ] β) := { inf := λ f g, ae_eq_fun.comp₂ (⊓) measurable_inf f g }
+
+lemma coe_fn_inf (f g : α →ₘ[μ] β) : ⇑(f ⊓ g) =ᵐ[μ] λ x, f x ⊓ g x := coe_fn_comp₂ _ _ _ _
+
+protected lemma inf_le_left (f g : α →ₘ[μ] β) : f ⊓ g ≤ f :=
+by { rw ← coe_fn_le, filter_upwards [coe_fn_inf f g], intros a ha,  rw ha, exact inf_le_left, }
+
+protected lemma inf_le_right (f g : α →ₘ[μ] β) : f ⊓ g ≤ g :=
+by { rw ← coe_fn_le, filter_upwards [coe_fn_inf f g], intros a ha,  rw ha, exact inf_le_right, }
+
+protected lemma le_inf (f' f g : α →ₘ[μ] β) (hf : f' ≤ f) (hg : f' ≤ g) : f' ≤ f ⊓ g :=
+begin
+  rw ← coe_fn_le at hf hg ⊢,
+  filter_upwards [hf, hg, coe_fn_inf f g],
+  intros a haf hag ha_inf,
+  rw ha_inf,
+  exact le_inf haf hag,
+end
+
+end inf
+
+instance [lattice β] [has_measurable_sup₂ β] [has_measurable_inf₂ β] : lattice (α →ₘ[μ] β) :=
+{ sup           := has_sup.sup,
+  le_sup_left   := ae_eq_fun.le_sup_left,
+  le_sup_right  := ae_eq_fun.le_sup_right,
+  sup_le        := ae_eq_fun.sup_le,
+  inf           := has_inf.inf,
+  inf_le_left   := ae_eq_fun.inf_le_left,
+  inf_le_right  := ae_eq_fun.inf_le_right,
+  le_inf        := ae_eq_fun.le_inf,
+  ..ae_eq_fun.partial_order}
+
+end lattice
 
 end order
 

src/measure_theory/lattice.lean

@@ -0,0 +1,203 @@
+/-
+Copyright (c) 2021 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+
+import measure_theory.measure.measure_space
+
+/-!
+# Typeclasses for measurability of lattice operations
+
+In this file we define classes `has_measurable_sup` and `has_measurable_inf` and prove dot-style
+lemmas (`measurable.sup`, `ae_measurable.sup` etc). For binary operations we define two typeclasses:
+
+- `has_measurable_sup` says that both left and right sup are measurable;
+- `has_measurable_sup₂` says that `λ p : α × α, p.1 ⊔ p.2` is measurable,
+
+and similarly for other binary operations. The reason for introducing these classes is that in case
+of topological space `α` equipped with the Borel `σ`-algebra, instances for `has_measurable_sup₂`
+etc require `α` to have a second countable topology.
+
+For instances relating, e.g., `has_continuous_sup` to `has_measurable_sup` see file
+`measure_theory.borel_space`.
+
+## Tags
+
+measurable function, lattice operation
+
+-/
+
+open measure_theory
+
+/-- We say that a type `has_measurable_sup` if `((⊔) c)` and `(⊔ c)` are measurable functions.
+For a typeclass assuming measurability of `uncurry (⊔)` see `has_measurable_sup₂`. -/
+class has_measurable_sup (M : Type*) [measurable_space M] [has_sup M] : Prop :=
+(measurable_const_sup : ∀ c : M, measurable ((⊔) c))
+(measurable_sup_const : ∀ c : M, measurable (⊔ c))
+
+/-- We say that a type `has_measurable_sup₂` if `uncurry (⊔)` is a measurable functions.
+For a typeclass assuming measurability of `((⊔) c)` and `(⊔ c)` see `has_measurable_sup`. -/
+class has_measurable_sup₂ (M : Type*) [measurable_space M] [has_sup M] : Prop :=
+(measurable_sup : measurable (λ p : M × M, p.1 ⊔ p.2))
+
+export has_measurable_sup₂ (measurable_sup)
+  has_measurable_sup (measurable_const_sup measurable_sup_const)
+
+/-- We say that a type `has_measurable_inf` if `((⊓) c)` and `(⊓ c)` are measurable functions.
+For a typeclass assuming measurability of `uncurry (⊓)` see `has_measurable_inf₂`. -/
+class has_measurable_inf (M : Type*) [measurable_space M] [has_inf M] : Prop :=
+(measurable_const_inf : ∀ c : M, measurable ((⊓) c))
+(measurable_inf_const : ∀ c : M, measurable (⊓ c))
+
+/-- We say that a type `has_measurable_inf₂` if `uncurry (⊔)` is a measurable functions.
+For a typeclass assuming measurability of `((⊔) c)` and `(⊔ c)` see `has_measurable_inf`. -/
+class has_measurable_inf₂ (M : Type*) [measurable_space M] [has_inf M] : Prop :=
+(measurable_inf : measurable (λ p : M × M, p.1 ⊓ p.2))
+
+export has_measurable_inf₂ (measurable_inf)
+  has_measurable_inf (measurable_const_inf measurable_inf_const)
+
+variables {M : Type*} [measurable_space M]
+
+section order_dual
+
+@[priority 100]
+instance order_dual.has_measurable_sup [has_inf M] [has_measurable_inf M] :
+  has_measurable_sup (order_dual M) :=
+⟨@measurable_const_inf M _ _ _, @measurable_inf_const M _ _ _⟩
+
+@[priority 100]
+instance order_dual.has_measurable_inf [has_sup M] [has_measurable_sup M] :
+  has_measurable_inf (order_dual M) :=
+⟨@measurable_const_sup M _ _ _, @measurable_sup_const M _ _ _⟩
+
+@[priority 100]
+instance order_dual.has_measurable_sup₂ [has_inf M] [has_measurable_inf₂ M] :
+  has_measurable_sup₂ (order_dual M) :=
+⟨@measurable_inf M _ _ _⟩
+
+@[priority 100]
+instance order_dual.has_measurable_inf₂ [has_sup M] [has_measurable_sup₂ M] :
+  has_measurable_inf₂ (order_dual M) :=
+⟨@measurable_sup M _ _ _⟩
+
+end order_dual
+
+variables {α : Type*} {m : measurable_space α} {μ : measure α} {f g : α → M}
+include m
+
+section sup
+variables [has_sup M]
+
+section measurable_sup
+variables [has_measurable_sup M]
+
+@[measurability]
+lemma measurable.const_sup (hf : measurable f) (c : M) : measurable (λ x, c ⊔ f x) :=
+(measurable_const_sup c).comp hf
+
+@[measurability]
+lemma ae_measurable.const_sup (hf : ae_measurable f μ) (c : M) : ae_measurable (λ x, c ⊔ f x) μ :=
+(has_measurable_sup.measurable_const_sup c).comp_ae_measurable hf
+
+@[measurability]
+lemma measurable.sup_const (hf : measurable f) (c : M) : measurable (λ x, f x ⊔ c) :=
+(measurable_sup_const c).comp hf
+
+@[measurability]
+lemma ae_measurable.sup_const (hf : ae_measurable f μ) (c : M) :
+  ae_measurable (λ x, f x ⊔ c) μ :=
+(measurable_sup_const c).comp_ae_measurable hf
+
+end measurable_sup
+
+section measurable_sup₂
+variables [has_measurable_sup₂ M]
+
+@[measurability]
+lemma measurable.sup' (hf : measurable f) (hg : measurable g) : measurable (f ⊔ g) :=
+measurable_sup.comp (hf.prod_mk hg)
+
+@[measurability]
+lemma measurable.sup (hf : measurable f) (hg : measurable g) : measurable (λ a, f a ⊔ g a) :=
+measurable_sup.comp (hf.prod_mk hg)
+
+@[measurability]
+lemma ae_measurable.sup' (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
+  ae_measurable (f ⊔ g) μ :=
+measurable_sup.comp_ae_measurable (hf.prod_mk hg)
+
+@[measurability]
+lemma ae_measurable.sup (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
+  ae_measurable (λ a, f a ⊔ g a) μ :=
+measurable_sup.comp_ae_measurable (hf.prod_mk hg)
+
+omit m
+@[priority 100]
+instance has_measurable_sup₂.to_has_measurable_sup : has_measurable_sup M :=
+⟨λ c, measurable_const.sup measurable_id, λ c, measurable_id.sup measurable_const⟩
+include m
+
+end measurable_sup₂
+
+end sup
+
+section inf
+variables [has_inf M]
+
+section measurable_inf
+variables [has_measurable_inf M]
+
+@[measurability]
+lemma measurable.const_inf (hf : measurable f) (c : M) :
+  measurable (λ x, c ⊓ f x) :=
+(measurable_const_inf c).comp hf
+
+@[measurability]
+lemma ae_measurable.const_inf (hf : ae_measurable f μ) (c : M) :
+  ae_measurable (λ x, c ⊓ f x) μ :=
+(has_measurable_inf.measurable_const_inf c).comp_ae_measurable hf
+
+@[measurability]
+lemma measurable.inf_const (hf : measurable f) (c : M) :
+  measurable (λ x, f x ⊓ c) :=
+(measurable_inf_const c).comp hf
+
+@[measurability]
+lemma ae_measurable.inf_const (hf : ae_measurable f μ) (c : M) :
+  ae_measurable (λ x, f x ⊓ c) μ :=
+(measurable_inf_const c).comp_ae_measurable hf
+
+end measurable_inf
+
+section measurable_inf₂
+variables [has_measurable_inf₂ M]
+
+@[measurability]
+lemma measurable.inf' (hf : measurable f) (hg : measurable g) : measurable (f ⊓ g) :=
+measurable_inf.comp (hf.prod_mk hg)
+
+@[measurability]
+lemma measurable.inf (hf : measurable f) (hg : measurable g) : measurable (λ a, f a ⊓ g a) :=
+measurable_inf.comp (hf.prod_mk hg)
+
+@[measurability]
+lemma ae_measurable.inf' (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
+  ae_measurable (f ⊓ g) μ :=
+measurable_inf.comp_ae_measurable (hf.prod_mk hg)
+
+@[measurability]
+lemma ae_measurable.inf (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
+  ae_measurable (λ a, f a ⊓ g a) μ :=
+measurable_inf.comp_ae_measurable (hf.prod_mk hg)
+
+omit m
+@[priority 100]
+instance has_measurable_inf₂.to_has_measurable_inf : has_measurable_inf M :=
+⟨λ c, measurable_const.inf measurable_id, λ c, measurable_id.inf measurable_const⟩
+include m
+
+end measurable_inf₂
+
+end inf

src/topology/order/lattice.lean

@@ -39,16 +39,17 @@ Let `L` be a topological space and let `L×L` be equipped with the product topol
 class has_continuous_sup (L : Type*) [topological_space L] [has_sup L] : Prop :=
 (continuous_sup : continuous (λ p : L × L, p.1 ⊔ p.2))
 
-/--
-Let `L` be a topological space with a supremum. If the order dual has a continuous infimum then the
-supremum is continuous.
--/
 @[priority 100] -- see Note [lower instance priority]
-instance has_continuous_inf_dual_has_continuous_sup
-  (L : Type*) [topological_space L] [has_sup L] [h: has_continuous_inf (order_dual L)] :
-  has_continuous_sup  L :=
-{ continuous_sup :=
-    @has_continuous_inf.continuous_inf (order_dual L) _ _ h }
+instance order_dual.has_continuous_sup
+  (L : Type*) [topological_space L] [has_inf L] [has_continuous_inf L] :
+  has_continuous_sup (order_dual L) :=
+{ continuous_sup := @has_continuous_inf.continuous_inf L _ _ _ }
+
+@[priority 100] -- see Note [lower instance priority]
+instance order_dual.has_continuous_inf
+  (L : Type*) [topological_space L] [has_sup L] [has_continuous_sup L] :
+  has_continuous_inf (order_dual L) :=
+{ continuous_inf := @has_continuous_sup.continuous_sup L _ _ _ }
 
 /--
 Let `L` be a lattice equipped with a topology such that `L` has continuous infimum and supremum.
@@ -57,6 +58,11 @@ Then `L` is said to be a *topological lattice*.
 class topological_lattice (L : Type*) [topological_space L] [lattice L]
   extends has_continuous_inf L, has_continuous_sup L
 
+@[priority 100] -- see Note [lower instance priority]
+instance order_dual.topological_lattice
+  (L : Type*) [topological_space L] [lattice L] [topological_lattice L] :
+  topological_lattice (order_dual L) := {}
+
 variables {L : Type*} [topological_space L]
 variables {X : Type*} [topological_space X]