Merge pull request #293 from teorth/restore-9a304a6

Restore repository content to last working snapshot (9a304a6)

Author: teorth

analysis/Analysis/MeasureTheory/Notation.lean

@@ -4,10 +4,6 @@ import Mathlib.Tactic
 # Introduction to Measure Theory, Chapter 0: Notation
 
 A companion to Chapter 0 of the book "An introduction to Measure Theory".
-
-We use existing Mathlib constructions, such as `Set.indicator`, `EuclideanSpace`, `ENNReal`,
-and `tsum` to describe the concepts defined in Chapter 0.
-
 -/
 
 /-- A version of `Set.indicator` suitable for this text. -/
@@ -40,15 +36,13 @@ theorem EuclideanSpace'.dot_apply {n:ℕ} (x y: EuclideanSpace' n) : x ⬝ y = 
 #check ENNReal.mul_top
 #check lt_top_iff_ne_top
 
-open Filter
-
+open Filter in
 theorem ENNReal.upward_continuous {x y:ℕ → ENNReal} (hx: Monotone x) (hy: Monotone y)
  {x₀ y₀ : ENNReal} (hx_lim: atTop.Tendsto x (nhds x₀))
  (hy_lim: atTop.Tendsto y (nhds y₀)) :
   atTop.Tendsto (fun n ↦ x n * y n) (nhds (x₀ * y₀)) := by
-  -- This proof is written to follow the structure of the original text.
-  have hx_lt (n:ℕ): x n ≤ x₀ := hx.ge_of_tendsto hx_lim n
-  have hy_lt (n:ℕ): y n ≤ y₀ := hy.ge_of_tendsto hy_lim n
+  have hx_lt (n:ℕ): x n ≤ x₀ := Monotone.ge_of_tendsto hx hx_lim n
+  have hy_lt (n:ℕ): y n ≤ y₀ := Monotone.ge_of_tendsto hy hy_lim n
   have zero_conv : atTop.Tendsto (fun n:ℕ ↦ (0:ENNReal)) (nhds 0) := tendsto_const_nhds
   have top_conv : atTop.Tendsto (fun n:ℕ ↦ (⊤:ENNReal)) (nhds ⊤) := tendsto_const_nhds
   obtain rfl | hx₀ := eq_zero_or_pos x₀
