Merge branch 'master' into scholzhannah/openPartialHomeomorphRenames

Author: scholzhannah

Mathlib/Algebra/Lie/InvariantForm.lean

@@ -202,7 +202,7 @@ theorem isSemisimple_of_nondegenerate : IsSemisimple K L := by
   intro J hJ hJI
   rw [← lie_eq_self_of_isAtom_of_nonabelian J hJ (hL J hJ), lieIdeal_oper_eq_span, lieSpan_le]
   rintro _ ⟨x, y, rfl⟩
-  simp only [orthogonal_carrier, Φ.isOrtho_def, Set.mem_setOf_eq]
+  simp only [orthogonal_carrier, LinearMap.IsOrtho, Set.mem_setOf_eq]
   intro z hz
   rw [← neg_eq_zero, ← hΦ_inv]
   suffices ⁅(x : L), z⁆ = 0 by simp only [this, map_zero, LinearMap.zero_apply]

Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean

@@ -130,13 +130,7 @@ Note that for general (neither symmetric nor antisymmetric) bilinear forms this
 chirality; in addition to this "right" orthogonal complement one could define a "left" orthogonal
 complement for which, for all `y` in `N`, `B x y = 0`.  This variant definition is not currently
 provided in mathlib. -/
-def orthogonal (B : BilinForm R M) (N : Submodule R M) : Submodule R M where
-  carrier := { m | ∀ n ∈ N, IsOrtho B n m }
-  zero_mem' x _ := isOrtho_zero_right x
-  add_mem' {x y} hx hy n hn := by
-    rw [IsOrtho, add_right, show B n x = 0 from hx n hn, show B n y = 0 from hy n hn, zero_add]
-  smul_mem' c x hx n hn := by
-    rw [IsOrtho, smul_right, show B n x = 0 from hx n hn, mul_zero]
+def orthogonal (B : BilinForm R M) (N : Submodule R M) : Submodule R M := N.orthogonalBilin B
 
 variable {N L : Submodule R M}
 

Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

@@ -1305,8 +1305,7 @@ theorem exists_orthogonal_basis [hK : Invertible (2 : K)] {B : LinearMap.BilinFo
   obtain ⟨x, hx⟩ := exists_bilinForm_self_ne_zero hB₁ hB₂
   rw [← Submodule.finrank_add_eq_of_isCompl (isCompl_span_singleton_orthogonal hx).symm,
     finrank_span_singleton (ne_zero_of_map hx)] at hd
-  let B' := B.domRestrict₁₂ (Submodule.orthogonalBilin (K ∙ x) B)
-    (Submodule.orthogonalBilin (K ∙ x) B)
+  let B' := B.domRestrict₁₂ ((K ∙ x).orthogonalBilin B) ((K ∙ x).orthogonalBilin B)
   obtain ⟨v', hv₁⟩ := ih (hB₂.domRestrict _ : B'.IsSymm) (Nat.succ.inj hd)
   -- concatenate `x` with the basis obtained by induction
   let b :=

Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean

@@ -332,7 +332,7 @@ lemma orthogonal_rootSpan_eq :
   obtain ⟨u, hu, v, hv, rfl⟩ : ∃ᵉ (u ∈ P.rootSpan R) (v ∈ LinearMap.ker P.RootForm), u + v = y := by
     rw [← Submodule.mem_sup, P.isCompl_rootSpan_ker_rootForm.sup_eq_top]; exact Submodule.mem_top
   simp only [LinearMap.mem_ker] at hv
-  simp [hx _ hu, hv]
+  simp [LinearMap.IsOrtho, hx _ hu, hv]
 
 @[simp]
 lemma orthogonal_corootSpan_eq :

Mathlib/LinearAlgebra/SesquilinearForm/Basic.lean

@@ -352,17 +352,25 @@ namespace Submodule
 
 /-! ### The orthogonal complement -/
 
