feat(measure_theory/integral): Cauchy integral formula for a circle (#…

…10000)

src/analysis/box_integral/box/basic.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import topology.metric_space.basic
+import topology.algebra.ordered.monotone_convergence
+import data.set.intervals.monotone
 
 /-!
 # Rectangular boxes in `ℝⁿ`
@@ -47,10 +49,10 @@ that returns the box `⟨l, u, _⟩` if it is nonempty and `⊥` otherwise.
 rectangular box
 -/
 
-open set function metric
+open set function metric filter
 
 noncomputable theory
-open_locale nnreal classical
+open_locale nnreal classical topological_space
 
 namespace box_integral
 
@@ -286,7 +288,7 @@ by rw [disjoint_coe, set.not_disjoint_iff_nonempty_inter]
 
 /-- Face of a box in `ℝⁿ⁺¹ = fin (n + 1) → ℝ`: the box in `ℝⁿ = fin n → ℝ` with corners at
 `I.lower ∘ fin.succ_above i` and `I.upper ∘ fin.succ_above i`. -/
-@[simps] def face {n} (I : box (fin (n + 1))) (i : fin (n + 1)) : box (fin n) :=
+@[simps { simp_rhs := tt }] def face {n} (I : box (fin (n + 1))) (i : fin (n + 1)) : box (fin n) :=
 ⟨I.lower ∘ fin.succ_above i, I.upper ∘ fin.succ_above i, λ j, I.lower_lt_upper _⟩
 
 @[simp] lemma face_mk {n} (l u : fin (n + 1) → ℝ) (h : ∀ i, l i < u i) (i : fin (n + 1)) :
@@ -297,6 +299,8 @@ rfl
   face I i ≤ face J i :=
 λ x hx i, Ioc_subset_Ioc ((le_iff_bounds.1 h).1 _) ((le_iff_bounds.1 h).2 _) (hx _)
 
+lemma monotone_face {n} (i : fin (n + 1)) : monotone (λ I, face I i) := λ I J h, face_mono h i
+
 lemma maps_to_insert_nth_face_Icc {n} (I : box (fin (n + 1))) {i : fin (n + 1)} {x : ℝ}
   (hx : x ∈ Icc (I.lower i) (I.upper i)) :
   maps_to (i.insert_nth x) (I.face i).Icc I.Icc :=