@@ -85,7 +79,7 @@ theorem ENNReal.upward_continuous {x y:ℕ → ENNReal} (hx: Monotone x) (hy: Mo
     have : atTop.Tendsto (fun n ↦ x n * y ny) (nhds ⊤) := by
       convert Tendsto.comp (g := fun z ↦ z * y ny) _ hx_lim
       convert (ENNReal.continuous_mul_const hyn').tendsto ⊤
-      rw [top_mul (by order)]
+      rw [ENNReal.top_mul (by order)]
     apply tendsto_nhds_top_mono this
     simp [EventuallyLE, eventually_atTop]
     use ny; intro n hn
@@ -106,82 +100,11 @@ theorem ENNReal.upward_continuous {x y:ℕ → ENNReal} (hx: Monotone x) (hy: Mo
   set y' : ℕ → NNReal := fun n ↦ (y n).toNNReal
   set x₀' : NNReal := x₀.toNNReal
   set y₀' : NNReal := y₀.toNNReal
-  have hxx₀' : x₀ = x₀' := by rw [coe_toNNReal]; order
-  have hyy₀' : y₀ = y₀' := by rw [coe_toNNReal]; order
-  have hxx' (n:ℕ) : x n = x' n := by rw [coe_toNNReal]; specialize hx_lt n; order
-  have hyy' (n:ℕ) : y n = y' n := by rw [coe_toNNReal]; specialize hy_lt n; order
+  have hxx₀' : x₀ = x₀' := by rw [ENNReal.coe_toNNReal]; order
+  have hyy₀' : y₀ = y₀' := by rw [ENNReal.coe_toNNReal]; order
+  have hxx' (n:ℕ) : x n = x' n := by rw [ENNReal.coe_toNNReal]; specialize hx_lt n; order
+  have hyy' (n:ℕ) : y n = y' n := by rw [ENNReal.coe_toNNReal]; specialize hy_lt n; order
   change atTop.Tendsto (fun n ↦ x n) (nhds x₀) at hx_lim
   change atTop.Tendsto (fun n ↦ y n) (nhds y₀) at hy_lim
-  simp [hxx', hyy', hxx₀', hyy₀',←coe_mul] at *
-  solve_by_elim [Filter.Tendsto.mul]
-
-example : ∃ (x y:ℕ → ENNReal) (hx: Antitone x) (hy: Antitone y)
- (x₀ y₀:ENNReal) (hx_lim: atTop.Tendsto x (nhds x₀))
- (hy_lim: atTop.Tendsto y (nhds y₀)), ¬ atTop.Tendsto (fun n ↦ x n * y n) (nhds (x₀ * y₀)) := by
- sorry
-
-#check ENNReal.tendsto_nat_tsum
-
-#check ENNReal.tsum_eq_iSup_sum
-
-#check Equiv.tsum_eq
-
-/-- Exercise 0.0.1 -/
-example {A:Type} {x : A → ENNReal} (hx: ∑' α, x α < ⊤) :
-  ∃ E: Set A, Countable E ∧ ∀ α ∉ E, x α = 0 := by
-  sorry
-
-/-- Theorem 0.0.2 (Tonelli's theorem for series)  -/
-theorem ENNReal.tsum_of_tsum (x: ℕ → ℕ → ENNReal) : ∑' p:ℕ × ℕ, x p.1 p.2 = ∑' n, ∑' m, x n m := by
-  -- This proof is written to largely follow the structure of the original text.
-  refine' le_antisymm _ _
-  . rw [ENNReal.tsum_eq_iSup_sum]; apply iSup_le; intro F
-    have : ∃ N, F ⊆ .range N ×ˢ .range N := by
-      have _ : IsOrderBornology ℕ := {
-        isBounded_iff_bddBelow_bddAbove s := by
-          constructor
-          . intro h; simp
-            rw [Metric.isBounded_iff_subset_closedBall 0] at h
-            choose N hN using h
-            rw [bddAbove_def]; use ⌊ N ⌋₊
-            intro n hn; specialize hN hn; simp [dist] at hN; exact Nat.le_floor hN
-          intro ⟨ h1, h2 ⟩; exact Metric.isBounded_of_bddAbove_of_bddBelow h2 h1
-        }
-      choose N₁ hN₁ using bddAbove_def.mp F.finite_toSet.isBounded.image_fst.bddAbove
-      choose N₂ hN₂ using bddAbove_def.mp F.finite_toSet.isBounded.image_snd.bddAbove
-      use N₁ ⊔ N₂ + 1; intro ⟨ n, m ⟩ hnm; simp_all
-      specialize hN₁ _ _ hnm; specialize hN₂ _ _ hnm; omega
-    choose N hN using this
-    calc
-      _ ≤ ∑ p ∈ .range N ×ˢ .range N, x p.1 p.2 := Finset.sum_le_sum_of_subset hN
-      _ = ∑ n ∈ .range N, ∑ m ∈ .range N, x n m := Finset.sum_product' _ _ _
-      _ ≤ ∑' n, ∑ m ∈ .range N, x n m := ENNReal.sum_le_tsum _
-      _ ≤ _ := by apply ENNReal.tsum_le_tsum; intro n; apply ENNReal.sum_le_tsum
-  apply le_of_tendsto' (tendsto_nat_tsum _); intro N
-  apply le_of_tendsto' (f := fun M ↦ ∑ n ∈ .range N, ∑ m ∈ .range M, x n m) (x := atTop)
-  . apply tendsto_finset_sum; intro n _; apply tendsto_nat_tsum
-  intro M
-  calc
-    _ = ∑ p ∈ .range N ×ˢ .range M, x p.1 p.2 := by symm; apply Finset.sum_product
-    _ ≤ _ := ENNReal.sum_le_tsum _
-
-/-- Theorem 0.0.2 -/
-theorem ENNReal.tsum_of_tsum' (x: ℕ → ℕ → ENNReal) : ∑' p:ℕ × ℕ, x p.1 p.2 = ∑' m, ∑' n, x n m := by
-  sorry
-
-#check ENNReal.tsum_comm
-
-/-- Exercise 0.0.2 (Tonelli's theorem for series over arbitrary sets)-/
-example {A B:Type*} (x: A → B → ENNReal) : ∑' p:A × B, x p.1 p.2 = ∑' a, ∑' b, x a b := by
-  sorry
-
-example {A B:Type*} (x: A → B → ENNReal) : ∑' p:A × B, x p.1 p.2 = ∑' b, ∑' a, x a b := by
-  sorry
-
-/-- Axiom 0.0.4 (Axiom of choice)-/
-noncomputable def Set.choose {A: Type*} {E: A → Type*} (hE: ∀ n, Nonempty (E n)) :
-∀ n, E n := fun n ↦ (hE n).some
-
-/-- Corollary 0.0.5 (Axiom of countable choice) -/
-noncomputable def Countable.choose {E: ℕ → Type*} (hE: ∀ n, Nonempty (E n)) :
-∀ n, E n := Set.choose hE
+  simp [hxx', hyy', hxx₀', hyy₀',←ENNReal.coe_mul] at hx_lim hy_lim ⊢
+  exact Filter.Tendsto.mul hx_lim hy_lim

analysis/Analysis/MeasureTheory/Section_1_1_1.lean

@@ -39,7 +39,7 @@ def finite_choice_trunc {X:Type*} {f:X → ℕ} {N:ℕ} (h: ∀ n < N, Trunc {x
   Trunc {g: Fin N → X // ∀ n, f (g n) = n} := by
   induction' N with N ih
   . apply Trunc.mk
-    refine' ⟨ Fin.elim0, _ ⟩
+    refine ⟨ Fin.elim0, ?_ ⟩
     simp only [IsEmpty.forall_iff, exists_const]
   specialize ih ?_
   . intro n hn; exact h n (Nat.lt_add_right 1 hn)

analysis/Analysis/Misc/FiniteChoice.lean

@@ -4,8 +4,6 @@ import Mathlib.Tactic
 
 namespace ProbabilityTheory
 
-/-- Todo: separate out the `prob_top` hypothesis, to allow for the zero finitely additive
-measure (useful as a junk value for conditional expectation) -/
 class FinitelyAdditive (A:Type*) [BooleanAlgebra A] where
   prob : A → ℝ
   prob_top : prob ⊤ = 1

analysis/Analysis/Misc/Probability.lean

@@ -66,7 +66,7 @@ theorem inverse_function_theorem {X Y: Set ℝ} {f: ℝ → ℝ} {g:ℝ → ℝ}
       simp [←AdherentPt_def, limit_of_AdherentPt] at hcluster ⊢
       choose x hx hconv using hcluster; use f ∘ x
       constructor
-      . intro n; refine' ⟨ by aesop, _ ⟩
+      . intro n; refine ⟨ by aesop, ?_ ⟩
         have hx2 := (hx n).2; contrapose! hx2; apply_fun g at hx2
         simpa [←hfx₀, hgf _ hx₀, hgf _ (hx n).1] using hx2
       rw [←hfx₀]

analysis/Analysis/Section_10_4.lean

@@ -57,9 +57,9 @@ theorem _root_.Filter.Tendsto.of_div' {a b L:ℝ} (hab: a < b) {f g f' g': ℝ 
       intro _; simp; intros; split_ands <;> linarith
     . intro _; simp; intro _ _; split_ands <;> linarith
     intro _; simp; intros; split_ands <;> linarith
-  refine' ⟨ this, _ ⟩
+  refine ⟨ this, ?_ ⟩
   rw [nhdsWithin.eq_1] at hderiv ⊢
-  rw [←Convergesto.iff, Convergesto.iff_conv]
+  rw [←Convergesto.iff, Convergesto.iff_conv _ _ _]
   . intro x hx hconv
     have hxy (n:ℕ) : ∃ yn ∈ Set.Ioo a (x n), (f (x n))/(g (x n)) = f' yn / (g' yn) := by
       set h : ℝ → ℝ := fun x' ↦ (f x') * (g (x n)) - (g x') * (f (x n))

analysis/Analysis/Section_10_5.lean

@@ -90,7 +90,7 @@ noncomputable instance BoundedInterval.instInter : Inter BoundedInterval where
 
 @[simp]
 theorem BoundedInterval.inter_eq (I J: BoundedInterval) : (I ∩ J : BoundedInterval) = (I:Set ℝ) ∩ (J:Set ℝ)  :=
-  (inter I J).choose_spec.symm
+  (BoundedInterval.inter I J).choose_spec.symm
 
 example :
   (Ioo 2 4 ∩ Icc 4 6) = (Icc 4 4 : Set ℝ) := by

analysis/Analysis/Section_11_1.lean

@@ -43,7 +43,7 @@ theorem PiecewiseConstantOn.RS_integ_eq_integ_of_mul_deriv
   set α' := derivWithin α (Icc a b)
   have hf_integ: IntegrableOn f (Icc a b) := (integ_of_piecewise_const hf).1
   observe hfα'_integ: IntegrableOn (f * α') (Icc a b)
-  refine' ⟨ hfα'_integ, _ ⟩
+  refine ⟨ hfα'_integ, ?_ ⟩
   choose P hP using hf
   rw [PiecewiseConstantOn.RS_integ_def hP α, hfα'_integ.split P]
   apply Finset.sum_congr rfl; intro J hJ
@@ -125,7 +125,7 @@ theorem RS_integ_eq_integ_of_mul_deriv
     linarith
   have h3 : lower_integral (f * α') (Icc a b) ≤
     upper_integral (f * α') (Icc a b) := lower_integral_le_upper hfα'_bound
-  refine' ⟨ ⟨ hfα'_bound, _ ⟩, _ ⟩ <;> linarith
+  refine ⟨ ⟨ hfα'_bound, ?_ ⟩, ?_ ⟩ <;> linarith
 
 /-- Lemma 11.10.5 / Exercise 11.10.2-/
 theorem PiecewiseConstantOn.RS_integ_of_comp {a b:ℝ} (hab: a < b) {φ f:ℝ → ℝ}
@@ -157,7 +157,7 @@ theorem PiecewiseConstantOn.RS_integ_of_comp {a b:ℝ} (hab: a < b) {φ f:ℝ 
   have hfφ_piecewise : PiecewiseConstantWith (f ∘ φ) Q := by
     sorry
   have hfφ_piecewise' : PiecewiseConstantOn (f ∘ φ) (Icc a b) := ⟨ Q, hfφ_piecewise ⟩
-  refine' ⟨ hfφ_piecewise' , _ ⟩
+  refine ⟨ hfφ_piecewise' , ?_ ⟩
   rw [RS_integ_def hfφ_piecewise]
   unfold PiecewiseConstantWith.RS_integ
   rw [Finset.sum_image, ←Finset.sum_coe_sort (s := P.intervals)]
@@ -205,7 +205,7 @@ theorem RS_integ_of_comp {a b:ℝ} (hab: a < b) {φ f: ℝ → ℝ}
     linarith [integ_le_lower_RS_integral hfφ_bdd this hpc.1 hφ_mono]
   have hle : lower_RS_integral (f ∘ φ) (Icc a b) φ ≤ upper_RS_integral (f ∘ φ) (Icc a b) φ :=
     lower_RS_integral_le_upper hfφ_bdd hφ_mono
-  refine' ⟨ ⟨ hfφ_bdd, _ ⟩, _ ⟩ <;> linarith
+  refine ⟨ ⟨ hfφ_bdd, ?_ ⟩, ?_ ⟩ <;> linarith
 
 /-- Proposition 11.10.7 (Change of variables formula III)-/
 theorem integ_of_comp {a b:ℝ} (hab: a < b) {φ f: ℝ → ℝ}
@@ -218,7 +218,7 @@ theorem integ_of_comp {a b:ℝ} (hab: a < b) {φ f: ℝ → ℝ}
     integ f (Icc (φ a) (φ b)) := by
  have h1 := RS_integ_of_comp hab hφ_cont hφ_mono hf
  have h2 := RS_integ_eq_integ_of_mul_deriv hab hφ_mono hφ_diff hφ_cont hφ' h1.1
- exact ⟨ h2.1, by aesop ⟩
+ refine ⟨ h2.1, by aesop ⟩
 
 /-- Exercise 11.10.3-/
 example {a b:ℝ} (hab: a < b) {f: ℝ → ℝ} (hf: IntegrableOn f (Icc a b)) :

analysis/Analysis/Section_11_10.lean

@@ -44,13 +44,13 @@ theorem lower_integral_congr {f g:ℝ → ℝ} {I: BoundedInterval} (h: Set.EqOn
 
 lemma integral_bound_upper_of_bounded {f:ℝ → ℝ} {M:ℝ} {I: BoundedInterval} (h: ∀ x ∈ (I:Set ℝ), |f x| ≤ M) : M * |I|ₗ ∈ (PiecewiseConstantOn.integ · I) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I} := by
   simp
-  refine' ⟨ fun _ ↦ M , ⟨ ⟨ _, _, ⟩, PiecewiseConstantOn.integ_const _ _ ⟩ ⟩
+  refine ⟨ fun _ ↦ M , ⟨ ⟨ ?_, ?_, ⟩, PiecewiseConstantOn.integ_const _ _ ⟩ ⟩
   . peel h with _ _ _; simp_all [abs_le']
   exact (ConstantOn.of_const (c := M) (by simp)).piecewiseConstantOn
 
 lemma integral_bound_lower_of_bounded {f:ℝ → ℝ} {M:ℝ} {I: BoundedInterval} (h: ∀ x ∈ (I:Set ℝ), |f x| ≤ M) : -M * |I|ₗ ∈ (PiecewiseConstantOn.integ · I) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I} := by
   simp
-  refine' ⟨ fun _ ↦ -M , ⟨ ⟨ _, _, ⟩, by convert PiecewiseConstantOn.integ_const _ _ using 1; simp ⟩ ⟩
+  refine ⟨ fun _ ↦ -M , ⟨ ⟨ ?_, ?_, ⟩, by convert PiecewiseConstantOn.integ_const _ _ using 1; simp ⟩ ⟩
   . peel h with _ _ _; simp [abs_le'] at *; linarith
   exact (ConstantOn.of_const (c := -M) (by simp)).piecewiseConstantOn
 

analysis/Analysis/Section_11_3.lean

@@ -27,7 +27,7 @@ theorem integ_of_uniform_cts {I: BoundedInterval} {f:ℝ → ℝ} (hf: UniformCo
   -- This proof is written to follow the structure of the original text.
   have hfbound : BddOn f I := by
     rw [BddOn.iff']; exact hf.of_bounded subset_rfl (Bornology.IsBounded.of_boundedInterval I)
-  refine' ⟨ hfbound, _ ⟩
+  refine ⟨ hfbound, ?_ ⟩
   by_cases hsing : |I|ₗ = 0
   . exact (integ_on_subsingleton hsing).1.2
   simp [length] at hsing