-variable [CommRing R] [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] [AddCommGroup M] [Module R M]
-  {I₁ : R₁ →+* R} {I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M}
+variable [CommSemiring R] [CommSemiring R₁] [CommSemiring R₂]
+variable [AddCommMonoid M] [Module R M]
+variable [AddCommMonoid M₁] [Module R₁ M₁]
+variable [AddCommMonoid M₂] [Module R₂ M₂]
+variable {N L : Submodule R₁ M₁}
+
+section
 
+variable {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M}
+
+variable (B) in
 /-- The orthogonal complement of a submodule `N` with respect to some bilinear map is the set of
 elements `x` which are orthogonal to all elements of `N`; i.e., for all `y` in `N`, `B x y = 0`.
 
 Note that for general (neither symmetric nor antisymmetric) bilinear maps this definition has a
 chirality; in addition to this "left" orthogonal complement one could define a "right" orthogonal
 complement for which, for all `y` in `N`, `B y x = 0`.  This variant definition is not currently
 provided in mathlib. -/
-def orthogonalBilin (N : Submodule R₁ M₁) (B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M) : Submodule R₁ M₁ where
+def orthogonalBilin (N : Submodule R₁ M₁) : Submodule R₂ M₂ where
   carrier := { m | ∀ n ∈ N, B.IsOrtho n m }
   zero_mem' x _ := B.isOrtho_zero_right x
   add_mem' hx hy n hn := by