@@ -314,6 +318,45 @@ lemma continuous_on_face_Icc {X} [topological_space X] {n} {f : (fin (n + 1) →
   continuous_on (f ∘ i.insert_nth x) (I.face i).Icc :=
 h.comp (continuous_on_const.fin_insert_nth i continuous_on_id) (I.maps_to_insert_nth_face_Icc hx)
 
+/-!
+### Covering of the interior of a box by a monotone sequence of smaller boxes
+-/
+
+/-- The interior of a box. -/
+protected def Ioo : box ι →o set (ι → ℝ) :=
+{ to_fun := λ I, pi univ (λ i, Ioo (I.lower i) (I.upper i)),
+  monotone' := λ I J h, pi_mono $ λ i hi, Ioo_subset_Ioo ((le_iff_bounds.1 h).1 i)
+    ((le_iff_bounds.1 h).2 i) }
+
+lemma Ioo_subset_coe (I : box ι) : I.Ioo ⊆ I := λ x hx i, Ioo_subset_Ioc_self (hx i trivial)
+
+protected lemma Ioo_subset_Icc (I : box ι) : I.Ioo ⊆ I.Icc := I.Ioo_subset_coe.trans coe_subset_Icc
+
+lemma Union_Ioo_of_tendsto [fintype ι] {I : box ι} {J : ℕ → box ι} (hJ : monotone J)
+  (hl : tendsto (lower ∘ J) at_top (𝓝 I.lower)) (hu : tendsto (upper ∘ J) at_top (𝓝 I.upper)) :
+  (⋃ n, (J n).Ioo) = I.Ioo :=
+have hl' : ∀ i, antitone (λ n, (J n).lower i),
+  from λ i, (monotone_eval i).comp_antitone (antitone_lower.comp_monotone hJ),
+have hu' : ∀ i, monotone (λ n, (J n).upper i),
+  from λ i, (monotone_eval i).comp (monotone_upper.comp hJ),
+calc (⋃ n, (J n).Ioo) = pi univ (λ i, ⋃ n, Ioo ((J n).lower i) ((J n).upper i)) :
+  Union_univ_pi_of_monotone (λ i, (hl' i).Ioo (hu' i))
+... = I.Ioo :
+  pi_congr rfl (λ i hi, Union_Ioo_of_mono_of_is_glb_of_is_lub (hl' i) (hu' i)
+    (is_glb_of_tendsto_at_top (hl' i) (tendsto_pi_nhds.1 hl _))
+    (is_lub_of_tendsto_at_top (hu' i) (tendsto_pi_nhds.1 hu _)))
+
+lemma exists_seq_mono_tendsto (I : box ι) : ∃ J : ℕ →o box ι, (∀ n, (J n).Icc ⊆ I.Ioo) ∧
+  tendsto (lower ∘ J) at_top (𝓝 I.lower) ∧ tendsto (upper ∘ J) at_top (𝓝 I.upper) :=
+begin
+  choose a b ha_anti hb_mono ha_mem hb_mem hab ha_tendsto hb_tendsto
+    using λ i, exists_seq_strict_anti_strict_mono_tendsto (I.lower_lt_upper i),
+  exact ⟨⟨λ k, ⟨flip a k, flip b k, λ i, hab _ _ _⟩,
+    λ k l hkl, le_iff_bounds.2 ⟨λ i, (ha_anti i).antitone hkl, λ i, (hb_mono i).monotone hkl⟩⟩,
+    λ n x hx i hi, ⟨(ha_mem _ _).1.trans_le (hx.1 _), (hx.2 _).trans_lt (hb_mem _ _).2⟩,
+    tendsto_pi_nhds.2 ha_tendsto, tendsto_pi_nhds.2 hb_tendsto⟩
+end
+
 section distortion
 
 variable [fintype ι]

src/analysis/box_integral/partition/measure.lean

@@ -35,22 +35,33 @@ open measure_theory
 
 namespace box
 
-variables (I : box ι)
+lemma measure_Icc_lt_top (I : box ι) (μ : measure (ι → ℝ)) [is_locally_finite_measure μ] :
+  μ I.Icc < ∞ :=
+show μ (Icc I.lower I.upper) < ∞, from I.is_compact_Icc.measure_lt_top
+
+lemma measure_coe_lt_top (I : box ι) (μ : measure (ι → ℝ)) [is_locally_finite_measure μ] :
+  μ I < ∞ :=
+(measure_mono $ coe_subset_Icc).trans_lt (I.measure_Icc_lt_top μ)
+
+variables [fintype ι] (I : box ι)
 
-lemma measurable_set_coe [fintype ι] (I : box ι) : measurable_set (I : set (ι → ℝ)) :=
+lemma measurable_set_coe : measurable_set (I : set (ι → ℝ)) :=
 begin
   rw [coe_eq_pi],
   haveI := fintype.encodable ι,
   exact measurable_set.univ_pi (λ i, measurable_set_Ioc)
 end
 
-lemma measurable_set_Icc [fintype ι] (I : box ι) : measurable_set I.Icc := measurable_set_Icc
+lemma measurable_set_Icc : measurable_set I.Icc := measurable_set_Icc
 
-lemma measure_Icc_lt_top (μ : measure (ι → ℝ)) [is_locally_finite_measure μ] : μ I.Icc < ∞ :=
-show μ (Icc I.lower I.upper) < ∞, from I.is_compact_Icc.measure_lt_top
+lemma measurable_set_Ioo : measurable_set I.Ioo :=
+(measurable_set_pi (finite.of_fintype _).countable).2 $ or.inl $ λ i hi, measurable_set_Ioo
 
-lemma measure_coe_lt_top (μ : measure (ι → ℝ)) [is_locally_finite_measure μ] : μ I < ∞ :=
-(measure_mono $ coe_subset_Icc).trans_lt (I.measure_Icc_lt_top μ)
+lemma coe_ae_eq_Icc : (I : set (ι → ℝ)) =ᵐ[volume] I.Icc :=
+by { rw coe_eq_pi, exact measure.univ_pi_Ioc_ae_eq_Icc }
+
+lemma Ioo_ae_eq_Icc : I.Ioo =ᵐ[volume] I.Icc :=
+measure.univ_pi_Ioo_ae_eq_Icc
 
 end box