@@ -371,18 +379,24 @@ def orthogonalBilin (N : Submodule R₁ M₁) (B : M₁ →ₛₗ[I₁] M₁ →
   smul_mem' c x hx n hn := by
     rw [LinearMap.IsOrtho, map_smulₛₗ, show B n x = 0 from hx n hn, smul_zero]
 
-variable {N L : Submodule R₁ M₁}
-
 @[simp]
-theorem mem_orthogonalBilin_iff {m : M₁} : m ∈ N.orthogonalBilin B ↔ ∀ n ∈ N, B.IsOrtho n m :=
+theorem mem_orthogonalBilin_iff {m : M₂} : m ∈ N.orthogonalBilin B ↔ ∀ n ∈ N, B.IsOrtho n m :=
   Iff.rfl
 
 theorem orthogonalBilin_le (h : N ≤ L) : L.orthogonalBilin B ≤ N.orthogonalBilin B :=
   fun _ hn l hl ↦ hn l (h hl)
 
+end
+
+section
+
+variable {I₁ : R₁ →+* R} {I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M}
+
 theorem le_orthogonalBilin_orthogonalBilin (b : B.IsRefl) :
     N ≤ (N.orthogonalBilin B).orthogonalBilin B := fun n hn _m hm ↦ b _ _ (hm n hn)
 
+end
+
 end Submodule
 
 namespace LinearMap
@@ -394,7 +408,7 @@ variable [Field K] [AddCommGroup V] [Module K V] [Field K₁] [AddCommGroup V₁
 
 -- ↓ This lemma only applies in fields as we require `a * b = 0 → a = 0 ∨ b = 0`
 theorem span_singleton_inf_orthogonal_eq_bot (B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂) (x : V₁)
-    (hx : ¬B.IsOrtho x x) : (K₁ ∙ x) ⊓ Submodule.orthogonalBilin (K₁ ∙ x) B = ⊥ := by
+    (hx : ¬B.IsOrtho x x) : (K₁ ∙ x) ⊓ (K₁ ∙ x).orthogonalBilin B = ⊥ := by
   rw [← Finset.coe_singleton]
   refine eq_bot_iff.2 fun y h ↦ ?_
   obtain ⟨μ, -, rfl⟩ := Submodule.mem_span_finset.1 h.1
@@ -408,7 +422,7 @@ theorem span_singleton_inf_orthogonal_eq_bot (B : V₁ →ₛₗ[J₁] V₁ →
 
 -- ↓ This lemma only applies in fields since we use the `mul_eq_zero`
 theorem orthogonal_span_singleton_eq_to_lin_ker {B : V →ₗ[K] V →ₛₗ[J] V₂} (x : V) :
-    Submodule.orthogonalBilin (K ∙ x) B = LinearMap.ker (B x) := by
+    (K ∙ x).orthogonalBilin B = LinearMap.ker (B x) := by
   ext y
   simp_rw [Submodule.mem_orthogonalBilin_iff, LinearMap.mem_ker, Submodule.mem_span_singleton]
   constructor
@@ -419,15 +433,15 @@ theorem orthogonal_span_singleton_eq_to_lin_ker {B : V →ₗ[K] V →ₛₗ[J]
 
 -- todo: Generalize this to sesquilinear maps
 theorem span_singleton_sup_orthogonal_eq_top {B : V →ₗ[K] V →ₗ[K] K} {x : V} (hx : ¬B.IsOrtho x x) :
-    (K ∙ x) ⊔ Submodule.orthogonalBilin (N := K ∙ x) (B := B) = ⊤ := by
+    (K ∙ x) ⊔ (K ∙ x).orthogonalBilin B = ⊤ := by
   rw [orthogonal_span_singleton_eq_to_lin_ker]
   exact (B x).span_singleton_sup_ker_eq_top hx
 
 -- todo: Generalize this to sesquilinear maps
 /-- Given a bilinear form `B` and some `x` such that `B x x ≠ 0`, the span of the singleton of `x`
   is complement to its orthogonal complement. -/
 theorem isCompl_span_singleton_orthogonal {B : V →ₗ[K] V →ₗ[K] K} {x : V} (hx : ¬B.IsOrtho x x) :
-    IsCompl (K ∙ x) (Submodule.orthogonalBilin (N := K ∙ x) (B := B)) :=
+    IsCompl (K ∙ x) ((K ∙ x).orthogonalBilin B) :=
   { disjoint := disjoint_iff.2 <| span_singleton_inf_orthogonal_eq_bot B x hx
     codisjoint := codisjoint_iff.2 <| span_singleton_sup_orthogonal_eq_top hx }
 

Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean

@@ -111,25 +111,17 @@ theorem measurable_limit_of_tendsto_metrizable_ae {ι} [Countable ι] [Nonempty
   inhabit ι
   rcases eq_or_neBot L with (rfl | hL)
   · exact ⟨(hf default).mk _, (hf default).measurable_mk, Eventually.of_forall fun x => tendsto_bot⟩
-  let p : α → (ι → β) → Prop := fun x f' => ∃ l : β, Tendsto (fun n => f' n) L (𝓝 l)
-  have hp_mem : ∀ x ∈ aeSeqSet hf p, p x fun n => f n x := fun x hx =>
-    aeSeq.fun_prop_of_mem_aeSeqSet hf hx
-  have h_ae_eq : ∀ᵐ x ∂μ, ∀ n, aeSeq hf p n x = f n x := aeSeq.aeSeq_eq_fun_ae hf h_ae_tendsto
-  set f_lim : α → β := fun x => dite (x ∈ aeSeqSet hf p) (fun h => (hp_mem x h).choose)
-    fun _ => (⟨f default x⟩ : Nonempty β).some
-  have hf_lim : ∀ x, Tendsto (fun n => aeSeq hf p n x) L (𝓝 (f_lim x)) := by
-    intro x
-    simp only [aeSeq, f_lim]
-    split_ifs with h
-    · refine (hp_mem x h).choose_spec.congr fun n => ?_
-      exact (aeSeq.mk_eq_fun_of_mem_aeSeqSet hf h n).symm
-    · exact tendsto_const_nhds
-  have h_ae_tendsto_f_lim : ∀ᵐ x ∂μ, Tendsto (fun n => f n x) L (𝓝 (f_lim x)) :=
-    h_ae_eq.mono fun x hx => (hf_lim x).congr hx
-  have h_f_lim_meas : Measurable f_lim :=
-    measurable_of_tendsto_metrizable' L (aeSeq.measurable hf p)
-      (tendsto_pi_nhds.mpr fun x => hf_lim x)
-  exact ⟨f_lim, h_f_lim_meas, h_ae_tendsto_f_lim⟩
+  set f_lim : α → β := fun x ↦
+    if h : ∃ l : β, Tendsto (fun n ↦ f n x) L (𝓝 l) then h.choose
+      else (⟨f default x⟩ : Nonempty β).some
+  have h_ae_tendsto_f_lim : ∀ᵐ x ∂μ, Tendsto (fun n ↦ f n x) L (𝓝 (f_lim x)) := by
+    filter_upwards [h_ae_tendsto] with x hx
+    simpa [f_lim, hx] using hx.choose_spec
+  have hf_lim : AEMeasurable f_lim μ :=
+    aemeasurable_of_tendsto_metrizable_ae L hf h_ae_tendsto_f_lim
+  refine ⟨hf_lim.mk f_lim, hf_lim.measurable_mk, ?_⟩
+  filter_upwards [h_ae_tendsto_f_lim, hf_lim.ae_eq_mk] with x hx h_eq
+  simpa [h_eq] using hx
 
 end Limits
 

Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean

@@ -134,14 +134,9 @@ theorem memLp_trim_of_mem_lpMeasSubgroup (hm : m ≤ m0) (f : Lp F p μ)
     MemLp (mem_lpMeasSubgroup_iff_aestronglyMeasurable.mp hf_meas).choose p (μ.trim hm) := by
   have hf : AEStronglyMeasurable[m] f μ :=
     mem_lpMeasSubgroup_iff_aestronglyMeasurable.mp hf_meas
-  let g := hf.choose
-  obtain ⟨hg, hfg⟩ := hf.choose_spec
-  change MemLp g p (μ.trim hm)
-  refine ⟨hg.aestronglyMeasurable, ?_⟩
-  have h_eLpNorm_fg : eLpNorm g p (μ.trim hm) = eLpNorm f p μ := by
-    rw [eLpNorm_trim hm hg]
-    exact eLpNorm_congr_ae hfg.symm
-  rw [h_eLpNorm_fg]
+  change MemLp (hf.mk f) p (μ.trim hm)
+  refine ⟨hf.stronglyMeasurable_mk.aestronglyMeasurable, ?_⟩
+  rw [eLpNorm_trim hm hf.stronglyMeasurable_mk, eLpNorm_congr_ae hf.ae_eq_mk.symm]
   exact Lp.eLpNorm_lt_top f
 
 /-- If `f` belongs to `Lp` for the measure `μ.trim hm`, then it belongs to the subgroup

Mathlib/MeasureTheory/Function/LpSpace/Complete.lean

@@ -282,26 +282,10 @@ theorem ae_tendsto_of_cauchy_eLpNorm' [CompleteSpace E] {f : ℕ → α → E} {
     have h4 : ∀ᵐ x ∂μ, ∑' i, ‖f (i + 1) x - f i x‖ₑ < ∞ :=
       tsum_enorm_sub_ae_lt_top hf hp1 hB h3
     exact h4.mono fun x hx => .of_nnnorm <| ENNReal.tsum_coe_ne_top_iff_summable.mp hx.ne
-  have h :
-    ∀ᵐ x ∂μ, ∃ l : E,
-      atTop.Tendsto (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) (𝓝 l) := by
-    refine h_summable.mono fun x hx => ?_
-    let hx_sum := hx.hasSum.tendsto_sum_nat
-    exact ⟨∑' i, (f (i + 1) x - f i x), hx_sum⟩
-  refine h.mono fun x hx => ?_
-  obtain ⟨l, hx⟩ := hx
-  have h_rw_sum :
-      (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) = fun n => f n x - f 0 x := by
-    ext1 n
-    change
-      (∑ i ∈ Finset.range n, ((fun m => f m x) (i + 1) - (fun m => f m x) i)) = f n x - f 0 x
-    rw [Finset.sum_range_sub (fun m => f m x)]
-  rw [h_rw_sum] at hx
-  have hf_rw : (fun n => f n x) = fun n => f n x - f 0 x + f 0 x := by
-    ext1 n
-    abel
-  rw [hf_rw]
-  exact ⟨l + f 0 x, Tendsto.add_const _ hx⟩
+  refine h_summable.mono fun x hx ↦ ?_
+  have hx_sum := hx.hasSum.tendsto_sum_nat
+  rw [funext fun n ↦ Finset.sum_range_sub (fun m ↦ f m x) n] at hx_sum
+  exact ⟨∑' i, (f (i + 1) x - f i x) + f 0 x, by simpa using hx_sum.add_const (f 0 x)⟩
 
 theorem ae_tendsto_of_cauchy_eLpNorm [CompleteSpace E] {f : ℕ → α → E}
     (hf : ∀ n, AEStronglyMeasurable (f n) μ) (hp : 1 ≤ p) {B : ℕ → ℝ≥0∞} (hB : ∑' i, B i ≠ ∞)

Mathlib/Probability/Process/Adapted.lean

@@ -11,20 +11,22 @@ public import Mathlib.Topology.Instances.Discrete
 /-!
 # Adapted and progressively measurable processes
 
-This file defines the related notions of a process `u` being `Adapted`, `StronglyAdapted`
-or `StronglyProgressive` (progressively measurable) with respect to a filter `f`, and proves
-some basic facts about them.
+This file defines the related notions of a process `u` being (strongly) `Adapted` or
+`Progressive` (progressively measurable) with respect to a filtration `f`, and proves some
+basic facts about them.
 
 ## Main definitions
 
 * `MeasureTheory.Adapted`: a sequence of functions `u` is said to be adapted to a
   filtration `f` if at each point in time `i`, `u i` is `f i`-measurable
-* `MeasureTheory.StronglyAdapted`: a sequence of functions `u` is said to be strongly adapted to a
-  filtration `f` if at each point in time `i`, `u i` is `f i`-strongly measurable
-* `MeasureTheory.IsStronglyProgressive`: a sequence of functions `u` is said to be strongly
-  progressive with respect to a filtration `f` if at each point in time `i`, `u` restricted to
-  `Set.Iic i × Ω` is strongly measurable with respect to the product `MeasurableSpace` structure
-  where the σ-algebra used for `Ω` is `f i`.
+* `MeasureTheory.IsProgressive`: a sequence of functions `u` is said to be progressive with respect
+  to a filtration `f` if at each point in time `i`, `u` restricted to `Set.Iic i × Ω` is strongly
+  measurable with respect to the product `MeasurableSpace` structure where the σ-algebra used for
+  `Ω` is `f i`.
+We also provide the following variants, which use `MeasureTheory.StronglyMeasurable` instead
+of `Measurable`:
+* `MeasureTheory.StronglyAdapted`
+* `MeasureTheory.IsStronglyProgressive`
 
 ## Main results
 
@@ -178,6 +180,77 @@ theorem Filtration.stronglyAdapted_natural [∀ i, MetrizableSpace (β i)]
 
 end StronglyAdapted
 
+section Progressive
+
+variable {β : Type*} {u v : ι → Ω → β}
+
+/-- Progressive process. A sequence of functions `u` is said to be progressive with respect
+to a filtration `f` if at each point in time `i`, `u` restricted to `Set.Iic i × Ω` is measurable
+with respect to the product `MeasurableSpace` structure where the σ-algebra used for `Ω` is `f i`.
+The usual definition uses the interval `[0,i]`, which we replace by `Set.Iic i`. We recover the
+usual definition for index types `ℝ≥0` or `ℕ`. -/
+def IsProgressive [MeasurableSpace ι] [MeasurableSpace β] (f : Filtration ι m)
+    (u : ι → Ω → β) : Prop :=
+  ∀ i, Measurable[Subtype.instMeasurableSpace.prod (f i)] fun p : Set.Iic i × Ω => u p.1 p.2
+
+theorem isProgressive_const {mi : MeasurableSpace ι} {mβ : MeasurableSpace β} (f : Filtration ι m)
+    (b : β) : IsProgressive f (fun _ _ => b : ι → Ω → β) :=
+  fun _ ↦ by exact measurable_const
+
+namespace IsProgressive
+
+variable {mi : MeasurableSpace ι} {mβ : MeasurableSpace β}
+
+protected theorem adapted (h : IsProgressive f u) : Adapted f u := by
+  intro i
+  have : u i = (fun p : Set.Iic i × Ω => u p.1 p.2) ∘ fun x => (⟨i, Set.mem_Iic.mpr le_rfl⟩, x) :=
+    rfl
+  rw [this]
+  exact (h i).comp measurable_prodMk_left
+
+protected theorem comp {t : ι → Ω → ι} (h : IsProgressive f u) (ht : IsProgressive f t)
+    (ht_le : ∀ i ω, t i ω ≤ i) :
+    IsProgressive f fun i ω => u (t i ω) ω := by
+  intro i
+  have : (fun p : ↥(Set.Iic i) × Ω => u (t (p.fst : ι) p.snd) p.snd) =
+    (fun p : ↥(Set.Iic i) × Ω => u (p.fst : ι) p.snd) ∘ fun p : ↥(Set.Iic i) × Ω =>
+      (⟨t (p.fst : ι) p.snd, Set.mem_Iic.mpr ((ht_le _ _).trans p.fst.prop)⟩, p.snd) := rfl
+  rw [this]
+  exact (h i).comp ((ht i).subtype_mk.prodMk measurable_snd)
+
+section Arithmetic
+
+@[to_additive]
+protected theorem mul [Mul β] [MeasurableMul₂ β] (hu : IsProgressive f u)
+    (hv : IsProgressive f v) : IsProgressive f fun i ω ↦  (u i ω * v i ω) :=
+  fun i ↦ Measurable.mul (hu i) (hv i)
+
+@[to_additive]
+protected theorem finsetProd {γ} [CommMonoid β] [MeasurableMul₂ β] {U : γ → ι → Ω → β}
+    {s : Finset γ} (h : ∀ c ∈ s, IsProgressive f (U c)) :
+    IsProgressive f fun i ω ↦ ∏ c ∈ s, U c i ω :=
+  fun i ↦ s.measurable_prod fun c hc ↦ h c hc i
+
+@[to_additive]
+protected theorem inv [Group β] [MeasurableInv β] (hu : IsProgressive f u) :
+    IsProgressive f fun i ω => (u i ω)⁻¹ := fun i ↦ (hu i).inv
+
+@[to_additive]
+protected theorem div [Group β] [MeasurableDiv₂ β] (hu : IsProgressive f u)
+    (hv : IsProgressive f v) : IsProgressive f fun i ω ↦ u i ω / v i ω :=
+  fun i ↦ Measurable.div (hu i) (hv i)
+
+/-- The norm of a progressive process is progressive. -/
+protected lemma norm [NormedAddCommGroup β] [OpensMeasurableSpace β] (hu : IsProgressive f u) :
+    IsProgressive f fun t ω ↦ ‖u t ω‖ :=
+  fun i ↦ by apply @(hu i).norm; infer_instance
+
+end Arithmetic
+
+end IsProgressive
+
+end Progressive
+
 variable {β : Type*} [TopologicalSpace β] {u v : ι → Ω → β}
 
 /-- Strongly progressive process. A sequence of functions `u` is said to be strongly
@@ -264,6 +337,15 @@ end Arithmetic
 
 end IsStronglyProgressive
 
+lemma IsProgressive.isStronglyProgressive {mi : MeasurableSpace ι} {mβ : MeasurableSpace β}
+    [PseudoMetrizableSpace β] [SecondCountableTopology β] [OpensMeasurableSpace β]
+  (h : IsProgressive f u) : IsStronglyProgressive f u :=
+  fun i ↦ (h i).stronglyMeasurable
+
+lemma IsStronglyProgressive.isProgressive {mi : MeasurableSpace ι} {mβ : MeasurableSpace β}
+    [PseudoMetrizableSpace β] [BorelSpace β] (h : IsStronglyProgressive f u) : IsProgressive f u :=
+  fun i ↦ (h i).measurable
+
 theorem isStronglyProgressive_of_tendsto' {γ} [MeasurableSpace ι] [PseudoMetrizableSpace β]
     (fltr : Filter γ) [fltr.NeBot] [fltr.IsCountablyGenerated] {U : γ → ι → Ω → β}
     (h : ∀ l, IsStronglyProgressive f (U l)) (h_tendsto : Tendsto U fltr (𝓝 u)) :