diff --git a/.gitignore b/.gitignore index 2b00952..0827f61 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,2 @@ .lake +*.log diff --git a/Ray/Analytic/Analytic.lean b/Ray/Analytic/Analytic.lean index b2c2be1..b398587 100644 --- a/Ray/Analytic/Analytic.lean +++ b/Ray/Analytic/Analytic.lean @@ -44,7 +44,7 @@ public lemma AnalyticWithinAt.analyticAt {f : E → F} {s : Set E} {x : E} obtain ⟨e, e0, es⟩ := Metric.mem_nhds_iff.mp xs refine ⟨p, min r (.ofReal e), {r_le := by simp [fp.r_le], r_pos := by simp [fp.r_pos, e0], hasSum := fun {y} yr ↦ ?_}⟩ - simp only [EMetric.mem_ball, edist_zero_right, lt_inf_iff] at yr + simp only [Metric.mem_eball, edist_zero_right, lt_inf_iff] at yr obtain ⟨yr, ye⟩ := yr simp only [← ofReal_norm, ENNReal.ofReal_lt_ofReal_iff e0] at ye exact fp.hasSum (.inr (es (by simp [ye]))) (by simp [yr]) @@ -59,12 +59,6 @@ public lemma ContDiffOn.analyticOnNhd {f : E → F} {s : Set E} (fa : ContDiffOn (os : IsOpen s) : AnalyticOnNhd 𝕜 f s := fun x xs ↦ (fa x xs).analyticWithinAt.analyticAt (os.mem_nhds xs) -public lemma AnalyticAt.div_const {f : E → 𝕜} {c : E} (fa : AnalyticAt 𝕜 f c) {w : 𝕜} : - AnalyticAt 𝕜 (fun z ↦ f z / w) c := by - by_cases w0 : w = 0 - · simp only [w0, div_zero, analyticAt_const] - · exact fa.div analyticAt_const w0 - public lemma AnalyticAt.dslope {f : 𝕜 → E} {c x : 𝕜} (fa : AnalyticAt 𝕜 f x) : AnalyticAt 𝕜 (dslope f c) x := by by_cases e : x = c @@ -100,7 +94,7 @@ public theorem orderAt_eq_zero {f : 𝕜 → E} {c : 𝕜} (f0 : f c ≠ 0) : or · rcases fp with ⟨p, fp⟩; rw [fp.orderAt_unique]; rw [← fp.coeff_zero 1] at f0 rw [FormalMultilinearSeries.order_eq_zero_iff']; right contrapose f0 - simp only [f0, ContinuousMultilinearMap.zero_apply] + simp only [f0, _root_.zero_apply] · simp [orderAt, fp] /-- `orderAt = 0` means either `f = 0` or `f c ≠ 0` -/ @@ -143,13 +137,12 @@ public theorem AnalyticAt.leading_approx {f : 𝕜 → E} {c : 𝕜} (fa : Analy simp_rw [← fp.orderAt_unique, hd] at e apply Asymptotics.IsLittleO.of_isBigOWith; intro k kp rw [Asymptotics.isBigOWith_iff] - apply e.mp have dc : ContinuousAt ((Function.swap _root_.dslope c)^[d] f) c := (fp.has_fpower_series_iterate_dslope_fslope d).analyticAt.continuousAt rcases Metric.continuousAt_iff.mp dc k kp with ⟨r, rp, rh⟩ rw [ha'] at rh generalize hg : (Function.swap _root_.dslope c)^[d] f = g; rw [hg] at rh - rw [Metric.eventually_nhds_iff]; use r, rp; intro y yr fe; rw [fe] + rw [Metric.eventually_nhds_iff]; use r, rp; intro y yr; rw [e y, hg] specialize rh yr; rw [dist_eq_norm] at rh calc ‖(y - c) ^ d • g y - (y - c) ^ d • a‖ _ = ‖(y - c) ^ d‖ * ‖g y - a‖ := by rw [←smul_sub, norm_smul] @@ -174,7 +167,8 @@ def FormalMultilinearSeries.unshift' (p : FormalMultilinearSeries 𝕜 𝕜 E) ( lemma FormalMultilinearSeries.unshift_coeff_zero (p : FormalMultilinearSeries 𝕜 𝕜 E) (c : E) : (p.unshift' c).coeff 0 = c := by simp only [FormalMultilinearSeries.coeff, FormalMultilinearSeries.unshift', - FormalMultilinearSeries.unshift, continuousMultilinearCurryFin0_symm_apply] + FormalMultilinearSeries.unshift, continuousMultilinearCurryFin0_symm_apply, + ContinuousMultilinearMap.uncurry0_apply] @[simp] lemma FormalMultilinearSeries.unshift_coeff_succ (p : FormalMultilinearSeries 𝕜 𝕜 E) (c : E) @@ -190,7 +184,7 @@ def FormalMultilinearSeries.unshiftIter (p : FormalMultilinearSeries 𝕜 𝕜 E lemma FormalMultilinearSeries.unshiftIter_coeff (p : FormalMultilinearSeries 𝕜 𝕜 E) (n : ℕ) (i : ℕ) : (p.unshiftIter n).coeff i = if i < n then 0 else p.coeff (i - n) := by revert i; induction' n with n h - · simp only [FormalMultilinearSeries.unshiftIter, Function.iterate_zero, id_eq, not_lt_zero', + · simp only [FormalMultilinearSeries.unshiftIter, Function.iterate_zero, id_eq, not_lt_zero, tsub_zero, if_false, forall_const] · simp_rw [FormalMultilinearSeries.unshiftIter] at h simp only [FormalMultilinearSeries.unshiftIter, Function.iterate_succ', Function.comp] @@ -278,7 +272,7 @@ public theorem AnalyticAt.monomial_mul_orderAt {f : 𝕜 → E} {c : 𝕜} (fa : have pnz : p ≠ 0 := by contrapose fnz simpa only [HasFPowerSeriesAt.locally_zero_iff fp, Filter.not_frequently, not_not] - have pe : ∃ i, p i ≠ 0 := by rw [Function.ne_iff] at pnz; exact pnz + have pe : ∃ i, p i ≠ 0 := by contrapose! pnz; exact FormalMultilinearSeries.ext pnz have pne : ∃ i, (p.unshiftIter n) i ≠ 0 := by rcases pe with ⟨i, pi⟩; use n + i simp only [FormalMultilinearSeries.ne_zero_iff_coeff_ne_zero] at pi ⊢ @@ -290,7 +284,7 @@ public theorem AnalyticAt.monomial_mul_orderAt {f : 𝕜 → E} {c : 𝕜} (fa : · have s := Nat.find_spec pe simp only [← p.coeff_eq_zero, Ne] at s simp only [p.unshiftIter_coeff, ← FormalMultilinearSeries.coeff_eq_zero, s, Ne, - add_lt_iff_neg_left, not_lt_zero', add_tsub_cancel_left, if_false, not_false_iff] + add_lt_iff_neg_left, not_lt_zero, add_tsub_cancel_left, if_false, not_false_iff] · intro m mp; simp [← FormalMultilinearSeries.coeff_eq_zero, p.unshiftIter_coeff]; intro mn generalize ha : m - n = a; have hm : m = n + a := by rw [← ha, add_comm, Nat.sub_add_cancel mn] simp only [hm, add_lt_add_iff_left, Nat.lt_find_iff, not_not] at mp @@ -340,8 +334,10 @@ public theorem AnalyticAt.deriv2 [CompleteSpace 𝕜] {f : E → 𝕜 → 𝕜} /-- Scaling commutes with power series -/ theorem HasFPowerSeriesAt.const_fun_smul {f : 𝕜 → E} {c a : 𝕜} {p : FormalMultilinearSeries 𝕜 𝕜 E} (fp : HasFPowerSeriesAt f p c) : HasFPowerSeriesAt (fun z ↦ a • f z) (fun n ↦ a • p n) c := by + show HasFPowerSeriesAt (fun z ↦ a • f z) (a • p) c rw [hasFPowerSeriesAt_iff] at fp ⊢; refine fp.mp (.of_forall fun z h ↦ ?_) - simp only [FormalMultilinearSeries.coeff, ContinuousMultilinearMap.smul_apply, smul_comm _ a] + simp only [FormalMultilinearSeries.coeff, FormalMultilinearSeries.smul_apply, + _root_.smul_apply, smul_comm _ a] exact h.const_smul a /-- Nonzero scaling does not change analyticitiy -/ @@ -390,7 +386,7 @@ public theorem leadingCoeff_const_smul {f : 𝕜 → E} {c a : 𝕜} : simp only [Function.iterate_succ_apply', h, hg] funext x; simp only [Function.swap] by_cases cx : x = c - · simp only [cx, dslope_same, Pi.smul_apply, Pi.smul_def, deriv_fun_const_smul'] + · simp only [cx, dslope_same, Pi.smul_apply, Pi.smul_def, deriv_fun_const_smul_field] · simp only [dslope_of_ne _ cx, Pi.smul_apply, slope, vsub_eq_sub, ← smul_sub, smul_comm _ a] simp only [e, Pi.smul_apply] diff --git a/Ray/Analytic/ConjConj.lean b/Ray/Analytic/ConjConj.lean index 27f2c2a..69485df 100644 --- a/Ray/Analytic/ConjConj.lean +++ b/Ray/Analytic/ConjConj.lean @@ -41,7 +41,7 @@ lemma HasFPowerSeriesOnBall.conj_conj (fa : HasFPowerSeriesOnBall f p (conj z) r r_pos := fa.r_pos hasSum := by intro y m - simp only [EMetric.mem_ball, edist_zero_right] at m + simp only [Metric.mem_eball, edist_zero_right] at m simpa only [FormalMultilinearSeries.conj_conj, ContinuousMultilinearMap.conj_conj_apply, map_add, conjCLM_apply] using conjCLM.hasSum (@fa.hasSum (conj y) (by simpa)) diff --git a/Ray/Analytic/Holomorphic.lean b/Ray/Analytic/Holomorphic.lean index 0ab6ac1..b410815 100644 --- a/Ray/Analytic/Holomorphic.lean +++ b/Ray/Analytic/Holomorphic.lean @@ -71,17 +71,17 @@ public theorem contDiffAt_iff_analytic_at2 {E : Type} {f : ℂ × ℂ → E} {x /-- If `f` is analytic in an open ball, it has a power series over that ball -/ public lemma analyticOnNhd_ball_iff_hasFPowerSeriesOnBall {f : ℂ → E} {c : ℂ} {r : ℝ≥0∞} (r0 : 0 < r) : - AnalyticOnNhd ℂ f (EMetric.ball c r) ↔ + AnalyticOnNhd ℂ f (Metric.eball c r) ↔ ∃ p : FormalMultilinearSeries ℂ ℂ E, HasFPowerSeriesOnBall f p c r := by constructor · intro a - obtain ⟨p,s,hs⟩ := a c (by simp only [EMetric.mem_ball, edist_self, r0]) + obtain ⟨p,s,hs⟩ := a c (by simp only [Metric.mem_eball, edist_self, r0]) have grow : ∀ t : ℝ≥0, 0 < t → t < r → HasFPowerSeriesOnBall f p c t := by intro t t0 tr have d : DifferentiableOn ℂ f (closedBall c t) := by apply (a.mono ?_).differentiableOn intro x m - simp only [Metric.mem_closedBall, dist_le_coe, EMetric.mem_ball, + simp only [Metric.mem_closedBall, dist_le_coe, Metric.mem_eball, ← ENNReal.coe_le_coe, ← edist_nndist] at m ⊢ order have ht := d.hasFPowerSeriesOnBall t0 @@ -89,13 +89,13 @@ public lemma analyticOnNhd_ball_iff_hasFPowerSeriesOnBall {f : ℂ → E} {c : refine ⟨p, ?_, r0, ?_⟩ · exact ENNReal.le_of_forall_pos_nnreal_lt fun t t0 tr ↦ (grow t t0 tr).r_le · intro y yr - simp only [EMetric.mem_ball, edist_zero_right] at yr + simp only [Metric.mem_eball, edist_zero_right] at yr obtain ⟨t,yt,tr⟩ := ENNReal.lt_iff_exists_nnreal_btwn.mp yr have t0 : 0 < t := by simp only [enorm_eq_nnnorm, ENNReal.coe_lt_coe] at yt exact pos_of_gt yt refine (grow t t0 tr).hasSum ?_ - simp only [Metric.emetric_ball_nnreal, Metric.mem_ball, dist_zero_right] + simp only [Metric.eball_coe, Metric.mem_ball, dist_zero_right] simpa only [← ofReal_norm, ENNReal.ofReal_lt_coe_iff, norm_nonneg] using yt · intro ⟨p,a⟩ exact a.analyticOnNhd diff --git a/Ray/Analytic/Integral.lean b/Ray/Analytic/Integral.lean index cc542c8..f8c0d81 100644 --- a/Ray/Analytic/Integral.lean +++ b/Ray/Analytic/Integral.lean @@ -190,7 +190,7 @@ theorem hasFPowerSeriesOnBall_integral (i : Holo f μ s c r) : simp only [series, ContinuousMultilinearMap.integral_apply i.integrableOn_cauchyPowerSeries] apply MeasureTheory.hasSum_integral_of_summable_integral_norm · exact fun _ ↦ i.integrableOn_cauchyPowerSeries_apply - · simp only [Metric.emetric_ball_nnreal, Metric.mem_ball, dist_zero_right] at ym + · simp only [Metric.eball_coe, Metric.mem_ball, dist_zero_right] at ym exact i.summable_cauchyPowerSeries_apply ym end Holo @@ -205,7 +205,7 @@ theorem AnalyticOnNhd.integral_ball {r : ℝ} (fc : ContinuousOn (uncurry f) (s (μs : μ s ≠ ⊤ := by finiteness) : AnalyticOnNhd ℂ (fun z ↦ ∫ x in s, f x z ∂μ) (ball c r) := by set r' : ℝ≥0 := ⟨r, r0.le⟩ set i : Holo f μ s c r' := ⟨r0, sc, μs, fc, fd⟩ - have e : ball c r = EMetric.ball c r' := by simp [r'] + have e : ball c r = Metric.eball c r' := by rw [Metric.eball_coe]; rfl rw [e] exact i.hasFPowerSeriesOnBall_integral.analyticOnNhd diff --git a/Ray/Analytic/Products.lean b/Ray/Analytic/Products.lean index 2770a30..95bc675 100644 --- a/Ray/Analytic/Products.lean +++ b/Ray/Analytic/Products.lean @@ -52,36 +52,51 @@ public theorem product_pow' {f : ℕ → ℂ} {p : ℕ} (h : ProdExists f) : tprod f ^ p = tprod fun n ↦ f n ^ p := by rcases h with ⟨g, h⟩; rw [HasProd.tprod_eq h]; rw [HasProd.tprod_eq _]; exact product_pow p h -/-- Adding one more term to a product multiplies by it -/ -theorem product_cons {a g : ℂ} {f : ℕ → ℂ} (h : HasProd f g) : - HasProd (Stream'.cons a f) (a * g) := by +/-- Adding one more term to a product multiplies by it, `Stream'.get` version to keep terms + type-correct at low transparency -/ +theorem product_cons_get {a t : ℂ} {q : Stream' ℂ} (h : HasProd q.get t) : + HasProd (Stream'.cons a q).get (a * t) := by rw [HasProd] at h ⊢ - have ha := Filter.Tendsto.comp (Continuous.tendsto (continuous_mul_left a) g) h - have s : ((fun z ↦ a * z) ∘ fun N : Finset ℕ ↦ N.prod f) = - (fun N : Finset ℕ ↦ N.prod (Stream'.cons a f)) ∘ push := by - apply funext; intro N; simp; exact push_prod + have ha := Filter.Tendsto.comp (Continuous.tendsto (continuous_const_mul a) t) h + have s : ((fun z ↦ a * z) ∘ fun N : Finset ℕ ↦ N.prod q.get) = + (fun N : Finset ℕ ↦ N.prod (Stream'.cons a q).get) ∘ push := by + apply funext; intro N + simp only [Function.comp_apply] + exact push_prod_get rw [s] at ha exact tendsto_comp_push.mp ha +/-- Adding one more term to a product multiplies by it -/ +theorem product_cons {a g : ℂ} {f : ℕ → ℂ} (h : HasProd f g) : + HasProd (Stream'.cons a f) (a * g) := + product_cons_get (q := f) h + /-- Adding one more term to a product multiplies by it (`tprod` version) -/ theorem product_cons' {a : ℂ} {f : ℕ → ℂ} (h : ProdExists f) : tprod (Stream'.cons a f) = a * tprod f := by - rcases h with ⟨g, h⟩; rw [HasProd.tprod_eq h]; rw [HasProd.tprod_eq _]; exact product_cons h + rcases h with ⟨g, h⟩; rw [HasProd.tprod_eq h]; exact HasProd.tprod_eq (product_cons h) -/-- Dropping a nonzero term divides by it -/ -theorem product_drop {f : ℕ → ℂ} {g : ℂ} (f0 : f 0 ≠ 0) (h : HasProd f g) : - HasProd (fun n ↦ f (n + 1)) (g / f 0) := by - have c := @product_cons (f 0)⁻¹ _ _ h +/-- Dropping a nonzero term divides by it, `Stream'.get` version -/ +theorem product_drop_get {q : Stream' ℂ} {t : ℂ} (q0 : q.head ≠ 0) (h : HasProd q.get t) : + HasProd q.tail.get (t / q.head) := by + have c := product_cons_get (a := q.head⁻¹) h rw [HasProd] rw [inv_mul_eq_div, HasProd, SummationFilter.unconditional_filter, ← tendsto_comp_push, ← tendsto_comp_push] at c - have s : ((fun N : Finset ℕ ↦ N.prod fun n ↦ (Stream'.cons (f 0)⁻¹ f) n) ∘ push) ∘ push = - fun N : Finset ℕ ↦ N.prod fun n ↦ f (n + 1) := by - clear c h g; apply funext; intro N; simp - nth_rw 2 [← Stream'.eta f] - simp only [←push_prod, Stream'.head, Stream'.tail, Stream'.get, ←mul_assoc, inv_mul_cancel₀ f0, - one_mul] - rw [s] at c; assumption + have s : ((fun N : Finset ℕ ↦ N.prod (Stream'.cons q.head⁻¹ q).get) ∘ push) ∘ push = + fun N : Finset ℕ ↦ N.prod q.tail.get := by + apply funext; intro N + simp only [Function.comp_apply] + have e1 := push_prod_get (a := q.head⁻¹) (g := q) (N := push N) + have e2 := push_prod_get (a := q.head) (g := q.tail) (N := N) + rw [Stream'.eta q] at e2 + rw [← e1, ← e2, ← mul_assoc, inv_mul_cancel₀ q0, one_mul] + rw [s] at c; exact c + +/-- Dropping a nonzero term divides by it -/ +theorem product_drop {f : ℕ → ℂ} {g : ℂ} (f0 : f 0 ≠ 0) (h : HasProd f g) : + HasProd (fun n ↦ f (n + 1)) (g / f 0) := + product_drop_get (q := f) f0 h /-- Dropping a nonzero term divides by it (`tprod` version) -/ theorem product_drop' {f : ℕ → ℂ} (f0 : f 0 ≠ 0) (h : ProdExists f) : diff --git a/Ray/Analytic/Series.lean b/Ray/Analytic/Series.lean index 4aa10e5..4c5cdf7 100644 --- a/Ray/Analytic/Series.lean +++ b/Ray/Analytic/Series.lean @@ -66,36 +66,35 @@ theorem CNonpos.degenerate {f : ℕ → ℂ → G} {s : Set ℂ} {c a : ℝ} (c0 have ca : c * a ^ n ≤ 0 := mul_nonpos_iff.mpr (Or.inr ⟨c0, by bound⟩) exact norm_eq_zero.mp (le_antisymm (le_trans hf ca) (norm_nonneg _)) -/-- Adding one more term to a sum adds it -/ -theorem sum_cons {a g : G} {f : ℕ → G} (h : HasSum f g) : - HasSum (Stream'.cons a f) (a + g) := by +/-- Adding one more term to a sum adds it, `Stream'.get` version to keep terms type-correct + at low transparency -/ +theorem sum_cons_get {a t : G} {q : Stream' G} (h : HasSum q.get t) : + HasSum (Stream'.cons a q).get (a + t) := by rw [HasSum] at h ⊢ - have ha := Filter.Tendsto.comp (Continuous.tendsto (continuous_add_left a) g) h - have s : ((fun z ↦ a + z) ∘ fun N : Finset ℕ ↦ N.sum f) = - (fun N : Finset ℕ ↦ N.sum (Stream'.cons a f)) ∘ push := by - apply funext; intro N; simp; exact push_sum + have ha := Filter.Tendsto.comp (Continuous.tendsto (continuous_const_add a) t) h + have s : ((fun z ↦ a + z) ∘ fun N : Finset ℕ ↦ N.sum q.get) = + (fun N : Finset ℕ ↦ N.sum (Stream'.cons a q).get) ∘ push := by + apply funext; intro N + simp only [Function.comp_apply] + exact push_sum_get rw [s] at ha exact tendsto_comp_push.mp ha +/-- Adding one more term to a sum adds it -/ +theorem sum_cons {a g : G} {f : ℕ → G} (h : HasSum f g) : + HasSum (Stream'.cons a f) (a + g) := + sum_cons_get (q := f) h + /-- Adding one more term to a sum adds it (`tprod` version) -/ lemma sum_cons' {a : G} {f : ℕ → G} (h : Summable f) : tsum (Stream'.cons a f) = a + tsum f := by - rcases h with ⟨g, h⟩; rw [HasSum.tsum_eq h]; rw [HasSum.tsum_eq _]; exact sum_cons h + rcases h with ⟨g, h⟩; rw [HasSum.tsum_eq h]; exact HasSum.tsum_eq (sum_cons h) /-- Dropping the first term subtracts it -/ public lemma sum_drop {f : ℕ → G} {g : G} (h : HasSum f g) : HasSum (fun n ↦ f (n + 1)) (g - f 0) := by - have c := sum_cons (a := -f 0) h - rw [HasSum] - rw [neg_add_eq_sub, HasSum, SummationFilter.unconditional_filter, ← tendsto_comp_push, - ← tendsto_comp_push] at c - have s : ((fun N : Finset ℕ ↦ N.sum fun n ↦ (Stream'.cons (-f 0) f) n) ∘ push) ∘ push = - fun N : Finset ℕ ↦ N.sum fun n ↦ f (n + 1) := by - clear c h g; apply funext; intro N; simp - nth_rw 2 [← Stream'.eta f] - simp only [←push_sum, Stream'.head, Stream'.tail, Stream'.get] - abel - rw [s] at c; assumption + rw [hasSum_nat_add_iff (f := f) 1] + simpa using h /-- Dropping the first term subtracts it (`tsum` version) -/ public lemma tsum_drop {f : ℕ → G} (h : Summable f) : @@ -153,7 +152,7 @@ theorem uniformVanishing_to_tendsto_uniformly_on {f : ℕ → ℂ → G} {s : Se theorem fast_series_converge_uniformly_on {f : ℕ → ℂ → G} {s : Set ℂ} {c a : ℝ} (a0 : 0 ≤ a) (a1 : a < 1) (hf : ∀ n z, z ∈ s → ‖f n z‖ ≤ c * a ^ n) : HasUniformSum f (tsumOn f) s := by by_cases c0 : c ≤ 0 - · have fz := CNonpos.degenerate c0 a0 hf; simp only at fz + · have fz := CNonpos.degenerate c0 a0 hf rw [HasUniformSum, Metric.tendstoUniformlyOn_iff] intro e ep; refine .of_forall ?_; intro n z zs rw [tsumOn] @@ -187,7 +186,6 @@ theorem fast_series_converge_at {f : ℕ → G} {c a : ℝ} (a0 : 0 ≤ a) (a1 : set g : ℕ → ℂ → G := fun n _ ↦ f n have hg : ∀ n z, z ∈ s → ‖g n z‖ ≤ c * a ^ n := fun n z _ ↦ hf n have u := fast_series_converge_uniformly_on a0 a1 hg - simp at u rw [HasUniformSum] at u rw [tendstoUniformlyOn_singleton_iff_tendsto] at u apply HasSum.summable; assumption diff --git a/Ray/Analytic/Uniform.lean b/Ray/Analytic/Uniform.lean index 0e8d02b..b714a88 100644 --- a/Ray/Analytic/Uniform.lean +++ b/Ray/Analytic/Uniform.lean @@ -26,7 +26,7 @@ theorem analyticOn_small_cball {f : ℂ → E} {z : ℂ} {r : ℝ≥0} (h : Anal intro x hx rw [closedBall] at hx; simp at hx have hb : x ∈ ball z r := by - rw [ball]; simp only [dist_lt_coe, Set.mem_setOf_eq]; exact lt_of_le_of_lt hx sr + rw [ball]; simp only [dist_lt_coe, Set.mem_ofPred_eq]; exact lt_of_le_of_lt hx sr exact h x hb theorem cauchy_bound {f : ℂ → E} {c : ℂ} {r : ℝ≥0} {d : ℝ≥0} {w : ℂ} {n : ℕ} (rp : r > 0) @@ -77,7 +77,7 @@ theorem circleIntegral_sub {f g : ℂ → E} {c : ℂ} {r : ℝ} (fi : CircleInt theorem circleMap_nz {c : ℂ} {r : ℝ≥0} {θ : ℝ} (rp : r > 0) : circleMap c r θ - c ≠ 0 := by simp only [circleMap_sub_center, Ne, circleMap_eq_center_iff, NNReal.coe_eq_zero] - intro h; rw [h] at rp; simp only [gt_iff_lt, not_lt_zero'] at rp + intro h; rw [h] at rp; simp only [gt_iff_lt, not_lt_zero] at rp theorem cauchy_is_circleIntegrable {f : ℂ → E} {c : ℂ} {r : ℝ≥0} (n : ℕ) (w : ℂ) (rp : r > 0) (h : ContinuousOn f (closedBall c r)) : @@ -158,7 +158,7 @@ theorem analyticOn_ball_radius {f : ℂ → E} {z : ℂ} {r : ℝ≥0} (rp : r > rw [← pp] at hp' refine hp'.r_le · intro y yr - rw [EMetric.ball, Set.mem_setOf] at yr + rw [Metric.mem_eball] at yr rcases exists_between yr with ⟨t, t0, t1⟩ have t1' : t.toNNReal < r := by rw [← WithTop.coe_lt_coe]; exact lt_of_le_of_lt ENNReal.coe_toNNReal_le_self t1 @@ -170,7 +170,7 @@ theorem analyticOn_ball_radius {f : ℂ → E} {z : ℂ} {r : ℝ≥0} (rp : r > HasFPowerSeriesAt.eq_formalMultilinearSeries ⟨↑(r / 2), ph⟩ ⟨t.toNNReal, hp'⟩ rw [← pp] at hp' refine hp'.hasSum ?_ - rw [EMetric.ball, Set.mem_setOf] + rw [Metric.mem_eball] calc edist y 0 _ < t := t0 _ = ↑t.toNNReal := (ENNReal.coe_toNNReal <| ne_top_of_lt t1).symm diff --git a/Ray/Dynamics/Bottcher.lean b/Ray/Dynamics/Bottcher.lean index 429870b..8f916b7 100644 --- a/Ray/Dynamics/Bottcher.lean +++ b/Ray/Dynamics/Bottcher.lean @@ -207,7 +207,7 @@ public theorem Super.bottcher_eqn (s : Super f d a) [OnePreimage s] : have fc := (s.fa (c, a)).along_snd.continuousAt; simp only [ContinuousAt, s.f0] at fc apply e.mp; apply (fc.eventually e).mp apply ((s.isOpen_near.snd_preimage c).eventually_mem (s.mem_near c)).mp - refine .of_forall fun w m e0 e1 ↦ ?_; simp only at m e0 e1 + refine .of_forall fun w m e0 e1 ↦ ?_ simp only [e0, e1]; exact s.bottcherNear_eqn m by_cases p : (c, z) ∈ s.post; simp only [h0 p] by_cases m : (c, z) ∈ s.basin @@ -263,7 +263,7 @@ public theorem Super.norm_bottcher (s : Super f d a) [OnePreimage s] : public theorem Super.bottcher_lt_one (s : Super f d a) [OnePreimage s] (m : (c, z) ∈ s.post) : ‖s.bottcher c z‖ < 1 := by replace m := s.bottcher_ext m - simp only [Super.ext, mem_setOf] at m + simp only [Super.ext, mem_ofPred] at m exact lt_of_lt_of_le m s.p_le_one /-- Functional equation for `s.ray` -/ @@ -277,7 +277,7 @@ omit [T3Space S] in /-- Raising to powers stays in `s.ext` -/ public lemma Super.pow_ext (s : Super f d a) [OnePreimage s] (post : (c, x) ∈ s.ext) (n : ℕ) : (c, x ^ d ^ n) ∈ s.ext := by - simp only [ext, mem_setOf_eq, norm_pow] at post ⊢ + simp only [ext, mem_ofPred_eq, norm_pow] at post ⊢ refine lt_of_le_of_lt (pow_le_of_le_one (by bound) ?_ (by simp [s.d0])) post exact le_trans post.le s.p_le_one diff --git a/Ray/Dynamics/BottcherNear.lean b/Ray/Dynamics/BottcherNear.lean index 6a37806..ae4e70b 100644 --- a/Ray/Dynamics/BottcherNear.lean +++ b/Ray/Dynamics/BottcherNear.lean @@ -108,14 +108,14 @@ theorem SuperAt.ga_of_fa (s : SuperAt f d) {c : ℂ} (fa : AnalyticAt ℂ f c) : suffices h : AnalyticOnNhd ℂ (g f d) t by rw [← ht] at h; exact h _ (mem_ball_self rp) have ga : DifferentiableOn ℂ (g f d) (t \ {0}) := by have e : ∀ z : ℂ, z ∈ t \ {0} → g f d z = f z / z ^ d := by - intro z zs; simp only [Set.mem_diff, Set.mem_singleton_iff] at zs + intro z zs; simp only [Set.mem_sdiff, Set.mem_singleton_iff] at zs simp only [g, zs.2, if_false] rw [differentiableOn_congr e] - apply DifferentiableOn.div (fa.mono diff_subset).differentiableOn + apply DifferentiableOn.div (fa.mono sdiff_subset).differentiableOn exact (Differentiable.pow differentiable_id _).differentiableOn - intro z zs; exact pow_ne_zero _ (Set.mem_diff_singleton.mp zs).2 + intro z zs; exact pow_ne_zero _ (Set.mem_sdiff_singleton.mp zs).2 rw [Complex.analyticOnNhd_iff_differentiableOn o] - by_cases t0 : (0 : ℂ) ∉ t; · rw [Set.diff_singleton_eq_self t0] at ga; exact ga + by_cases t0 : (0 : ℂ) ∉ t; · rw [Set.sdiff_singleton_eq_self t0] at ga; exact ga simp only [Set.not_notMem] at t0 have gc : ContinuousAt (g f d) 0 := by rw [Metric.continuousAt_iff]; intro e ep @@ -539,7 +539,7 @@ theorem SuperNearC.union {I : Type} {u : I → Set ℂ} {t : I → Set (ℂ × have sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u a b := by intro c z m; rcases Set.mem_iUnion.mp m with ⟨i, m⟩; use{z | (c, z) ∈ t i} - simp only [Set.mem_setOf_eq, m, Set.mem_iUnion, Set.setOf_subset_setOf, true_and, tu] + simp only [Set.mem_ofPred_eq, m, Set.mem_iUnion, Set.ofPred_subset_ofPred, true_and, tu] constructor · exact fun z m ↦ ⟨i, m⟩ · exact (s i).s ((s i).tc m) @@ -622,7 +622,7 @@ public theorem SuperAtC.superNearC' (s : SuperAtC f d u) {w : Set (ℂ × ℂ)} apply Set.iUnion_subset; intro i; rcases choose_spec (h _ i.mem) with ⟨_, _, rw, _⟩; exact rw have si : ∀ c : u, SuperNearC f d (v c) (t c) (1 / 2) (1 / 4) := by intro i; rcases choose_spec (h _ i.mem) with ⟨_, _, _, s⟩; exact s - have s := SuperNearC.union si; simp only at s; rw [← e] at s + have s := SuperNearC.union si; rw [← e] at s exact ⟨tw, s⟩ /-- `SuperAtC → SuperNearC` -/ diff --git a/Ray/Dynamics/BottcherNearM.lean b/Ray/Dynamics/BottcherNearM.lean index ef00e86..10ef138 100644 --- a/Ray/Dynamics/BottcherNearM.lean +++ b/Ray/Dynamics/BottcherNearM.lean @@ -75,15 +75,15 @@ public theorem Super.fla (s : Super f d a) (c : ℂ) : AnalyticAt ℂ (uncurry s refine ((analyticAt_id.sub analyticAt_const).mAnalyticAt I I).comp _ ?_ refine (contMDiffAt_extChartAt' ?_).comp _ ?_ · simp only [s.f0, extChartAt, OpenPartialHomeomorph.extend, PartialEquiv.coe_trans, zero_add, - ModelWithCorners.toPartialEquiv_coe, OpenPartialHomeomorph.coe_coe, Function.comp_apply, - PartialEquiv.coe_trans_symm, OpenPartialHomeomorph.coe_coe_symm, + ModelWithCorners.toPartialEquiv_coe, OpenPartialHomeomorph.coe_toPartialEquiv, Function.comp_apply, + PartialEquiv.coe_trans_symm, OpenPartialHomeomorph.coe_toPartialEquiv_symm, ModelWithCorners.toPartialEquiv_coe_symm, ModelWithCorners.left_inv, OpenPartialHomeomorph.left_inv, mem_chart_source] · refine (s.fa _).comp₂ contMDiffAt_fst ?_ refine ((contMDiffOn_extChartAt_symm _).contMDiffAt (extChartAt_target_mem_nhds' ?_)).comp _ ?_ · simp only [extChartAt, OpenPartialHomeomorph.extend, PartialEquiv.coe_trans, zero_add, - ModelWithCorners.toPartialEquiv_coe, OpenPartialHomeomorph.coe_coe, Function.comp_apply, + ModelWithCorners.toPartialEquiv_coe, OpenPartialHomeomorph.coe_toPartialEquiv, Function.comp_apply, PartialEquiv.trans_target, ModelWithCorners.target_eq, ModelWithCorners.toPartialEquiv_coe_symm, Set.mem_inter_iff, Set.mem_range_self, Set.mem_preimage, ModelWithCorners.left_inv, OpenPartialHomeomorph.map_source, @@ -142,13 +142,13 @@ theorem Super.critical_0 (s : Super f d a) (c : ℂ) : Critical (s.fl c) 0 := by simp only [sub_zero, smul_eq_mul, Super.fl, s.fd, s.fc, mul_one, uncurry] at p generalize hg : _root_.fl f a c = g; rw [hg] at p have g0 : g 0 = 0 := by rw [← hg]; exact s.fl0 - apply HasFDerivAt.fderiv + apply HasFDerivAt.fderiv (f' := (0 : ℂ →L[ℂ] ℂ)) simp only [hasFDerivAt_iff_isLittleO_nhds_zero, sub_zero, zero_add, g0] have od : (fun z : ℂ ↦ z ^ d) =o[𝓝 0] (fun z ↦ z) := by rw [Asymptotics.isLittleO_iff]; intro e ep apply ((@Metric.isOpen_ball ℂ _ 0 (min 1 e)).eventually_mem (mem_ball_self (by bound))).mp refine .of_forall fun z b ↦ ?_ - simp only at b; rw [mem_ball_zero_iff, lt_min_iff] at b + rw [mem_ball_zero_iff, lt_min_iff] at b simp only [norm_pow] rw [← Nat.sub_add_cancel s.d2, pow_add, pow_two] calc ‖z‖ ^ (d - 2) * (‖z‖ * ‖z‖) @@ -293,7 +293,7 @@ public theorem Super.isOpen_near (s : Super f d a) : IsOpen s.near := by @[simp] public theorem Super.mem_near (s : Super f d a) (c : ℂ) : (c, a) ∈ s.near := by simp only [Super.near, extChartAt_prod, PartialEquiv.prod_source, Set.mem_prod, Set.mem_inter_iff, mem_extChartAt_source, extChartAt_eq_refl, PartialEquiv.refl_source, Set.mem_univ, true_and, - Set.mem_preimage, PartialEquiv.prod_coe, PartialEquiv.refl_coe, id, Set.mem_setOf_eq, sub_self] + Set.mem_preimage, PartialEquiv.prod_coe, PartialEquiv.refl_coe, id, Set.mem_ofPred_eq, sub_self] exact (s.superNearC.s (Set.mem_univ _)).t0 /-- `s.near` stays within the chart -/ @@ -315,7 +315,7 @@ public theorem Super.stays_near (s : Super f d a) {c : ℂ} {z : S} (m : (c, z) (c, f c z) ∈ s.near := by simp only [Super.near, extChartAt_prod, PartialEquiv.prod_source, Set.mem_prod, Set.mem_inter_iff, extChartAt_eq_refl, PartialEquiv.refl_source, Set.mem_univ, true_and, Set.mem_preimage, - PartialEquiv.prod_coe, PartialEquiv.refl_coe, id, Set.mem_setOf_eq] at m ⊢ + PartialEquiv.prod_coe, PartialEquiv.refl_coe, id, Set.mem_ofPred_eq] at m ⊢ rcases mem_iUnion.mp (s.near_subset' m.2) with ⟨b, mb⟩ simp only [mem_ball_iff_norm, Prod.norm_def, max_lt_iff, Prod.fst_sub, Prod.snd_sub, sub_zero] at mb @@ -380,7 +380,7 @@ public lemma Super.basin_iff_near (s : Super f d a) {p : ℂ × S} : p ∈ s.basin ↔ ∃ n, (p.1, (f p.1)^[n] p.2) ∈ s.near := by constructor · intro m - simp only [basin, mem_setOf_eq] at m + simp only [basin, mem_ofPred_eq] at m have e : ∀ᶠ n in atTop, (f p.1)^[n] p.2 ∈ {x : S | (p.1, x) ∈ s.near} := m.eventually_mem ((s.isOpen_near.snd_preimage p.1).mem_nhds (by simp)) exact e.exists @@ -524,8 +524,12 @@ public theorem Super.bottcherNear_mfderiv_ne_zero (s : Super f d a) (c : ℂ) : exact ContinuousLinearMap.smulRight_ne_zero ContinuousLinearMap.one_ne_zero (by norm_num) · have u : (fun z : S ↦ extChartAt I a z - extChartAt I a a) = extChartAt I a - fun _ : S ↦ extChartAt I a a := rfl - rw [u, mfderiv_sub, mfderiv_const, sub_zero] - · exact extChartAt_mderiv_ne_zero a + rw [u, mfderiv_sub, mfderiv_const] + · intro h + apply extChartAt_mderiv_ne_zero a + apply ContinuousLinearMap.ext + intro v + exact (sub_zero _).symm.trans (ContinuousLinearMap.ext_iff.mp h v) · exact (contMDiffAt_extChartAt' (mem_chart_source _ a)).mdifferentiableAt one_ne_zero · apply mdifferentiableAt_const @@ -593,9 +597,9 @@ public theorem Super.isClosed_critical_not_a (s : Super f d a) : rw [← isOpen_compl_iff]; rw [isOpen_iff_eventually]; intro ⟨c, z⟩ m by_cases za : z = a · rw [za]; refine (s.f_noncritical_near_a c).mp (.of_forall ?_); intro ⟨e, w⟩ h - simp only [mem_compl_iff, mem_setOf, not_and, not_not] at h ⊢; exact h.1 + simp only [mem_compl_iff, mem_ofPred, not_and, not_not] at h ⊢; exact h.1 · have o := isOpen_iff_eventually.mp (isOpen_noncritical s.fa) - simp only [za, mem_compl_iff, mem_setOf, not_and, not_not, imp_false] at m o ⊢ + simp only [za, mem_compl_iff, mem_ofPred, not_and, not_not, imp_false] at m o ⊢ refine (o (c, z) m).mp (.of_forall ?_); intro ⟨e, w⟩ a b; exfalso; exact a b /-- If `z ∈ s.basin`, iterating enough takes us to a noncritical point of `s.bottcherNear` -/ diff --git a/Ray/Dynamics/Grow.lean b/Ray/Dynamics/Grow.lean index c0732f5..5f317de 100644 --- a/Ray/Dynamics/Grow.lean +++ b/Ray/Dynamics/Grow.lean @@ -141,7 +141,7 @@ theorem domain_open' {p : ℝ} {t : Set ℂ} (sub : closedBall (0 : ℂ) p ⊆ t ∃ q, p < q ∧ closedBall 0 q ⊆ t := by set u := norm '' (closedBall 0 (p + 1) \ t) by_cases ne : u = ∅ - · refine ⟨p + 1, by bound, ?_⟩; rw [image_eq_empty, diff_eq_empty] at ne; exact ne + · refine ⟨p + 1, by bound, ?_⟩; rw [image_eq_empty, sdiff_eq_empty] at ne; exact ne replace ne := nonempty_iff_ne_empty.mpr ne have uc : IsClosed u := (((isCompact_closedBall _ _).diff ot).image continuous_norm).isClosed @@ -156,16 +156,16 @@ theorem domain_open' {p : ℝ} {t : Set ℂ} (sub : closedBall (0 : ℂ) p ⊆ t intro z m; simp only [mem_closedBall, Complex.dist_eq, sub_zero, le_min_iff] at m rcases m with ⟨zq, zp⟩; have zi := lt_of_le_of_lt zq qi contrapose zi; simp only [not_lt]; refine csInf_le ub (mem_image_of_mem _ ?_) - simp only [mem_diff, mem_closedBall, Complex.dist_eq, sub_zero]; use zp, zi + simp only [mem_sdiff, mem_closedBall, Complex.dist_eq, sub_zero]; use zp, zi /-- If `{c} ×ˢ closedBall 0 p ⊆ t`, we can increase `p` bit without leaving `t` -/ theorem domain_open {p : ℝ} {t : Set (ℂ × ℂ)} (sub : {c} ×ˢ closedBall 0 p ⊆ t) (o : IsOpen t) : ∃ q, p < q ∧ {c} ×ˢ closedBall 0 q ⊆ t := by have sub : closedBall 0 p ⊆ {b | (c, b) ∈ t} := by - intro z m; simp only [mem_setOf]; apply sub; exact ⟨mem_singleton _, m⟩ + intro z m; simp only [mem_ofPred]; apply sub; exact ⟨mem_singleton _, m⟩ rcases domain_open' sub (o.snd_preimage c) with ⟨q, pq, sub⟩ use q, pq; intro ⟨e, z⟩ ⟨ec, m⟩; simp only [mem_singleton_iff] at ec - replace m := sub m; simp only [← ec, mem_setOf] at m; exact m + replace m := sub m; simp only [← ec, mem_ofPred] at m; exact m /-- `Grow` is local -/ theorem Grow.congr {r0 r1 : ℂ → ℂ → S} (g : Grow s c p n r0) @@ -205,9 +205,10 @@ theorem eqn_noncritical {x : ℂ × ℂ} (e : ∀ᶠ y in 𝓝 x, Eqn s n r y) ( (.of_forall fun _ e ↦ e.eqn) rw [mfderiv_eq_fderiv, loc.fderiv_eq] at x0 have d := (differentiableAt_pow (𝕜 := ℂ) (x := x) (d ^ n)).hasFDerivAt.hasDerivAt.deriv - apply_fun (fun x ↦ x 1) at x0 + replace x0 := ContinuousLinearMap.ext_iff.mp x0 1 rw [x0] at d - replace d := Eq.trans d (ContinuousLinearMap.zero_apply _) + have z1 : (0 : ℂ →L[ℂ] ℂ) 1 = (0 : ℂ) := rfl + replace d := d.trans z1 simp only [differentiableAt_fun_id, deriv_fun_pow, Nat.cast_pow, deriv_id'', mul_one, mul_eq_zero, pow_eq_zero_iff', Nat.cast_eq_zero, s.d0, ne_eq, false_and, false_or] at d exact d.1 @@ -259,7 +260,7 @@ theorem Super.grow_start (s : Super f d a) (c : ℂ) : ∃ p r, 0 < p ∧ Grow s theorem Grow.open (g : Grow s c p n r) : ∃ p', p < p' ∧ ∀ᶠ c' in 𝓝 c, Grow s c' p' n r := by have e := g.eqn; simp only [isCompact_singleton.nhdsSet_prod_eq (isCompact_closedBall _ _)] at e rcases Filter.mem_prod_iff.mp e with ⟨a', an, b', bn, sub⟩ - simp only [subset_setOf] at sub + simp only [subset_ofPred] at sub rcases eventually_nhds_iff.mp (nhdsSet_singleton.subst an) with ⟨a, aa, ao, am⟩ rcases eventually_nhdsSet_iff_exists.mp bn with ⟨b, bo, bp, bb⟩ rcases domain_open' bp bo with ⟨q, pq, qb⟩ @@ -546,7 +547,7 @@ theorem join_r (s : Super f d a) {p : ℕ → ℝ} {n : ℕ → ℕ} {ps : ℝ} · have m : (e, x) ∈ u0 ×ˢ u1 := by refine mk_mem_prod eu (subset_of_mem_nhdsSet n1 ?_) simp only [mem_closedBall, Complex.dist_eq, sub_zero, xk0.le] - specialize eq m; simp only [mem_setOf, uncurry] at eq + specialize eq m; simp only [mem_ofPred, uncurry] at eq rw [h _ xk0, eq] · have xe : ∃ k, ‖x‖ < p k := ⟨k + 1, xk1⟩ have n := (Nat.find_eq_iff xe).mpr ⟨xk1, ?_⟩ @@ -627,7 +628,7 @@ theorem Super.grow (s : Super f d a) [OnePreimage s] : have eq := le_antisymm le (not_lt.mp lt); rw [eq]; clear eq lt le q0 q -- Piece together a single r that works < Sup t, then close to Sup t rcases exists_seq_tendsto_sSup ne above with ⟨p, mono, tend, sub⟩ - simp only [mem_setOf, t] at sub + simp only [mem_ofPred, t] at sub set pr := fun k ↦ choose (self (sub k)) have pg : ∀ k, Grow s c (p k) (s.np c (sSup t)) (pr k) := fun k ↦ (choose_spec (self (sub k))).mono diff --git a/Ray/Dynamics/Multiple.lean b/Ray/Dynamics/Multiple.lean index 1443273..91a300d 100644 --- a/Ray/Dynamics/Multiple.lean +++ b/Ray/Dynamics/Multiple.lean @@ -4,6 +4,7 @@ import Mathlib.Geometry.Manifold.Algebra.Structures import Mathlib.Geometry.Manifold.ContMDiff.Atlas import Mathlib.Geometry.Manifold.MFDeriv.FDeriv import Mathlib.RingTheory.RootsOfUnity.Complex +import Mathlib.SetTheory.Cardinal.NatCard import Ray.Analytic.Analytic import Ray.Dynamics.BottcherNear import Ray.Manifold.Analytic @@ -47,7 +48,7 @@ variable {T : Type} [TopologicalSpace T] [ChartedSpace ℂ T] [IsManifold I ω T theorem exist_root_of_unity {d : ℕ} (d2 : 2 ≤ d) : ∃ a : ℂ, a ≠ 1 ∧ a ^ d = 1 := by set n : ℕ+ := ⟨d, lt_of_lt_of_le (by norm_num) d2⟩ have two : Nontrivial (rootsOfUnity n ℂ) := by - rw [← Fintype.one_lt_card_iff_nontrivial, Complex.card_rootsOfUnity] + rw [← Finite.one_lt_card_iff_nontrivial, Complex.card_rootsOfUnity] simp only [PNat.mk_coe, n]; exact lt_of_lt_of_le (by norm_num) d2 rcases two with ⟨⟨a, am⟩, ⟨b, bm⟩, ab⟩ simp only [Ne, Subtype.mk_eq_mk, mem_rootsOfUnity] at am bm ab @@ -77,8 +78,8 @@ theorem SuperAt.not_local_inj {f : ℂ → ℂ} {d : ℕ} (s : SuperAt f d) : have d0 : mfderiv I I (fun z : ℂ ↦ z) 0 ≠ 0 := id_mderiv_ne_zero rw [(Filter.EventuallyEq.symm ib).mfderiv_eq] at d0 rw [←Function.comp_def, mfderiv_comp 0 _ ba.differentiableAt.mdifferentiableAt] at d0 - simp only [Ne, mderiv_comp_eq_zero_iff, nc, or_false] at d0 - rw [bottcherNear_zero] at d0; exact d0 + rw [bottcherNear_zero] at d0 + exact fun h ↦ d0 (ContinuousLinearMap.ext fun v ↦ by rw [h]; rfl) rw [bottcherNear_zero]; exact ia.mdifferentiableAt (by decide) rcases exist_root_of_unity s.d2 with ⟨a, a1, ad⟩ refine ⟨fun z ↦ i (a * bottcherNear f d z), ?_, ?_, ?_⟩ @@ -193,7 +194,10 @@ public theorem not_local_inj_of_mfderiv_zero {f : S → T} {c : S} (fa : ContMDi mfderiv_comp _ ((contMDiffAt_extChartAt' _).mdifferentiableAt one_ne_zero) _, mfderiv_comp _ fd (((contMDiffOn_extChartAt_symm _).contMDiffAt (extChartAt_target_mem_nhds' _)).mdifferentiableAt one_ne_zero), - PartialEquiv.left_inv, df, ContinuousLinearMap.zero_comp, ContinuousLinearMap.comp_zero] + PartialEquiv.left_inv, df] + · apply ContinuousLinearMap.ext + intro v + exact ContinuousLinearMap.map_zero _ · apply mem_extChartAt_source · apply mem_extChartAt_target · simp @@ -201,9 +205,11 @@ public theorem not_local_inj_of_mfderiv_zero {f : S → T} {c : S} (fa : ContMDi (((contMDiffOn_extChartAt_symm _).contMDiffAt (extChartAt_target_mem_nhds' (mem_extChartAt_target c))).mdifferentiableAt one_ne_zero) simp only [mAnalyticAt_iff_of_boundaryless, Function.comp_def, hg] at fa - have dg' := fa.2.differentiableAt.mdifferentiableAt.hasMFDerivAt - rw [dg, hasMFDerivAt_iff_hasFDerivAt] at dg' - replace dg := dg'.hasDerivAt; clear dg' + have dg' : HasFDerivAt g (0 : ℂ →L[ℂ] ℂ) (extChartAt I c c) := by + have h := fa.2.differentiableAt.mdifferentiableAt.hasMFDerivAt + rw [dg] at h + exact hasMFDerivAt_iff_hasFDerivAt.mp h + replace dg : HasDerivAt g 0 (extChartAt I c c) := dg'.hasDerivAt rcases not_local_inj_of_deriv_zero fa.2 dg with ⟨h, ha, h0, e⟩ refine ⟨fun z ↦ (extChartAt I c).symm (h (extChartAt I c z)), ?_, ?_, ?_⟩ · apply ((contMDiffOn_extChartAt_symm _).contMDiffAt diff --git a/Ray/Dynamics/Postcritical.lean b/Ray/Dynamics/Postcritical.lean index c52178b..041699f 100644 --- a/Ray/Dynamics/Postcritical.lean +++ b/Ray/Dynamics/Postcritical.lean @@ -44,7 +44,7 @@ variable {s : Super f d a} /-- `s.ps c` is nonempty (since it contains 1) -/ public theorem Super.nonempty_ps (s : Super f d a) : (s.ps c).Nonempty := - ⟨1, by simp only [Super.ps, mem_setOf, true_or]⟩ + ⟨1, by simp only [Super.ps, mem_ofPred, true_or]⟩ /-- `s.ps c` is compact -/ public theorem Super.compact_ps (s : Super f d a) [OnePreimage s] [T2Space S] : @@ -53,7 +53,7 @@ public theorem Super.compact_ps (s : Super f d a) [OnePreimage s] [T2Space S] : have c1 : IsCompact {(1 : ℝ)} := isCompact_singleton convert c1.union ((s.isClosed_critical_not_a.snd_preimage c).isCompact.image pc) apply Set.ext; intro p - simp only [mem_setOf, Super.ps, mem_singleton_iff, mem_union, mem_image, Ne, ← + simp only [mem_ofPred, Super.ps, mem_singleton_iff, mem_union, mem_image, Ne, ← s.potential_eq_zero_of_onePreimage c] apply or_congr_right; constructor intro ⟨p0, z, e, c⟩; rw [← e] at p0; exact ⟨z, ⟨c, p0⟩, e⟩ @@ -145,7 +145,7 @@ public theorem Super.isOpen_post (s : Super f d a) [OnePreimage s] [T2Space S] : (Continuous.potential s).neg.lowerSemicontinuous have e : s.post = f ⁻¹' Ioi 0 := Set.ext fun _ ↦ by - simp only [Super.post, mem_setOf, Postcritical, mem_preimage, mem_Ioi, sub_pos, f] + simp only [Super.post, mem_ofPred, Postcritical, mem_preimage, mem_Ioi, sub_pos, f] rw [e]; exact fc.isOpen_preimage _ /-- Postcritical holds locally -/ @@ -164,12 +164,12 @@ theorem Super.postPostcritical (s : Super f d a) {p : ℂ × S} (m : p ∈ s.pos /-- `a` is postcritical -/ @[simp] public lemma Super.post_a (s : Super f d a) [OnePreimage s] [T2Space S] (c : ℂ) : (c, a) ∈ s.post := by - simp only [Super.post, Postcritical, s.potential_a, mem_setOf]; exact s.p_pos c + simp only [Super.post, Postcritical, s.potential_a, mem_ofPred]; exact s.p_pos c /-- `f` maps `s.post` into itself -/ public theorem Super.stays_post (s : Super f d a) {p : ℂ × S} (m : p ∈ s.post) : (p.1, f p.1 p.2) ∈ s.post := by - rcases p with ⟨c, z⟩; simp only [Super.post, mem_setOf, Postcritical, s.potential_eqn] + rcases p with ⟨c, z⟩; simp only [Super.post, mem_ofPred, Postcritical, s.potential_eqn] exact lt_of_le_of_lt (pow_le_of_le_one s.potential_nonneg s.potential_le_one s.d0) m /-- Iterating `f` maps `s.post` into itself -/ @@ -183,7 +183,7 @@ public theorem Super.basin_post (s : Super f d a) [OnePreimage s] [T2Space S] (m : (c, z) ∈ s.basin) : ∃ n, (c, (f c)^[n] z) ∈ s.post := by rcases tendsto_atTop_nhds.mp (s.basin_attracts m) {z | (c, z) ∈ s.post} (s.post_a c) (s.isOpen_post.snd_preimage c) with ⟨n, h⟩ - specialize h n (le_refl n); simp only [mem_setOf] at h; use n, h + specialize h n (le_refl n); simp only [mem_ofPred] at h; use n, h /-- `s.potential` has postcritical minima only at `z = a` -/ public theorem Super.potential_minima_only_a (s : Super f d a) [OnePreimage s] [T2Space S] diff --git a/Ray/Dynamics/Potential.lean b/Ray/Dynamics/Potential.lean index c4e63ae..71f8210 100644 --- a/Ray/Dynamics/Potential.lean +++ b/Ray/Dynamics/Potential.lean @@ -284,10 +284,10 @@ theorem Super.barrier (s : Super f d a) [OnePreimage s] [T2Space S] (n : Set ( simp only [Set.subset_inter_iff] at ii set t := u \ univ ×ˢ i1 have ta : ∀ e, (e, a) ∉ t := fun e ↦ - Set.notMem_diff_of_mem (Set.mk_mem_prod (Set.mem_univ _) i1m) + Set.notMem_sdiff_of_mem (Set.mk_mem_prod (Set.mem_univ _) i1m) use t - refine ⟨uc.diff (isOpen_univ.prod i1o), subset_trans diff_subset us.1, - subset_trans diff_subset us.2, ta, ?_⟩ + refine ⟨uc.diff (isOpen_univ.prod i1o), subset_trans sdiff_subset us.1, + subset_trans sdiff_subset us.2, ta, ?_⟩ rw [eventually_nhds_iff]; use i0; refine ⟨?_, i0o, i0m⟩ intro e em z zm za rcases tendsto_atTop_nhds.mp za i1 i1m i1o with ⟨m, mh⟩ @@ -300,7 +300,7 @@ theorem Super.barrier (s : Super f d a) [OnePreimage s] [T2Space S] (n : Set ( simp only [zm, Function.iterate_zero, id_eq] at ni1 exact us.1 (ii.1 (Set.mk_mem_prod em ni1)) have nt : (f e)^[n-1] z ∉ i1 := Nat.find_min en (Nat.pred_lt n0) - apply Set.mem_diff_of_mem + apply Set.mem_sdiff_of_mem · apply interior_subset; apply ih (e, (f e)^[n] z) (ii.2 (Set.mk_mem_prod em ni1)) simp only [Super.fp]; rw [← Function.iterate_succ_apply' (f e) (n - 1)] simp only [Nat.succ_eq_add_one, Nat.sub_add_cancel (Nat.one_le_of_lt (Nat.pos_of_ne_zero n0))] @@ -405,7 +405,7 @@ public theorem Continuous.potential (s : Super f d a) [OnePreimage s] [T2Space S rcases en with ⟨n, h⟩ rcases eventually_nhds_iff.mp h with ⟨v, vh, vo, vc⟩ have ev : ∀ᶠ p : ℂ × S in 𝓝 (c, z), p ∈ u ∩ v ×ˢ univ := by - simp only [Filter.eventually_iff, Set.setOf_mem_eq] + simp only [Filter.eventually_iff, Set.ofPred_mem_eq] exact Filter.inter_mem un ((vo.prod isOpen_univ).mem_nhds (Set.mk_mem_prod vc (Set.mem_univ _))) have ef : ∃ᶠ p in 𝓝 (c, z), p ∈ b.fast n := by refine (re.and_eventually ev).mp (.of_forall ?_) diff --git a/Ray/Dynamics/Ray.lean b/Ray/Dynamics/Ray.lean index 7ca2be7..b6fc8bf 100644 --- a/Ray/Dynamics/Ray.lean +++ b/Ray/Dynamics/Ray.lean @@ -55,7 +55,7 @@ variable {y : ℂ × ℂ} /-- The `c`-slice of `s.ext` is `ball 0 (s.p c)` -/ theorem Super.ext_slice (s : Super f d a) (c : ℂ) : {x | (c, x) ∈ s.ext} = ball (0 : ℂ) (s.p c) := by - apply Set.ext; intro x; simp only [Super.ext, mem_ball, mem_setOf, Complex.dist_eq, sub_zero] + apply Set.ext; intro x; simp only [Super.ext, mem_ball, mem_ofPred, Complex.dist_eq, sub_zero] variable [T2Space S] @@ -71,13 +71,13 @@ public theorem Super.isOpen_ext (s : Super f d a) [OnePreimage s] : IsOpen s.ext (s.lowerSemicontinuous_p.comp continuous_fst).add (continuous_norm.comp continuous_snd).neg.lowerSemicontinuous have e : s.ext = f ⁻¹' Ioi 0 := - Set.ext fun _ ↦ by simp only [Super.ext, mem_setOf, mem_preimage, mem_Ioi, sub_pos, f] + Set.ext fun _ ↦ by simp only [Super.ext, mem_ofPred, mem_preimage, mem_Ioi, sub_pos, f] rw [e]; exact fc.isOpen_preimage _ /-- `(c,0) ∈ s.ext` -/ @[simp] public theorem Super.mem_ext (s : Super f d a) [OnePreimage s] (c : ℂ) : (c, (0 : ℂ)) ∈ s.ext := by - simp only [Super.ext, mem_setOf, norm_zero, s.p_pos c] + simp only [Super.ext, mem_ofPred, norm_zero, s.p_pos c] /-- `c`-slices of `s.ext` are connected -/ public theorem Super.ext_slice_connected (s : Super f d a) [OnePreimage s] (c : ℂ) : @@ -89,10 +89,10 @@ public theorem Super.ext_slice_connected (s : Super f d a) [OnePreimage s] (c : public theorem Super.ext_connected (s : Super f d a) [OnePreimage s] : IsConnected s.ext := by refine ⟨⟨(0, 0), s.mem_ext 0⟩, isPreconnected_of_forall (0, 0) ?_⟩; intro ⟨c, x⟩ m use(fun x ↦ (c, x)) '' {x | (c, x) ∈ s.ext} ∪ univ ×ˢ {0} - simp only [mem_image, mem_union, union_subset_iff, mem_setOf, mem_prod_eq, mem_univ, true_and, + simp only [mem_image, mem_union, union_subset_iff, mem_ofPred, mem_prod_eq, mem_univ, true_and, mem_singleton_iff, or_true] refine ⟨⟨?_, ?_⟩, ?_, ?_⟩ - · intro y n; simp only [mem_image, mem_setOf] at n; rcases n with ⟨x, m, e⟩; rw [e] at m; exact m + · intro y n; simp only [mem_image, mem_ofPred] at n; rcases n with ⟨x, m, e⟩; rw [e] at m; exact m · intro ⟨c, x⟩ m; simp only [mem_prod_eq, mem_singleton_iff] at m; rw [m.2]; exact s.mem_ext c · left; exact ⟨x, m, rfl⟩ · refine IsPreconnected.union (c, 0) ?_ ?_ ?_ ?_ @@ -159,7 +159,7 @@ public theorem Super.ray_potential (s : Super f d a) [OnePreimage s] (post : (c, /-- `s.ray` maps `s.ext` into `s.post` -/ public theorem Super.ray_post (s : Super f d a) [OnePreimage s] (post : (c, x) ∈ s.ext) : (c, s.ray c x) ∈ s.post := by - simp only [Super.post, Postcritical, mem_setOf, s.ray_potential post]; exact post + simp only [Super.post, Postcritical, mem_ofPred, s.ray_potential post]; exact post /-- `s.ray` is noncritical at 0 -/ theorem Super.ray_noncritical_zero (s : Super f d a) [OnePreimage s] (c : ℂ) : @@ -187,9 +187,10 @@ public theorem Super.ray_noncritical (s : Super f d a) [OnePreimage s] (post : ( rw [e.mfderiv_eq]; contrapose x0 rw [mfderiv_eq_fderiv] at x0 have d := (differentiableAt_pow (x := x) (d ^ n)).hasFDerivAt.hasDerivAt.deriv - apply_fun (fun x ↦ x 1) at x0 + replace x0 := ContinuousLinearMap.ext_iff.mp x0 1 rw [x0] at d - replace d := Eq.trans d (ContinuousLinearMap.zero_apply _) + have z1 : (0 : ℂ →L[ℂ] ℂ) 1 = (0 : ℂ) := rfl + replace d := d.trans z1 simp only [differentiableAt_fun_id, deriv_fun_pow, Nat.cast_pow, deriv_id'', mul_one, mul_eq_zero, pow_eq_zero_iff', Nat.cast_eq_zero, s.d0, ne_eq, false_and, false_or] at d exact d.1 @@ -227,7 +228,7 @@ public theorem Super.ray_inj (s : Super f d a) [OnePreimage s] {x0 x1 : ℂ} : Complex.continuous_ofReal.continuousAt.mul continuousAt_const have pt : ∀ {x : ℂ} {t : ℝ}, (c, x) ∈ s.ext → t ∈ Ioc (0 : ℝ) 1 → (c, ↑t * x) ∈ s.ext := by intro x t p m - simp only [Super.ext, mem_setOf, norm_mul, Complex.norm_real, Real.norm_eq_abs, + simp only [Super.ext, mem_ofPred, norm_mul, Complex.norm_real, Real.norm_eq_abs, abs_of_pos m.1] at p ⊢ exact lt_of_le_of_lt (mul_le_of_le_one_left (norm_nonneg _) m.2) p -- It suffices to show that the set of t's where the x0 and x1 rays match @@ -249,13 +250,13 @@ public theorem Super.ray_inj (s : Super f d a) [OnePreimage s] {x0 x1 : ℂ} : exact mul_left_cancel₀ (Complex.ofReal_ne_zero.mpr t0.ne') inj refine isPreconnected_Ioc.relative_clopen ?_ ?_ ?_ · use 1, right_mem_Ioc.mpr zero_lt_one - simp only [mem_setOf, Complex.ofReal_one, one_mul, e, u] + simp only [mem_ofPred, Complex.ofReal_one, one_mul, e, u] · intro t ⟨m, e⟩ simp only [mem_interior_iff_mem_nhds] at e ⊢ generalize hn : s.np c ‖↑t * x0‖ = n have t0 : (t : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr m.1.ne' have pe : ‖↑t * x0‖ = ‖↑t * x1‖ := by - simp only [mem_setOf_eq, u] at e + simp only [mem_ofPred_eq, u] at e simp only [← s.ray_potential (pt p0 m), e, ← s.ray_potential (pt p1 m)] have e0 := (s.ray_spec (norm_nonneg _) (pt p0 m)).eqn.filter_mono (nhds_le_nhdsSet mem_domain_self) @@ -265,7 +266,7 @@ public theorem Super.ray_inj (s : Super f d a) [OnePreimage s] {x0 x1 : ℂ} : have de : (↑t * x0) ^ d ^ n = (↑t * x1) ^ d ^ n := by have e0 := e0.self_of_nhds.eqn have e1 := e1.self_of_nhds.eqn - simp only [mem_setOf_eq, u] at e + simp only [mem_ofPred_eq, u] at e simp only [← e] at e0 e1 exact e0.symm.trans e1 simp only [mul_pow] at de @@ -288,8 +289,9 @@ public theorem Super.ray_inj (s : Super f d a) [OnePreimage s] {x0 x1 : ℂ} : refine ((continuousAt_const.prodMk (Complex.continuous_ofReal.continuousAt.mul continuousAt_const)).eventually (eqn_unique e0 er ?_ (mul_ne_zero t0 x00))).mp (.of_forall fun u e ↦ ?_) - · simp only [← hr]; rw [xe]; exact e + · simp only [← hr]; simp only [Pi.mul_apply]; rw [xe]; exact e · rw [← hr] at e; simp only [uncurry] at e + simp only [Pi.mul_apply] at e ⊢ rw [← mul_assoc, mul_comm _ (u:ℂ), mul_assoc, div_mul_cancel₀ _ x00] at e exact e · intro t ⟨m, e⟩; simp only [mem_closure_iff_frequently] at e ⊢ @@ -321,7 +323,7 @@ public theorem Super.ray_surj (s : Super f d a) [OnePreimage s] : intro z0 m0 by_contra i0; simp only [not_exists, not_and] at i0 set p0 := s.potential c z0 - simp only [Super.post, mem_setOf, Postcritical] at m0 + simp only [Super.post, mem_ofPred, Postcritical] at m0 rcases exists_between m0 with ⟨p1, p01, post⟩ set i := s.ray c '' {x | (c, x) ∈ s.ext} set j := {z | s.potential c z ≤ p1} ∩ i @@ -336,7 +338,7 @@ public theorem Super.ray_surj (s : Super f d a) [OnePreimage s] : have jc : IsClosed j := by have e : j = s.ray c '' closedBall 0 p1 := by refine Set.ext fun z ↦ ?_ - simp only [mem_inter_iff, mem_setOf, mem_image, mem_closedBall, Complex.dist_eq, sub_zero, j] + simp only [mem_inter_iff, mem_ofPred, mem_image, mem_closedBall, Complex.dist_eq, sub_zero, j] constructor · intro ⟨zp1, x, xp, xz⟩; rw [← xz, s.ray_potential xp] at zp1; use x, zp1, xz · intro ⟨x, xp, xz⟩; have zp1 := lt_of_le_of_lt xp post; rw [← xz, s.ray_potential zp1] @@ -346,11 +348,11 @@ public theorem Super.ray_surj (s : Super f d a) [OnePreimage s] : exact (s.ray_mAnalytic (lt_of_le_of_lt m post)).along_snd.continuousAt.continuousWithinAt have uc : IsCompact u := ((isClosed_le pc continuous_const).sdiff io).isCompact have z0u : z0 ∈ u := by - simp only [mem_diff, mem_setOf, u]; use p01.le; contrapose i0 + simp only [mem_sdiff, mem_ofPred, u]; use p01.le; contrapose i0 simp only [not_not, not_forall, exists_prop] at i0 ⊢; exact i0 have ne : u.Nonempty := ⟨z0, z0u⟩ rcases uc.exists_isMinOn ne pc.continuousOn with ⟨z, zu, zm⟩ - simp only [mem_diff, mem_setOf, u] at zu + simp only [mem_sdiff, mem_ofPred, u] at zu replace zm : ∀ᶠ w in 𝓝 z, s.potential c z ≤ s.potential c w := by have m : z ∈ jᶜ := by rw [compl_inter]; right; exact zu.2 have lt : s.potential c z < p1 := lt_of_le_of_lt (zm z0u) p01 @@ -358,9 +360,9 @@ public theorem Super.ray_surj (s : Super f d a) [OnePreimage s] : apply ((Continuous.potential s).along_snd.continuousAt.eventually_lt continuousAt_const lt).mp refine .of_forall fun w lt m ↦ ?_ rw [compl_inter] at m; cases' m with m m - · simp only [compl_setOf, mem_setOf, not_le] at m; linarith - · apply zm; simp only [mem_diff, mem_setOf, u]; use lt.le, m - simp only [mem_setOf, mem_image, not_exists, not_and, i] at zu + · simp only [compl_ofPred, mem_ofPred, not_le] at m; linarith + · apply zm; simp only [mem_sdiff, mem_ofPred, u]; use lt.le, m + simp only [mem_ofPred, mem_image, not_exists, not_and, i] at zu have za := s.potential_minima_only_a (lt_of_le_of_lt zu.1 post) zm have h := zu.2 0 (s.mem_ext c); simp only [s.ray_zero] at h; exact h za.symm diff --git a/Ray/Hartogs/Duals.lean b/Ray/Hartogs/Duals.lean index fc9e4ef..e944354 100644 --- a/Ray/Hartogs/Duals.lean +++ b/Ray/Hartogs/Duals.lean @@ -116,7 +116,7 @@ theorem norm_eq_duals_supr' {g : ℝ → ℝ} {k : NNReal} (gm : Monotone g) (gk /-- Norms are suprs over `duals` -/ theorem norm_eq_duals_iSup (x : E) : ‖x‖ = ⨆ n, ‖duals n x‖ := by have h := norm_eq_duals_supr' (@monotone_id ℝ _) LipschitzWith.id x - simpa only using h + simpa only [id_eq] using h /-- Norms are suprs over `duals` (`maxLog` version) -/ theorem maxLog_norm_eq_duals_iSup (b : ℝ) (x : E) : maxLog b ‖x‖ = ⨆ n, maxLog b ‖duals n x‖ := @@ -149,6 +149,6 @@ public theorem duals_lim_tendsto_maxLog_norm (b : ℝ) (x : E) : /-- Partial sups of `maxLog b ‖duals k x‖` converge to `maxLog b ‖x‖` -/ theorem maxLog_norm_eq_duals_limUnder (b : ℝ) (x : E) : - maxLog b ‖x‖ = limUnder atTop (partialSups fun k ↦ maxLog b ‖duals k x‖) := + maxLog b ‖x‖ = Filter.limUnder atTop (partialSups fun k ↦ maxLog b ‖duals k x‖) := haveI a := duals_lim_tendsto_maxLog_norm b x tendsto_nhds_unique a (tendsto_nhds_limUnder ⟨_, a⟩) diff --git a/Ray/Hartogs/FubiniBall.lean b/Ray/Hartogs/FubiniBall.lean index e084950..66b1428 100644 --- a/Ray/Hartogs/FubiniBall.lean +++ b/Ray/Hartogs/FubiniBall.lean @@ -117,11 +117,11 @@ theorem square_eq {c : ℂ} {r0 r1 : ℝ} (r0p : 0 ≤ r0) : simp only [square, prodMk_mem_set_prod_eq, mem_Ioc] at ss rw [← tz] have s0 : 0 < s := by linarith - simp only [circleMap, add_comm c, annulus_oc, mem_diff, Metric.mem_closedBall, + simp only [circleMap, add_comm c, annulus_oc, mem_sdiff, Metric.mem_closedBall, dist_add_self_left, norm_mul, Complex.norm_real, Real.norm_eq_abs, Complex.norm_exp_ofReal_mul_I, mul_one, not_le, abs_of_pos s0, ss.1, true_and] · intro zr - simp only [mem_diff, Metric.mem_closedBall, annulus_oc, not_le] at zr + simp only [mem_sdiff, Metric.mem_closedBall, annulus_oc, not_le] at zr rw [dist_comm] at zr have zz : z ∈ sphere c (dist c z) := by simp only [Complex.dist_eq, mem_sphere_iff_norm, norm_sub_rev] @@ -240,7 +240,7 @@ public theorem fubini_annulus {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ intro x xs simp only [Icc_prod_Icc, mem_Icc, Prod.le_def] at xs have x0 : 0 ≤ x.1 := by linarith - simp only [circleMap, annulus_cc, mem_diff, Metric.mem_closedBall, dist_self_add_left, + simp only [circleMap, annulus_cc, mem_sdiff, Metric.mem_closedBall, dist_self_add_left, norm_mul, Complex.norm_real, abs_of_nonneg x0, Real.norm_eq_abs, Complex.norm_exp_ofReal_mul_I, mul_one, xs.2.1, Metric.mem_ball, not_lt, xs.1.1, and_self] exact fi.mono_set (prod_mono Ioc_subset_Icc_self Ioc_subset_Icc_self) @@ -254,7 +254,7 @@ public theorem fubini_ball {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] rw [MeasureTheory.setIntegral_congr_set center]; clear center rw [← Metric.closedBall_zero, ← annulus_oc] apply fubini_annulus - · simpa only [annulus_cc, Metric.ball_zero, diff_empty] + · simpa only [annulus_cc, Metric.ball_zero, sdiff_empty] · rfl /-- The volume of the complex closed ball is `π r^2` -/ diff --git a/Ray/Hartogs/Hartogs.lean b/Ray/Hartogs/Hartogs.lean index 9118dd4..6256ad0 100644 --- a/Ray/Hartogs/Hartogs.lean +++ b/Ray/Hartogs/Hartogs.lean @@ -135,7 +135,8 @@ theorem Bounded.dist0 (h : Har f s) {z w : ℂ × ℂ} {b e r : ℝ} (bp : 0 < b _ ≤ b + b := by linarith _ = 2 * b := by ring _ < 3 * b := mul_lt_mul_of_pos_right (by norm_num) bp - have L := Complex.dist_le_div_mul_dist_of_mapsTo_ball d m wf; simp only [Prod.mk.eta] at L + have L := Complex.dist_le_div_mul_dist_of_mapsTo_ball d + (m.mono_right Metric.ball_subset_closedBall) wf; simp only [Prod.mk.eta] at L refine _root_.trans L (_root_.trans ?_ ue); simp only [Metric.mem_ball] at wz rw [div_eq_mul_inv _ (2 : ℝ), div_mul_eq_div_div]; ring_nf bound @@ -218,7 +219,7 @@ theorem forall_const_and_distrib {A : Type} [Nonempty A] {p : Prop} {q : A → P theorem ContinuousOn.isClosed_le {A B : Type} [TopologicalSpace A] [TopologicalSpace B] [Preorder B] [OrderClosedTopology B] {s : Set A} {f g : A → B} (sc : IsClosed s) (fc : ContinuousOn f s) (gc : ContinuousOn g s) : IsClosed {x | x ∈ s ∧ f x ≤ g x} := by - rw [Set.setOf_and]; simp only [Set.setOf_mem_eq] + rw [Set.ofPred_and]; simp only [Set.ofPred_mem_eq] set t := {p : B × B | p.fst ≤ p.snd} set fg := fun x ↦ (f x, g x) have e : {x | f x ≤ g x} = fg ⁻¹' t := by aesop @@ -238,9 +239,9 @@ theorem on_subdisk [CompleteSpace E] (h : Har f (closedBall (c0, c1) r)) (rp : r {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1, z1 ∈ closedBall c1 r → ‖f (z0, z1)‖ ≤ b}) = S have hc : ∀ b, IsClosed (S b) := by intro b; rw [← hS]; simp only [← forall_const_and_distrib] - rw [Set.setOf_forall]; apply isClosed_iInter; intro z1 + rw [Set.ofPred_forall]; apply isClosed_iInter; intro z1 by_cases z1r : z1 ∉ closedBall c1 r - · simp only [z1r, false_imp_iff, and_true, Set.setOf_mem_eq, Metric.isClosed_closedBall] + · simp only [z1r, false_imp_iff, and_true, Set.ofPred_mem_eq, Metric.isClosed_closedBall] · rw [Set.not_notMem] at z1r simp only [z1r, true_imp_iff] refine ContinuousOn.isClosed_le Metric.isClosed_closedBall ?_ continuousOn_const @@ -253,7 +254,7 @@ theorem on_subdisk [CompleteSpace E] (h : Har f (closedBall (c0, c1) r)) (rp : r have z0s' := esub (ball_subset_closedBall z0s) rcases (isCompact_closedBall _ _).bddAbove_image (h.on1 z0s').continuousOn.norm with ⟨b, fb⟩ simp only [mem_upperBounds, Set.forall_mem_image] at fb - use Nat.ceil b; rw [← hS]; simp only [Set.mem_setOf] + use Nat.ceil b; rw [← hS]; simp only [Set.mem_ofPred] refine ⟨ball_subset_closedBall z0s, ?_⟩ simp only [Metric.mem_closedBall] at fb ⊢; intro z1 z1r exact _root_.trans (fb z1r) (Nat.le_ceil _) @@ -264,7 +265,7 @@ theorem on_subdisk [CompleteSpace E] (h : Har f (closedBall (c0, c1) r)) (rp : r have tr : ball c0' t ⊆ closedBall c0 re := by rw [Set.subset_def]; intro z0 z0t have z0b := _root_.trans ts s's z0t - rw [← hS] at z0b; simp only [Set.setOf_and, Set.setOf_mem_eq, Set.mem_inter_iff] at z0b + rw [← hS] at z0b; simp only [Set.ofPred_and, Set.ofPred_mem_eq, Set.mem_inter_iff] at z0b exact z0b.left have c0e : c0' ∈ closedBall c0 e := _root_.trans tr (Metric.closedBall_subset_closedBall (min_le_right _ _)) @@ -273,7 +274,7 @@ theorem on_subdisk [CompleteSpace E] (h : Har f (closedBall (c0, c1) r)) (rp : r intro z zs; rw [Set.mem_prod] at zs have zb := _root_.trans ts s's zs.left rw [← hS] at zb - simp only [Metric.mem_ball, Metric.mem_closedBall, Set.mem_setOf_eq] at zb zs + simp only [Metric.mem_ball, Metric.mem_closedBall, Set.mem_ofPred_eq] at zb zs have zb' := zb.right z.snd zs.right.le simp only [Prod.mk.eta] at zb'; exact zb' use t, tp, c0e @@ -512,7 +513,7 @@ theorem Along0.norm {n : ℕ} (p : ContinuousMultilinearMap ℂ (fun _ : Fin n have e : ∀ i : Fin n, ‖m i‖ = ‖idZeroLm (m i)‖ := by intro i simp only [idZeroLm, ContinuousLinearMap.prod_apply, ContinuousLinearMap.coe_id', id_eq, - ContinuousLinearMap.zero_apply, Prod.norm_def, norm_zero, norm_nonneg, sup_of_le_left] + _root_.zero_apply, Prod.norm_def, norm_zero, norm_nonneg, sup_of_le_left] simp_rw [e] exact ContinuousMultilinearMap.le_opNorm p _ @@ -525,12 +526,12 @@ def Along0.linearMap (n : ℕ) : intro p q; simp_rw [ContinuousMultilinearMap.along0] apply ContinuousMultilinearMap.ext; intro m simp only [ContinuousMultilinearMap.compContinuousLinearMap_apply, - ContinuousMultilinearMap.add_apply] + _root_.add_apply] map_smul' := by intro s p; simp_rw [ContinuousMultilinearMap.along0] apply ContinuousMultilinearMap.ext; intro m simp only [ContinuousMultilinearMap.compContinuousLinearMap_apply, - ContinuousMultilinearMap.smul_apply, RingHom.id_apply] + _root_.smul_apply, RingHom.id_apply] /-- `.along0` is continuous linear -/ def Along0.continuousLinearMap (n : ℕ) : @@ -570,11 +571,12 @@ theorem HasFPowerSeriesAt.along0 {f : ℂ × ℂ → E} {c0 c1 : ℂ} simp_rw [FormalMultilinearSeries.along0, ContinuousMultilinearMap.along0, idZeroLm] simp only [ContinuousMultilinearMap.compContinuousLinearMap_apply, ContinuousLinearMap.prod_apply, ContinuousLinearMap.coe_id', id_eq, - ContinuousLinearMap.zero_apply] - have w01r : (w0, (0 : ℂ)) ∈ EMetric.ball (0 : ℂ × ℂ) r := by - simpa only [Prod.edist_eq, EMetric.mem_ball, Prod.fst_zero, Prod.snd_zero, edist_self, - ENNReal.max_zero_right] using w0r - convert fpr.hasSum w01r; rw [Prod.mk_add_mk, add_zero] + _root_.zero_apply] + have w01r : (w0, (0 : ℂ)) ∈ Metric.eball (0 : ℂ × ℂ) r := by + simpa only [Prod.edist_eq, Metric.mem_eball, Prod.fst_zero, Prod.snd_zero, edist_self, + max_zero] using w0r + convert fpr.hasSum w01r + all_goals simp /-- The map `p ↦ p.along0` is analytic -/ theorem Along0.analyticAt (n : ℕ) : ∀ {p}, @@ -608,23 +610,23 @@ theorem unevenSeries_analytic [CompleteSpace E] (u : Uneven f c0 c1 r0 r1) (n : have s'p : s' > 0 := by simp only [Metric.mem_ball] at z1s; bound have sp : s > 0 := by bound have sr : s ≤ r := by bound - have sb : EMetric.ball z1 s ⊆ ball c1 r1 := by + have sb : Metric.eball z1 s ⊆ ball c1 r1 := by rw [Set.subset_def]; intro x xs - simp only [Metric.mem_ball, EMetric.mem_ball, lt_min_iff, edist_lt_ofReal, s] at xs z1s ⊢ + simp only [Metric.mem_ball, Metric.mem_eball, lt_min_iff, edist_lt_ofReal, s] at xs z1s ⊢ calc dist x c1 _ ≤ dist x z1 + dist z1 c1 := by bound _ < s' + dist z1 c1 := (add_lt_add_left xs.right _) _ = r1 - dist z1 c1 + dist z1 c1 := rfl _ = r1 := by ring_nf - use EMetric.ball z1 s - refine ⟨?_, EMetric.isOpen_ball, EMetric.mem_ball_self sp⟩ + use Metric.eball z1 s + refine ⟨?_, Metric.isOpen_eball, Metric.mem_eball_self sp⟩ intro w1 w1s have p0 : HasFPowerSeriesAt (fun z0 ↦ f (z0, w1)) (unevenSeries u w1) c0 := by have w1c : w1 ∈ closedBall c1 r1 := ball_subset_closedBall (sb w1s) refine (Uneven.has_series u u.r1p (le_refl _) w1c).hasFPowerSeriesAt have p1 : HasFPowerSeriesAt (fun z0 ↦ f (z0, w1)) (p.changeOrigin (g w1)).along0 c0 := by have wz : ↑‖((0 : ℂ), w1 - z1)‖₊ < r := by - simp only [EMetric.mem_ball, edist_dist, Complex.dist_eq, ofReal_norm, + simp only [Metric.mem_eball, edist_dist, Complex.dist_eq, ofReal_norm, enorm_eq_nnnorm] at w1s simp only [Prod.nnnorm_mk, nnnorm_zero, zero_le, sup_of_le_right] exact lt_of_lt_of_le w1s sr @@ -792,7 +794,7 @@ theorem uneven_bounded [CompleteSpace E] [SecondCountableTopology E] have ds : z.1 - c0 ∈ Metric.ball (0 : ℂ) s := by simp only [Complex.dist_eq] at zs simp only [zs.1, mem_ball_zero_iff] - have ds' : z.1 - c0 ∈ EMetric.ball (0 : ℂ) (ENNReal.ofReal s) := by rwa [Metric.emetric_ball] + have ds' : z.1 - c0 ∈ Metric.eball (0 : ℂ) (ENNReal.ofReal s) := by rwa [Metric.eball_ofReal] have hs := (u.has_series sp sr.le z1r).hasSum ds' simp only [unevenSeries_eq u sp sr.le z1r, FormalMultilinearSeries.apply_eq_pow_smul_coeff, add_sub_cancel, Prod.mk.eta] at hs diff --git a/Ray/Hartogs/Osgood.lean b/Ray/Hartogs/Osgood.lean index 7491843..4af3792 100644 --- a/Ray/Hartogs/Osgood.lean +++ b/Ray/Hartogs/Osgood.lean @@ -93,8 +93,8 @@ theorem spheres_subset_closedBall {c0 c1 : ℂ} {r : ℝ} : theorem Separate.rs' (h : Separate f c0 c1 r b s) : sphere c0 r ×ˢ sphere c1 r ⊆ s := le_trans spheres_subset_closedBall h.rs -theorem mem_sphere_closed {z c : ℂ} {r : ℝ} : z ∈ sphere c r → z ∈ closedBall c r := by - simp only [mem_sphere_iff_norm, Metric.mem_closedBall]; exact le_of_eq +theorem mem_sphere_closed {z c : ℂ} {r : ℝ} : z ∈ sphere c r → z ∈ closedBall c r := fun h ↦ + Metric.mem_closedBall.mpr (le_of_eq (Metric.mem_sphere.mp h)) /-- Spheres don't contain their center -/ theorem center_not_in_sphere {c z : ℂ} {r : ℝ} (rp : r > 0) (zs : z ∈ sphere c r) : z - c ≠ 0 := by @@ -375,7 +375,7 @@ theorem series2_norm (h : Separate f c0 c1 r b s) (n : ℕ) : intro n0 n0n; simp at n0n apply le_trans (termCmmap_norm ℂ n n0 (h.series2Coeff n0 (n - n0))) have sb := series2Coeff_bound h n0 (n - n0) - rw [← Nat.add_sub_assoc (Nat.le_of_lt_succ n0n) n0, Nat.add_sub_cancel_left] at sb + rw [← Nat.add_sub_assoc n0n n0, Nat.add_sub_cancel_left] at sb assumption trans (Finset.range (n + 1)).sum fun n0 ↦ ‖termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))‖ · bound @@ -413,7 +413,7 @@ theorem cauchy1 {r : ℝ} {c w : ℂ} {f : ℂ → E} (wm : w ∈ ball c r) (2*π*I : ℂ)⁻¹ • (∮ z in C(c, r), (z - w)⁻¹ • f z) = f w := by refine Complex.two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable Set.countable_empty wm fc ?_ - intro z zm; apply fd z _; simp only [Metric.mem_ball, Set.diff_empty] at zm ⊢; assumption + intro z zm; apply fd z _; simp only [Metric.mem_ball, Set.sdiff_empty] at zm ⊢; assumption /-- The 2D Cauchy integral formula -/ theorem cauchy2 (h : Separate f c0 c1 r b s) (w0m : w0 ∈ ball c0 r) (w1m : w1 ∈ ball c1 r) : @@ -516,7 +516,7 @@ theorem cauchy2_hasSum_2d (h : Separate f c0 c1 r b s) (w0m : w0 ∈ ball (0 : · intro n; simp only [Pi.zero_apply, div_pow]; bound · intro n; simp only [Pi.zero_apply, div_pow]; bound have fs' : HasSum f a' := by rw [← ha']; exact sf.hasSum - have gs' := HasSum.prod_fiberwise fs' fs; simp at gs' + have gs' := HasSum.prod_fiberwise fs' fs rwa [HasSum.unique gs gs'] /-- We convert the 2D sum to a 1D outer sum with an inner finite antidiagonal -/ @@ -524,10 +524,10 @@ theorem HasSum.antidiagonal_of_2d {V : Type} [AddCommMonoid V] [TopologicalSpace [ContinuousAdd V] [RegularSpace V] {f : ℕ × ℕ → V} {a : V} (h : HasSum f a) : HasSum (fun n ↦ (Finset.range (n + 1)).sum fun n1 ↦ f (n1, n - n1)) a := by generalize hg : (fun n ↦ (Finset.range (n + 1)).sum fun n1 ↦ f (n1, n - n1)) = g - rw [←Finset.sigmaAntidiagonalEquivProd.hasSum_iff] at h + rw [←Finset.HasAntidiagonal.sigmaAntidiagonalEquivProd.hasSum_iff] at h have fg : ∀ n, HasSum (fun d : Finset.antidiagonal n ↦ - (f ∘ Finset.sigmaAntidiagonalEquivProd) ⟨n, d⟩) (g n) := by - intro n; simp only [Function.comp_apply, Finset.sigmaAntidiagonalEquivProd_apply] + (f ∘ Finset.HasAntidiagonal.sigmaAntidiagonalEquivProd) ⟨n, d⟩) (g n) := by + intro n; simp only [Function.comp_apply, Finset.HasAntidiagonal.sigmaAntidiagonalEquivProd_apply] have fs := hasSum_fintype fun d : ↥(Finset.antidiagonal n) ↦ f ↑d -- simp at fs, have e : (Finset.univ.sum fun d : ↥(Finset.antidiagonal n) ↦ f ↑d) = g n := by @@ -545,7 +545,7 @@ theorem cauchy2_hasSum (h : Separate f c0 c1 r b s) (w0m : w0 ∈ ball (0 : ℂ) (Finset.range (n + 1)).sum fun n1 ↦ w0 ^ (n - n1) • w1 ^ n1 • h.series2Coeff (n - n1) n1) = fun n ↦ series2 h n fun _ : Fin n ↦ (w0, w1) := by clear sum; funext n - rw [series2]; simp only [ContinuousMultilinearMap.sum_apply] + rw [series2]; simp only [_root_.sum_apply] simp_rw [termCmmap_apply] nth_rw 1 [← Finset.sum_range_reflect]; simp apply Finset.sum_congr rfl @@ -560,7 +560,7 @@ theorem osgood_h (h : Separate f c0 c1 r b s) : { r_le := cauchy2_radius h r_pos := by simp; exact h.rp hasSum := by - simp only [Metric.emetric_ball, Metric.mem_ball, dist_zero_right, Prod.forall] + simp only [Metric.eball_ofReal, Metric.mem_ball, dist_zero_right, Prod.forall] intro w0 w1 wr; rw [Prod.norm_def] at wr simp only [max_lt_iff] at wr have w0m : w0 ∈ ball (0 : ℂ) r := by simp; exact wr.left diff --git a/Ray/Hartogs/Subharmonic.lean b/Ray/Hartogs/Subharmonic.lean index 5b7cdc6..eeed040 100644 --- a/Ray/Hartogs/Subharmonic.lean +++ b/Ray/Hartogs/Subharmonic.lean @@ -246,7 +246,7 @@ theorem AnalyticOnNhd.circle_mean_eq [CompleteSpace H] {f : ℂ → H} {c : ℂ} rw [← smul_assoc, Complex.real_smul] field_simp [Real.pi_ne_zero] simp - · intro z zs; rw [Set.diff_empty] at zs + · intro z zs; rw [Set.sdiff_empty] at zs exact (fa z (Metric.ball_subset_closedBall zs)).differentiableAt /-- Analytic functions are harmonic -/ @@ -573,7 +573,7 @@ theorem IsClosed.extendable {s : Set C(Real.Angle, ℂ)} (e : ∀ f, f ∈ s → have m := Extension.maximum_principle eab fab rp z zs simp only [Complex.dist_eq, Pi.sub_apply] at m ⊢ exact lt_of_le_of_lt m (by linarith) - set G := fun z ↦ limUnder atTop fun n ↦ g n z + set G := fun z ↦ Filter.limUnder atTop fun n ↦ g n z have gG : TendstoUniformlyOn g G atTop (closedBall c r) := by apply UniformCauchySeqOn.tendstoUniformlyOn_of_tendsto cauchy intro z zs; exact (cauchy.cauchySeq zs).tendsto_limUnder @@ -656,12 +656,15 @@ theorem fourierExtend {f : C(Real.Angle, ℂ)} (rp : r > 0) /-- All continuous functions on the circle extend to harmonic functions on the disk -/ theorem continuousExtend (f : C(Real.Angle, ℂ)) (c : ℂ) (rp : r > 0) : Extendable f c r := by - set s : Submodule ℂ C(Real.Angle, ℂ) := Submodule.span ℂ (Set.range (@fourier (2 * π))) + set s : Submodule ℂ C(Real.Angle, ℂ) := Submodule.span ℂ (Set.range (@fourier (2 * π))) with hs have se : ∀ f, f ∈ s.carrier → Extendable f c r := fun f fs ↦ fourierExtend rp fs have ce : ∀ f, f ∈ closure s.carrier → Extendable f c r := IsClosed.extendable se rp have e : closure s.carrier = s.topologicalClosure.carrier := rfl - rw [e, @span_fourier_closure_eq_top _ (fact_iff.mpr Real.two_pi_pos)] at ce - apply ce; simp only [Submodule.mem_carrier]; trivial + rw [e] at ce + apply ce + have et : s.topologicalClosure = ⊤ := @span_fourier_closure_eq_top _ (fact_iff.mpr Real.two_pi_pos) + rw [et] + trivial end HarmonicExtension @@ -691,7 +694,7 @@ theorem continuous_to_harmonic_complex {f : ℂ → ℂ} {c : ℂ} {r : ℝ} · exact continuous_const.add (continuous_const.mul (continuous_subtype_val.comp AddCircle.continuous_toCircle)) · simp only [mem_sphere_iff_norm, add_sub_cancel_left, Complex.norm_mul, Complex.norm_real, - Real.norm_eq_abs, norm_eq_of_mem_sphere, mul_one, abs_eq_self, rp.le, implies_true] + Real.norm_eq_abs, Circle.norm_coe, mul_one, abs_eq_self, rp.le, implies_true] rcases continuousExtend ⟨f', fc'⟩ c rp with ⟨g, e⟩ use g, e.gh; intro z zs generalize hz' : (↑r)⁻¹ * (z - c) = z' @@ -702,10 +705,11 @@ theorem continuous_to_harmonic_complex {f : ℂ → ℂ} {c : ℂ} {r : ℝ} rcases mem_addCircle_iff_abs.mp za' with ⟨t, tz⟩ have rr : c + r * t.toCircle = z := by rw [← tz, ← hz']; exact rri rp _ have h := e.b t - simp only [ContinuousMap.coe_mk] at h nth_rw 2 [← rr] rw [← h] - simp only [← hf', rr] + simp only [← hf'] + show f z = f (c + ↑r * ↑t.toCircle) + rw [rr] /-- Continuous functions on the sphere extend to harmonic functions on the ball (`ℝ` case) -/ theorem continuous_to_harmonic_real {f : ℂ → ℝ} {c : ℂ} {r : ℝ} (fc : ContinuousOn f (sphere c r)) : @@ -866,7 +870,7 @@ theorem SubharmonicOn.monotone_lim {f : ℕ → ℂ → ℝ} {g : ℂ → ℝ} { _ ≤ -(|f 0 z| + 0) := by rw [←hz]; bound _ = -|f 0 z| := by simp only [add_zero] _ ≤ f 0 z := (neg_abs_le _) - _ ≤ f n z := fm (by simp only [zero_le']) _ + _ ≤ f n z := fm (by simp only [zero_le]) _ · have mn : Monotone fun n ↦ f n z := fun _ _ ab ↦ fm ab z calc f n z _ ≤ g z := Monotone.ge_of_tendsto (f := fun n ↦ f n z) mn (ft z zs) n @@ -897,7 +901,7 @@ theorem Limsup.neg {f : ℕ → ℝ} : (atTop.limsup fun n ↦ f n) = -atTop.lim rw [Filter.limsup_eq]; rw [Filter.liminf_eq]; rw [Real.sInf_def] have ns : -{a | ∀ᶠ n in atTop, a ≤ -f n} = {a | ∀ᶠ n in atTop, f n ≤ a} := by apply Set.ext - simp only [Set.mem_neg, Set.mem_setOf_eq, neg_le_neg_iff, iff_self, forall_const] + simp only [Set.mem_neg, Set.mem_ofPred_eq, neg_le_neg_iff, iff_self, forall_const] simp_rw [← ns]; simp only [neg_neg] /-- `p : ENNReal → Prop` is true for all `ENNReal`s if it is true for `⊤` and positive reals -/ @@ -917,14 +921,14 @@ theorem le_liminf.simple {L : Type} [CompleteLinearOrder L] [DenselyOrdered L] { c ≤ atTop.liminf f ↔ ∀ d, d < c → ∀ᶠ n in atTop, d ≤ f n := by constructor · intro h d dc; rw [Filter.liminf_eq, le_sSup_iff, upperBounds] at h - simp only [Filter.eventually_atTop, ge_iff_le, Set.mem_setOf_eq, forall_exists_index] at h + simp only [Filter.eventually_atTop, ge_iff_le, Set.mem_ofPred_eq, forall_exists_index] at h specialize h d; contrapose h simp only [dc, not_forall, not_le, exists_prop, and_true, Filter.eventually_atTop, ge_iff_le, not_exists] at h ⊢ intro a n an; rcases h n with ⟨m, nm, fmd⟩ exact _root_.trans (an m nm) fmd.le · intro h; rw [Filter.liminf_eq, le_sSup_iff, upperBounds] - simp only [Filter.eventually_atTop, ge_iff_le, Set.mem_setOf_eq, forall_exists_index] + simp only [Filter.eventually_atTop, ge_iff_le, Set.mem_ofPred_eq, forall_exists_index] intro a ah; apply le_of_lt_imp_le; intro d dc rcases Filter.eventually_atTop.mp (h d dc) with ⟨n, hn⟩; exact ah n hn @@ -975,7 +979,7 @@ theorem SuperharmonicOn.hartogs {f : ℕ → ℂ → ENNReal} {s k : Set ℂ} {c -- Prepare d and c intro d dc by_cases dz : d = 0 - · simp only [dz, ge_iff_le, zero_le', imp_true_iff, Filter.eventually_atTop, exists_const] + · simp only [dz, ge_iff_le, zero_le, imp_true_iff, Filter.eventually_atTop, exists_const] have dp : d > 0 := pos_iff_ne_zero.mpr dz have df : d ≠ ⊤ := ne_top_of_lt dc have drp : d.toReal > 0 := ENNReal.toReal_pos dz df @@ -1039,7 +1043,7 @@ theorem SuperharmonicOn.hartogs {f : ℕ → ℂ → ENNReal} {s k : Set ℂ} {c set fi := fun z ↦ atTop.liminf fun n ↦ f n z have fm : ∀ n, _root_.AEMeasurable (f n) (volume.restrict (closedBall z r1)) := fun n ↦ AEMeasurable.mono_set r1s (fs n).AEMeasurable - have fatou' := @lintegral_liminf_le' _ _ (volume.restrict (closedBall z r1)) f fm + have fatou' := lintegral_liminf_le' (u := Filter.atTop) fm have im := @set_lintegral_mono_aEMeasurable _ _ (closedBall z r1) (fun _ ↦ c) _ measurableSet_closedBall fun _ zs ↦ fc _ (r1s zs) simp only [lintegral_const, Measure.restrict_apply, MeasurableSet.univ, Set.univ_inter] at im diff --git a/Ray/Koebe/Bieberbach.lean b/Ray/Koebe/Bieberbach.lean index a143fd1..87f38d0 100644 --- a/Ray/Koebe/Bieberbach.lean +++ b/Ray/Koebe/Bieberbach.lean @@ -139,7 +139,7 @@ lemma h_inj (b : Bier f) : InjOn (fun z ↦ z * b.h z⁻¹) (norm_Ioi 1) := by intro z zm w wm e have n : ∀ {x}, x ∈ norm_Ioi 1 → (x ^ 2)⁻¹ ∈ ball 0 1 := by intro x m - simp only [norm_Ioi, mem_setOf_eq, Metric.mem_ball, dist_zero_right, norm_inv, norm_pow] at m ⊢ + simp only [norm_Ioi, mem_ofPred_eq, Metric.mem_ball, dist_zero_right, norm_inv, norm_pow] at m ⊢ exact inv_lt_one_of_one_lt₀ (by exact one_lt_pow₀ (by bound) (by norm_num)) have e2 : (z * b.h z⁻¹) ^ 2 = (w * b.h w⁻¹) ^ 2 := by simp only at e; simp [e] rw [← inv_inj] at e2 diff --git a/Ray/Koebe/Gronwall.lean b/Ray/Koebe/Gronwall.lean index dcb83be..3ba8aa3 100644 --- a/Ray/Koebe/Gronwall.lean +++ b/Ray/Koebe/Gronwall.lean @@ -27,6 +27,8 @@ import Ray.Misc.MonotoneSeries import Ray.Misc.Subexp import Ray.Misc.Topology +attribute [local simp] Circle.norm_coe + /-! ## Grönwall's area theorem @@ -102,7 +104,7 @@ lemma hasFPowerSeriesOnBall (i : Gronwall f) : HasFPowerSeriesOnBall f (.ofScalars ℂ i.coeff) 0 1 := by have a0 := (i.fa 0 (by simp)).hasFPowerSeriesAt obtain ⟨p,a1⟩ := (analyticOnNhd_ball_iff_hasFPowerSeriesOnBall (by norm_num)).mp - (Metric.emetric_ball (α := ℂ) ▸ i.fa) + (Metric.eball_ofReal (α := ℂ) ▸ i.fa) have pe := a0.eq_formalMultilinearSeries a1.hasFPowerSeriesAt unfold coeff simp only [a0.eq_formalMultilinearSeries a1.hasFPowerSeriesAt] at a0 ⊢ @@ -113,7 +115,9 @@ lemma norm_coeff_le (i : Gronwall f) (r0 : 0 < r) (r1 : r < 1) : ∃ a ∈ Set.Ioo 0 1, ∃ C : ℝ, 0 < C ∧ ∀ n, ‖i.coeff n‖ ≤ C * (a / r) ^ n := by have le := i.hasFPowerSeriesOnBall.r_le set r' : ℝ≥0 := ⟨r, r0.le⟩ - have r'1 : r' < 1 := by rw [← NNReal.mk_one]; simp only [r', ← NNReal.coe_lt_coe]; simp [r1] + have r'1 : r' < 1 := by + have h : (r' : ℝ) < 1 := r1 + exact_mod_cast h have r'r : r' < (FormalMultilinearSeries.ofScalars ℂ i.coeff).radius := lt_of_lt_of_le (by simp only [ENNReal.coe_lt_one_iff, r'1]) le obtain ⟨a,am,C,C0,le⟩ := @@ -121,7 +125,9 @@ lemma norm_coeff_le (i : Gronwall f) (r0 : 0 < r) (r1 : r < 1) : refine ⟨a, am, C, C0, fun n ↦ ?_⟩ specialize le n rw [div_pow, ← mul_div_assoc, le_div_iff₀ (by bound)] - simpa [r'] using le + have le'' : ‖i.coeff n‖ * (r' : ℝ) ^ n ≤ C * a ^ n := by + simpa only [FormalMultilinearSeries.ofScalars_norm] using le + exact le'' def norm_prop (i : Gronwall f) (r : ℝ) : Prop := ∃ ac : ℝ × ℝ, ac.1 ∈ Set.Ioo 0 1 ∧ 0 < ac.2 ∧ ∀ n, ‖i.coeff n‖ ≤ ac.2 * (ac.1 * r) ^ n def a (i : Gronwall f) (r : ℝ) : ℝ := if p : i.norm_prop r then (choose p).1 else 1 @@ -245,7 +251,7 @@ lemma disk_subset_disk (i : Gronwall f) (rs : r ≤ s) : i.disk r ⊆ i.disk s : lemma disk_diff_disk (i : Gronwall f) (r1 : 1 ≤ r) (rs : r ≤ s) : i.disk s \ i.disk r = i.g '' annulus_oc 0 r s := by simp only [disk, compl_sdiff_compl, outer] - rw [← (i.inj.mono _).image_diff_subset] + rw [← (i.inj.mono _).image_sdiff_subset] · apply congr_arg₂ _ rfl ext w simp [norm_Ioi, annulus_oc, and_comm] @@ -274,7 +280,7 @@ lemma g_open (i : Gronwall f) : ∀ s ⊆ norm_Ioi 1, IsOpen s → IsOpen (i.g ' lemma isOpen_outer (i : Gronwall f) (r1 : 1 < r) : IsOpen (i.outer r) := by refine i.g_open _ ?_ isOpen_norm_Ioi intro z m - simp only [norm_Ioi, mem_setOf_eq] at m ⊢ + simp only [norm_Ioi, mem_ofPred_eq] at m ⊢ linarith -- Measurability of `i.outer` and `i.disk` @@ -291,7 +297,7 @@ lemma g_tendsto (i : Gronwall f) : Tendsto i.g (cobounded ℂ) (cobounded ℂ) : obtain ⟨s,s0,sh⟩ := f0 (1/2) (by simp) simp only [dist_zero_right, Complex.dist_eq, one_div] at sh simp only [tendsto_cobounded, Complex.norm_mul, hasBasis_cobounded_norm_lt.eventually_iff, - mem_setOf_eq, true_and] + mem_ofPred_eq, true_and] intro r use max (2 * r) s⁻¹ intro z lt @@ -313,7 +319,7 @@ lemma closure_outer (i : Gronwall f) : ∀ᶠ r in atTop, closure (i.outer r) = filter_upwards [Filter.eventually_gt_atTop 1] with r r1 apply subset_antisymm · intro w m - simp only [outer, mem_closure_iff_frequently, mem_image, norm_Ioi, norm_Ici, mem_setOf_eq, + simp only [outer, mem_closure_iff_frequently, mem_image, norm_Ioi, norm_Ici, mem_ofPred_eq, Filter.frequently_iff_seq_forall, Classical.skolem] at m ⊢ obtain ⟨s,st,z,m⟩ := m rcases tendsto_cobounded_or_mapClusterPt z atTop with t | ⟨a,c⟩ @@ -340,7 +346,7 @@ lemma closure_outer (i : Gronwall f) : ∀ᶠ r in atTop, closure (i.outer r) = calc ‖a‖ + e _ = ‖z n - (z n - a)‖ + e := by ring_nf _ ≥ ‖z n‖ - ‖z n - a‖ + e := by bound - _ > ‖z n‖ - e + e := by bound + _ > ‖z n‖ - e + e := by bound [mem_ball_iff_norm.mp za] _ = ‖z n‖ := by ring _ ≥ r := by bound [(m n).1] refine ⟨ra, ?_⟩ @@ -364,7 +370,7 @@ lemma frontier_outer (i : Gronwall f) : ∀ᶠ r in atTop, frontier (i.outer r) = i.g '' sphere 0 r := by filter_upwards [Filter.eventually_gt_atTop 1, i.closure_outer] with r r1 close rw [frontier, (i.isOpen_outer r1).interior_eq, close, outer, - ← (i.inj.mono (norm_Ici_subset_norm_Ioi r1)).image_diff_subset norm_Ioi_subset_norm_Ici, + ← (i.inj.mono (norm_Ici_subset_norm_Ioi r1)).image_sdiff_subset norm_Ioi_subset_norm_Ici, norm_Ici_diff_norm_Ioi] /-! @@ -389,7 +395,7 @@ lemma wind (i : Gronwall f) : ∀ᶠ r in atTop, WindDiff (i.gc r) := by · exact (i.ga (by simp [abs_of_pos r0, r1])).continuousAt.comp (by fun_prop) · intro x y e simp only [gc, Units.snap_mk1] at e - simpa only [mul_eq_mul_left_iff, SetLike.coe_eq_coe, Complex.ofReal_eq_zero, r0.ne', + simpa only [mul_eq_mul_left_iff, Circle.coe_inj, Complex.ofReal_eq_zero, r0.ne', or_false] using (inj.eq_iff (by simp [r0.le]) (by simp [r0.le])).mp e · have e : ∀ t, (i.gc r (Circle.exp t)).val = i.g (circleMap 0 r t) := by intro t @@ -666,7 +672,7 @@ lemma sum_integral_comm (i : Gronwall f) : ∀ᶠ r in atTop, · intro n; apply Continuous.aestronglyMeasurable; fun_prop · simp [i.le_ut r1] · simp [i.summable_ut r1] - · apply intervalIntegrable_const; simp + · apply intervalIntegrable_const · simp [(hasSum_inner w _).summable.hasSum] /-- Diagonal term integrals -/ @@ -824,7 +830,7 @@ lemma analyticAt_series (i : Gronwall f) {z : ℂ} (z1 : 1 < ‖z‖) : lemma volume_diff_eq (i : Gronwall f) (r1 : 1 < r) (rs : r ≤ s) : volume.real (i.disk s \ i.disk r) = volume.real (i.disk s) - volume.real (i.disk r) := by - rw [← MeasureTheory.measureReal_diff (i.disk_subset_disk rs) (i.measurableSet_disk r1)] + rw [← MeasureTheory.measureReal_sdiff (i.disk_subset_disk rs) (i.measurableSet_disk r1)] /-! ### Area within small annuli as an integral @@ -846,7 +852,7 @@ def volume_integral_c (i : Gronwall f) (r s : ℝ) (z : ℂ) : ℂ := ∫ w in annulus_cc 0 r s, i.integrand w z lemma wz_norm (r1 : 1 < r) (wm : w ∈ annulus_cc 0 r s) (zr : r⁻¹ < ‖z‖) : 1 < ‖w‖ * ‖z‖ := by - simp only [annulus_cc, mem_diff, Metric.mem_closedBall, dist_zero_right, Metric.mem_ball, + simp only [annulus_cc, mem_sdiff, Metric.mem_closedBall, dist_zero_right, Metric.mem_ball, not_lt] at wm zr calc ‖w‖ * ‖z‖ _ > r * r⁻¹ := mul_lt_mul' wm.2 zr (by bound) (by linarith) @@ -877,7 +883,7 @@ lemma integrable_sq_norm (i : Gronwall f) (r1 : 1 < r) : IntegrableOn (fun w ↦ ‖deriv i.g w‖ ^ 2) (annulus_cc 0 r s) := by apply ContinuousOn.integrableOn_compact isCompact_annulus_cc intro z m - simp only [annulus_cc, mem_diff, Metric.mem_closedBall, dist_zero_right, Metric.mem_ball, + simp only [annulus_cc, mem_sdiff, Metric.mem_closedBall, dist_zero_right, Metric.mem_ball, not_lt] at m exact ((i.ga (by linarith)).deriv.continuousAt.norm.pow 2).continuousWithinAt @@ -929,7 +935,7 @@ lemma small_volume_eq_integral_c (i : Gronwall f) (r1 : 1 < r) (rs : r ≤ s) (z have tn : ∀ w, ‖t w‖ = ‖w‖ * z := by simp [t, z0.le] have ti : t '' annulus_cc 0 (r / ‖z‖) (s / ‖z‖) = annulus_cc 0 r s := by ext a - simp only [annulus_cc, mem_image, mem_diff, Metric.mem_closedBall, dist_zero_right, + simp only [annulus_cc, mem_image, mem_sdiff, Metric.mem_closedBall, dist_zero_right, Metric.mem_ball, not_lt, le_div_iff₀ z0, div_le_iff₀ z0, Real.norm_eq_abs, abs_of_pos z0] constructor · intro ⟨b,⟨bs,rb⟩,ba⟩ @@ -1004,7 +1010,7 @@ lemma small_volume_eq_c (i : Gronwall f) (r1 : 1 < r) : rwa [← sub_eq_zero] have ua : AnalyticOnNhd ℂ u (norm_Ioi r⁻¹) := by intro z zr - simp only [norm_Ioi, mem_setOf_eq] at zr + simp only [norm_Ioi, mem_ofPred_eq] at zr have zr' := (inv_lt_iff_one_lt_mul₀' r0).mp zr refine AnalyticAt.sub (AnalyticAt.sub ?_ ?_) ?_ · refine (i.analyticAt_series (lt_of_lt_of_le zr' ?_)).comp (by fun_prop) @@ -1029,12 +1035,12 @@ lemma small_volume_eq_c (i : Gronwall f) (r1 : 1 < r) : bound have ue : EqOn u 0 (norm_Ioi r⁻¹) := by refine ua.eqOn_zero_of_preconnected_of_frequently_eq_zero isPreconnected_norm_Ioi ?_ u0 - simp only [norm_Ioi, Complex.ofReal_div, mem_setOf_eq, Complex.norm_div, Complex.norm_real, + simp only [norm_Ioi, Complex.ofReal_div, mem_ofPred_eq, Complex.norm_div, Complex.norm_real, Real.norm_eq_abs, abs_of_pos s0, abs_of_pos r0] rw [div_eq_mul_inv] bound apply ue - simp only [norm_Ioi, mem_setOf_eq, one_mem, CStarRing.norm_of_mem_unitary] + simp only [norm_Ioi, mem_ofPred_eq, one_mem, CStarRing.norm_of_mem_unitary] bound /-- Our large radius formula holds for small radii, real version -/ @@ -1094,7 +1100,7 @@ lemma volume_one_sum (i : Gronwall f) : · simp only [disk, ← compl_iUnion, compl_subset_compl, outer, ← image_iUnion] apply image_mono intro z m - simp only [norm_Ioi, mem_setOf_eq, mem_iUnion] at m ⊢ + simp only [norm_Ioi, mem_ofPred_eq, mem_iUnion] at m ⊢ obtain ⟨n, lt⟩ := exists_nat_gt (‖z‖ - 1)⁻¹ refine ⟨n, ?_⟩ simp only [r, add_comm (1 : ℝ), ← lt_sub_iff_add_lt, one_div] @@ -1113,7 +1119,7 @@ lemma volume_one_sum (i : Gronwall f) : have rm : ∀ {c}, Tendsto (fun n ↦ c * r n ^ 2) atTop (𝓝 c) := fun {c} ↦ by simpa using tendsto_const_nhds.mul (tr.pow 2) have rd : ∀ {c k}, Tendsto (fun n ↦ c / r n ^ k) atTop (𝓝 c) := fun {c k} ↦ by - simpa using tendsto_const_nhds.div (tr.pow k) + simpa [Pi.div_def] using tendsto_const_nhds.div (tr.pow k) have s := fun n ↦ i.small_volume_sum_nonneg (r1 n) have mono : Monotone fun n ↦ i.gronwall_nonneg (r n) := by intro n m nm diff --git a/Ray/Koebe/Snap.lean b/Ray/Koebe/Snap.lean index 1f435ba..763301d 100644 --- a/Ray/Koebe/Snap.lean +++ b/Ray/Koebe/Snap.lean @@ -26,8 +26,8 @@ public def snap (z : ℂ) : Circle := public lemma coe_snap {z : ℂ} (z0 : z ≠ 0) : (snap z).val = z / ‖z‖ := by simp only [snap, z0, ↓reduceDIte, div_eq_mul_inv] -@[simp] public lemma norm_snap {z : ℂ} : ‖(snap z).val‖ = 1 := by - simp only [snap, norm_eq_of_mem_sphere] +@[simp] public lemma norm_snap {z : ℂ} : ‖(snap z).val‖ = 1 := + Circle.norm_coe _ @[simp] public lemma arg_snap {z : ℂ} (z0 : z ≠ 0) : arg (snap z) = arg z := by simp only [snap, z0, ↓reduceDIte, div_eq_mul_inv] @@ -47,32 +47,39 @@ public lemma snap_eq_snap_iff {z w : ℂ} (z0 : z ≠ 0) (w0 : w ≠ 0) : @[simp] public lemma snap_mul {z w : ℂ} (z0 : z ≠ 0) (w0 : w ≠ 0) : snap (z * w) = snap z * snap w := by - simp only [snap, mul_eq_zero, z0, w0, or_self, ↓reduceDIte, Complex.norm_mul, Complex.ofReal_mul, - div_eq_mul_inv, mul_inv_rev, Circle.ext_iff, Circle.coe_mul] - ring + apply Circle.ext + simp only [Circle.coe_mul, coe_snap z0, coe_snap w0, coe_snap (mul_ne_zero z0 w0), + Complex.norm_mul, Complex.ofReal_mul] + rw [div_mul_div_comm] @[simp] public lemma snap_div {z w : ℂ} (z0 : z ≠ 0) (w0 : w ≠ 0) : snap (z / w) = snap z / snap w := by - simp only [snap, div_eq_mul_inv, mul_eq_zero, z0, inv_eq_zero, w0, or_self, ↓reduceDIte, norm_mul, - norm_inv, Complex.ofReal_mul, Complex.ofReal_inv, mul_inv_rev, inv_inv, Circle.ext_iff, - Circle.coe_mul, Circle.coe_inv] - ring + apply Circle.ext + simp only [Circle.coe_div, coe_snap z0, coe_snap w0, coe_snap (div_ne_zero z0 w0), + Complex.norm_div, Complex.ofReal_div] + rw [div_div_div_comm] @[simp] public lemma snap_zero : snap 0 = 1 := by simp only [snap, ↓reduceDIte] @[simp] public lemma snap_of_pos {t : ℝ} (t0 : 0 < t) : snap (t : ℂ) = 1 := by - simp only [snap, Complex.ofReal_eq_zero, t0.ne', ↓reduceDIte, Complex.norm_real, Real.norm_eq_abs, - abs_of_pos t0, ne_eq, not_false_eq_true, div_self, Circle.ext_iff, OneMemClass.coe_one] + apply Circle.ext + have n : (t : ℂ) ≠ 0 := by exact_mod_cast t0.ne' + simp only [coe_snap n, Complex.norm_real, Real.norm_eq_abs, abs_of_pos t0, Circle.coe_one] + rw [div_self n] @[simp] public lemma snap_mul_of_pos {t : ℝ} (t0 : 0 < t) {z : ℂ} : snap (t * z) = snap z := by - simp only [snap, mul_eq_zero, Complex.ofReal_eq_zero, t0.ne', false_or, Complex.norm_mul, - Complex.norm_real, Real.norm_eq_abs, abs_of_pos t0, Complex.ofReal_mul, div_mul_eq_div_div, - ne_eq, not_false_eq_true, mul_div_cancel_left₀] + rcases eq_or_ne z 0 with rfl | z0 + · simp only [mul_zero] + · have n : (t : ℂ) ≠ 0 := by exact_mod_cast t0.ne' + apply Circle.ext + simp only [coe_snap (mul_ne_zero n z0), coe_snap z0, Complex.norm_mul, Complex.norm_real, + Real.norm_eq_abs, abs_of_pos t0, Complex.ofReal_mul, div_mul_eq_div_div, ne_eq, + not_false_eq_true, mul_div_cancel_left₀, n] @[simp] public lemma snap_circle (z : Circle) : snap z.val = z := by - simp only [snap, Circle.coe_ne_zero, ↓reduceDIte, norm_eq_of_mem_sphere, Complex.ofReal_one, - div_one, Subtype.coe_eta] + apply Circle.ext + simp only [coe_snap z.coe_ne_zero, Circle.norm_coe, Complex.ofReal_one, div_one] @[simp] public lemma norm_mul_snap {z : ℂ} (z0 : z ≠ 0) : ‖z‖ * (snap z).val = z := by have n : (‖z‖ : ℂ) ≠ 0 := by simpa @@ -81,16 +88,17 @@ public lemma snap_eq_snap_iff {z w : ℂ} (z0 : z ≠ 0) (w0 : w ≠ 0) : /-- Alternative definition using `Set.codRestrict` -/ lemma snap_eq_restrict : snap = codRestrict (fun z : ℂ ↦ if z = 0 then 1 else z / ‖z‖) (Submonoid.unitSphere ℂ) - (by intro z; simp only; split_ifs with h; all_goals simp [h]) := by + (by intro z; split_ifs with h; all_goals simp [h]) := by ext z by_cases z0 : z = 0 all_goals simp [z0, coe_snap] public lemma continuousAt_snap {z : ℂ} (z0 : z ≠ 0) : ContinuousAt snap z := by - rw [snap_eq_restrict, continuousAt_codRestrict_iff] - have e : ∀ᶠ w : ℂ in 𝓝 z, (if w = 0 then 1 else w / ‖w‖) = w / ‖w‖ := by - filter_upwards [eventually_ne_nhds z0] - aesop + have i : Topology.IsInducing ((↑) : Circle → ℂ) := Topology.IsInducing.subtypeVal + refine i.continuousAt_iff.mpr ?_ + have e : (fun w : ℂ ↦ (snap w).val) =ᶠ[𝓝 z] fun w ↦ w / ‖w‖ := by + filter_upwards [eventually_ne_nhds z0] with w w0 + exact coe_snap w0 refine ContinuousAt.congr_of_eventuallyEq ?_ e exact continuousAt_id.div (Complex.continuous_ofReal.comp continuous_norm).continuousAt (by simpa only [ne_eq, Complex.ofReal_eq_zero, norm_eq_zero]) @@ -108,11 +116,14 @@ public lemma continuousAt_snap {z : ℂ} (z0 : z ≠ 0) : ContinuousAt snap z := public lemma snap_unit (z : ℂˣ) : snap z = ⟨z / ‖z.val‖, by simp [Submonoid.unitSphere]⟩ := by simp only [snap, Units.ne_zero, ↓reduceDIte] + rfl @[simp] public lemma snap_exp_mul_I {t : ℝ} : snap (Complex.exp (t * I)) = Circle.exp t := by simp [Circle.ext_iff, coe_snap] -@[simp] lemma snap_one : snap 1 = 1 := by simp [snap, Circle.ext_iff] +@[simp] lemma snap_one : snap 1 = 1 := by + simp only [snap, one_ne_zero, ↓reduceDIte, norm_one, Complex.ofReal_one, div_one] + rfl /-! ### Snap calculus diff --git a/Ray/Koebe/Wind.lean b/Ray/Koebe/Wind.lean index b2cc78a..5319c28 100644 --- a/Ray/Koebe/Wind.lean +++ b/Ray/Koebe/Wind.lean @@ -48,10 +48,10 @@ public def h (i : Wind f) : Homeomorph Circle Circle := i.isHomeomorph.homeomorp lemma f_h_symm (i : Wind f) (z : Circle) : f (i.h.symm z) = ‖(f (i.h.symm z)).val‖ • z.val := by - have h := i.h.apply_symm_apply z - simp only [Wind.h_apply, Circle.ext_iff, Complex.real_smul, snap_unit] at h ⊢ - rwa [mul_comm, ← div_eq_iff] - simp + have h := congrArg Subtype.val (i.h.apply_symm_apply z) + rw [Wind.h_apply, coe_snap (Units.ne_zero _)] at h + rw [Complex.real_smul, mul_comm, ← div_eq_iff (by simp)] + exact h @[simp] lemma h_symm_f (i : Wind f) (z : Circle) : i.h.symm (snap (f z)) = z := i.h.symm_apply_apply z @@ -117,7 +117,7 @@ public lemma right_inv (i : Wind f) : Function.RightInverse i.fi i.fe := by by_cases w0 : w = 0 · simp only [w0, fe_zero, fi_zero] · simp only [fe, fi, norm_mul, norm_div, Complex.norm_real, Real.norm_eq_abs, - abs_norm, norm_eq_of_mem_sphere, mul_one, Complex.real_smul, Complex.ofReal_div] + abs_norm, Circle.norm_coe, mul_one, Complex.real_smul, Complex.ofReal_div] rw [← Complex.ofReal_div, snap_mul, snap_of_pos, one_mul, i.f_h_symm] all_goals simp [Complex.real_smul, Complex.norm_real, ne_eq, w0, not_false_eq_true, mul_one, Complex.ofReal_div] @@ -133,8 +133,10 @@ public lemma continuous_fe (i : Wind f) : Continuous i.fe := by simp only [z0, dist_zero_right, fe, Complex.real_smul, norm_zero, snap_zero, zero_smul, Complex.norm_mul, Complex.norm_real, norm_norm, lt_div_iff₀ i.max_pos] at wz ⊢ exact lt_of_le_of_lt (by bound) wz - · apply ContinuousAt.smul - · exact continuous_norm.continuousAt + · show ContinuousAt (fun z : ℂ ↦ ‖z‖ • ((f (snap z)).val : ℂ)) z + simp only [Complex.real_smul] + apply ContinuousAt.mul + · exact Complex.continuous_ofReal.continuousAt.comp continuous_norm.continuousAt · exact Units.continuous_val.continuousAt.comp (i.fc.continuousAt.comp (continuousAt_snap z0)) public lemma continuous_fi (i : Wind f) : Continuous i.fi := by @@ -144,7 +146,7 @@ public lemma continuous_fi (i : Wind f) : Continuous i.fi := by · refine Metric.continuousAt_iff.mpr fun ε ε0 ↦ ⟨ε * i.min, by bound, fun z zw ↦ ?_⟩ simp only [w0, dist_zero_right, ← div_lt_iff₀ i.min_pos, fi, norm_zero, Complex.ofReal_zero, snap_zero, zero_div, zero_mul, Complex.norm_mul, Complex.norm_div, Complex.norm_real, - norm_norm, norm_eq_of_mem_sphere, mul_one] at zw ⊢ + norm_norm, Circle.norm_coe, mul_one] at zw ⊢ exact lt_of_le_of_lt (by bound) zw · apply ContinuousAt.mul (ContinuousAt.div ?_ ?_ ?_) ?_ · fun_prop @@ -196,7 +198,7 @@ public lemma sphere_eq (i : Wind f) : i.g '' sphere 0 1 = range (fun z ↦ (f z) simp only [x1, Complex.ofReal_one, one_mul] at e exact ⟨_, e⟩ · intro ⟨x,e⟩ - exact ⟨x.val, by simp, by simp [e]⟩ + exact ⟨x.val, by simp [Circle.norm_coe], by simp [Circle.norm_coe, e]⟩ lemma frontier_disk (i : Wind f) : frontier i.disk = i.g '' sphere 0 1 := by simp only [disk, ← Homeomorph.image_frontier] @@ -209,7 +211,7 @@ public lemma frontier_outer (i : Wind f) : frontier i.outer = i.g '' sphere 0 1 public lemma compl_outer (i : Wind f) : i.outerᶜ = i.disk := by simp only [outer, disk, norm_Ioi, ← Equiv.image_compl, ← Homeomorph.coe_toEquiv, - Equiv.image_eq_iff_eq, compl_setOf, not_lt] + Equiv.image_eq_iff_eq, compl_ofPred, not_lt] ext z simp @@ -230,7 +232,7 @@ public lemma large_mem_outer (i : Wind f) : ∀ᶠ z in cobounded ℂ, z ∈ i.o intro z lt simp only [outer, mem_image] refine ⟨i.g.symm z, ?_, by simp only [i.g.apply_symm_apply]⟩ - simp only [norm_Ioi, i.g_symm_apply, mem_setOf_eq, Complex.norm_mul, Complex.norm_div, - Complex.norm_real, norm_norm, norm_eq_of_mem_sphere, mul_one] + simp only [norm_Ioi, i.g_symm_apply, mem_ofPred_eq, Complex.norm_mul, Complex.norm_div, + Complex.norm_real, norm_norm, Circle.norm_coe, mul_one] rw [one_lt_div₀ (by simp)] exact lt_of_le_of_lt i.le_max lt diff --git a/Ray/Koebe/WindArea.lean b/Ray/Koebe/WindArea.lean index f2b37bc..27feea6 100644 --- a/Ray/Koebe/WindArea.lean +++ b/Ray/Koebe/WindArea.lean @@ -157,7 +157,7 @@ lemma measurableSet_gs_square (i : WindDiff f) : MeasurableSet (i.gs '' square) public theorem volume_eq (i : WindDiff f) : volume.real i.wind.disk = 2⁻¹ * ∫ t in (-π)..π, |inner ℝ (i.fe t * I) (i.dfe t)| := by simp only [i.disk_eq, image_union, MeasureTheory.Measure.real, image_singleton, - measure_union_eq_right, MeasureTheory.NoAtoms.measure_singleton] + measure_union_eq_right, MeasureTheory.measure_singleton] rw [MeasurableEquiv.image_symm, Complex.volume_preserving_equiv_real_prod.measure_preimage i.measurableSet_gs_square.nullMeasurableSet] have ie : ∫ z in i.gs '' square, (1 : ℝ) = volume.real (i.gs '' square) • 1 := diff --git a/Ray/Mandelbrot.lean b/Ray/Mandelbrot.lean index 99b6253..6a66b2d 100644 --- a/Ray/Mandelbrot.lean +++ b/Ray/Mandelbrot.lean @@ -27,7 +27,7 @@ noncomputable section /-- The Mandelbrot set is the `d = 2` Multibrot set -/ public theorem mandelbrot_eq_multibrot : mandelbrot = multibrot 2 := by ext c - simp only [mandelbrot, mem_setOf_eq, multibrot, f_f'_iter, tendsto_inf_iff_tendsto_cobounded, + simp only [mandelbrot, mem_ofPred_eq, multibrot, f_f'_iter, tendsto_inf_iff_tendsto_cobounded, tendsto_cobounded_iff_norm_tendsto_atTop] rfl diff --git a/Ray/Manifold/Defs.lean b/Ray/Manifold/Defs.lean index 1c020d3..d53dcd3 100644 --- a/Ray/Manifold/Defs.lean +++ b/Ray/Manifold/Defs.lean @@ -39,9 +39,9 @@ public theorem extChartAt_eq_refl [NormedAddCommGroup E] [NormedSpace 𝕜 E] [T /-- `extChartAt = refl` for `I = modelWithCornersSelf 𝕜 E` -/ public instance extChartEqReflSelf [NormedAddCommGroup E] [NormedSpace 𝕜 E] : ExtChartEqRefl (modelWithCornersSelf 𝕜 E) := ⟨by - simp only [OpenPartialHomeomorph.singletonChartedSpace_chartAt_eq, - OpenPartialHomeomorph.refl_partialEquiv, PartialEquiv.refl_source, forall_const, extChartAt, - OpenPartialHomeomorph.extend, modelWithCornersSelf_partialEquiv, PartialEquiv.refl_trans]⟩ + simp only [extChartAt, OpenPartialHomeomorph.extend, chartAt_self_eq, + OpenPartialHomeomorph.refl_partialEquiv, modelWithCornersSelf_partialEquiv, + PartialEquiv.trans_refl, forall_const]⟩ /-- `extChartAt = refl` extends to products -/ public instance extChartEqReflProd [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace A] diff --git a/Ray/Manifold/GlobalInverse.lean b/Ray/Manifold/GlobalInverse.lean index 234798a..fc93ac7 100644 --- a/Ray/Manifold/GlobalInverse.lean +++ b/Ray/Manifold/GlobalInverse.lean @@ -62,9 +62,9 @@ public theorem global_complex_inverse_fun_open {f : ℂ → S → T} [Nonempty S rw [left] at e; exact (Prod.ext_iff.mp e).2 have ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ q : ℂ × T in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = (i p m).g q.1 q.2 := by - intro ⟨c, z⟩ m; simp only + intro ⟨c, z⟩ m have n := nontrivialMAnalyticAt_of_mfderiv_ne_zero - (fa.contMDiffAt (so.mem_nhds m)).along_snd (nc _ m); simp only at n + (fa.contMDiffAt (so.mem_nhds m)).along_snd (nc _ m) simp only [n.nhds_eq_map_nhds_param (fa.contMDiffAt (so.mem_nhds m)), Filter.eventually_map] apply (i _ m).left_inv.mp; apply (so.eventually_mem m).mp refine .of_forall fun ⟨e, w⟩ wm gf ↦ ?_ diff --git a/Ray/Manifold/Inverse.lean b/Ray/Manifold/Inverse.lean index 42d2ac0..f7fb1df 100644 --- a/Ray/Manifold/Inverse.lean +++ b/Ray/Manifold/Inverse.lean @@ -131,7 +131,7 @@ lemma Cinv.dei_de (i : Cinv f c z) : ∀ t, i.dei (i.de t) = t := by intro t have h := ContinuousLinearMap.ext_iff.mp (extChartAt_mderiv_right_inverse' (mem_extChartAt_source (I := I) z)) t - simp only [ContinuousLinearMap.comp_apply, ContinuousLinearMap.id_apply] at h; exact h + exact h variable [cmt : IsManifold I ω T] @@ -173,21 +173,21 @@ lemma Cinv.de_dei' (i : Cinv f c z) : ∀ t, i.de' (i.dei' t) = t := by intro t have h := ContinuousLinearMap.ext_iff.mp (extChartAt_mderiv_right_inverse' (mem_extChartAt_source (I := I) (f c z))) t - simp only [ContinuousLinearMap.comp_apply, ContinuousLinearMap.id_apply] at h; exact h + exact h lemma Cinv.dhi_dh (i : Cinv f c z) : ∀ t, i.dhi (i.dh t) = t := by intro ⟨u, v⟩ simp only [Cinv.dh, Cinv.dhi, dc, dz, Cinv.dfi', Cinv.df', Cinv.df, i.dei_de', i.dei_de, i.dfzi_dfz, ContinuousLinearMap.comp_apply, ContinuousLinearMap.prod_apply, - ContinuousLinearMap.sub_apply, ContinuousLinearMap.coe_fst', ContinuousLinearMap.coe_snd', - ContinuousLinearMap.add_apply, ContinuousLinearMap.map_add, add_sub_cancel_left] + _root_.sub_apply, ContinuousLinearMap.coe_fst', ContinuousLinearMap.coe_snd', + _root_.add_apply, ContinuousLinearMap.map_add, add_sub_cancel_left] lemma Cinv.dh_dhi (i : Cinv f c z) : ∀ t, i.dh (i.dhi t) = t := by intro ⟨u, v⟩ simp only [Cinv.dh, Cinv.dhi, dc, dz, Cinv.dfi', Cinv.df', Cinv.df, i.de_dei', i.de_dei, i.dfz_dfzi, ContinuousLinearMap.comp_apply, ContinuousLinearMap.prod_apply, - ContinuousLinearMap.sub_apply, ContinuousLinearMap.coe_fst', ContinuousLinearMap.coe_snd', - ContinuousLinearMap.add_apply, ContinuousLinearMap.map_add, ContinuousLinearMap.map_sub, + _root_.sub_apply, ContinuousLinearMap.coe_fst', ContinuousLinearMap.coe_snd', + _root_.add_apply, ContinuousLinearMap.map_add, ContinuousLinearMap.map_sub, add_sub_cancel_left, ← add_sub_assoc] /-- `dh` as a `ContinuousLinearEquiv` -/ diff --git a/Ray/Manifold/Manifold.lean b/Ray/Manifold/Manifold.lean index 350990f..35145fb 100644 --- a/Ray/Manifold/Manifold.lean +++ b/Ray/Manifold/Manifold.lean @@ -109,18 +109,13 @@ theorem MDifferentiableAt.hasMFDerivAt_uncurry {f : N → O → P} {y : N} {z : have fh := fd.hasMFDerivAt; rw [hdf] at fh suffices e : df = df0.comp fst + df1.comp snd by rw [e] at fh; exact fh apply ContinuousLinearMap.ext; intro ⟨u, v⟩ - simp only [Function.uncurry_apply_pair, ContinuousLinearMap.add_apply, - ContinuousLinearMap.comp_apply] have hu : ∀ u : TangentSpace J y, df (u, 0) = df0 u := by intro u have d : HasMFDerivAt J L (uncurry f ∘ fun x ↦ (x, z)) y (df.comp ((ContinuousLinearMap.id 𝕜 (TangentSpace J y)).prod 0)) := fh.comp y ((hasMFDerivAt_id _).prodMk (hasMFDerivAt_const _ _)) simp only [hasMFDerivAt_unique fh0 d] - refine Eq.trans (congr_arg _ ?_) (ContinuousLinearMap.comp_apply _ _ _).symm - refine Eq.trans ?_ (ContinuousLinearMap.prod_apply _ _ _).symm - simp only [ContinuousLinearMap.zero_apply, Prod.mk.injEq, and_true] - exact rfl + rfl have hv : ∀ v : TangentSpace K z, df (0, v) = df1 v := by intro v have d : HasMFDerivAt K L (uncurry f ∘ fun x ↦ (y, x)) z (df.comp @@ -128,14 +123,10 @@ theorem MDifferentiableAt.hasMFDerivAt_uncurry {f : N → O → P} {y : N} {z : (ContinuousLinearMap.id 𝕜 (TangentSpace K z)))) := fh.comp z ((hasMFDerivAt_const _ _).prodMk (hasMFDerivAt_id _)) rw [hasMFDerivAt_unique fh1 d] - refine Eq.trans (congr_arg _ ?_) (ContinuousLinearMap.comp_apply _ _ _).symm - refine Eq.trans ?_ (ContinuousLinearMap.prod_apply _ _ _).symm - simp only [Prod.mk.injEq] - exact ⟨(ContinuousLinearMap.zero_apply _).symm, rfl⟩ + rfl have e : (u, v) = (u, 0) + (0, v) := by simp only [Prod.mk_add_mk, add_zero, zero_add] nth_rw 1 [e] - rw [map_add] - exact congr_arg₂ _ (hu u) (hv v) + exact (map_add df _ _).trans (by rw [hu u, hv v]; rfl) /-- `HasMFDerivAt` composition for curried functions -/ public theorem MDifferentiableAt.hasMFDerivAt_comp2 {f : N → O → P} {g : M → N} {h : M → O} {x : M} @@ -148,7 +139,6 @@ public theorem MDifferentiableAt.hasMFDerivAt_comp2 {f : N → O → P} {g : M (fh1 : HasMFDerivAt K L (fun y ↦ f (g x) y) (h x) df1) : HasMFDerivAt I L (fun y ↦ f (g y) (h y)) x (df0.comp dg + df1.comp dh) := by have fh := (fd.hasMFDerivAt_uncurry fh0 fh1).comp x (gh.prodMk hh) - simp only [ContinuousLinearMap.add_comp, ContinuousLinearMap.comp_assoc] at fh exact fh /-- More general version of `hasMFDerivAt_iff_hasDerivAt`. @@ -158,10 +148,11 @@ public theorem hasMFDerivAt_iff_hasFDerivAt' {I : ModelWithCorners 𝕜 E A} [I. {J : ModelWithCorners 𝕜 F B} [J.Boundaryless] [ChartedSpace B F] [IsManifold J ⊤ F] [ExtChartEqRefl J] {f : E → F} {x : E} {f' : E →L[𝕜] F} : HasMFDerivAt I J f x f' ↔ HasFDerivAt f f' x := by - simp only [HasMFDerivAt, ModelWithCorners.range_eq_univ, hasFDerivWithinAt_univ, + simp only [HasMFDerivAt, ModelWithCorners.range_eq_univ, writtenInExtChartAt, extChartAt_eq_refl, Function.comp_def, PartialEquiv.refl_coe, PartialEquiv.refl_symm, id] - exact ⟨fun x ↦ x.2, fun d ↦ ⟨d.continuousAt, d⟩⟩ + exact ⟨fun x ↦ hasFDerivWithinAt_univ.mp x.2, + fun d ↦ ⟨d.continuousAt, hasFDerivWithinAt_univ.mpr d⟩⟩ /-- Variant of `mfderiv_comp` that doesn't use `∘` for better inference -/ theorem mfderiv_comp' {f : M → N} (x : M) {g : N → O} (hg : MDifferentiableAt J K g (f x)) diff --git a/Ray/Manifold/Nonseparating.lean b/Ray/Manifold/Nonseparating.lean index 74f2458..90f442f 100644 --- a/Ray/Manifold/Nonseparating.lean +++ b/Ray/Manifold/Nonseparating.lean @@ -46,7 +46,7 @@ theorem Nonseparating.univ_prod [LocallyConnectedSpace X] {t : Set Y} (n : Nonse rcases locallyConnectedSpace_iff_subsets_isOpen_isConnected.mp (by infer_instance) a u0 n0 with ⟨c0, cs0, co0, cm0, cc0⟩ use c0 ×ˢ c1; refine ⟨?_, ?_, ?_⟩ - · intro ⟨b, y⟩ m'; simp only [mem_prod_eq, mem_diff, mem_univ, true_and] at m' ⊢ + · intro ⟨b, y⟩ m'; simp only [mem_prod_eq, mem_sdiff, mem_univ, true_and] at m' ⊢ refine ⟨?_, (cs1 m'.2).2⟩; apply uu; use cs0 m'.1, (cs1 m'.2).1 · rw [e, nhdsWithin_prod_eq, nhdsWithin_univ]; exact Filter.prod_mem_prod (co0.mem_nhds cm0) cn1 · exact cc0.isPreconnected.prod cp1 @@ -86,13 +86,13 @@ theorem Nonseparating.complexManifold {t : Set S} apply Set.ext; intro x; simp only [mem_inter_iff, mem_preimage, mem_image]; constructor · intro ⟨xz, xc⟩; refine ⟨_, xc, ?_⟩; simp only [PartialEquiv.left_inv _ xz] · intro ⟨y, yc, yx⟩; rw [← yx] - have xc := cs yc; simp only [mem_diff, mem_inter_iff, mem_preimage] at xc + have xc := cs yc; simp only [mem_sdiff, mem_inter_iff, mem_preimage] at xc have yz := xc.1.1; use PartialEquiv.map_target _ yz simp only [PartialEquiv.right_inv _ yz, yc] use(extChartAt I z).source ∩ extChartAt I z ⁻¹' c; refine ⟨?_, ?_, ?_⟩ · intro x xm; simp only [mem_inter_iff, mem_preimage] at xm; rcases xm with ⟨xz, xc⟩ replace xc := cs xc - simp only [mem_diff, mem_inter_iff, mem_preimage, PartialEquiv.map_source _ xz, true_and, + simp only [mem_sdiff, mem_inter_iff, mem_preimage, PartialEquiv.map_source _ xz, true_and, PartialEquiv.left_inv _ xz] at xc exact xc · rw [e]; convert Filter.image_mem_map cn @@ -111,7 +111,7 @@ theorem Nonseparating.complexManifold {t : Set S} · intro ⟨⟨y, ⟨⟨yz, yt⟩, yx⟩⟩, _⟩ simp only [← yx, yt, PartialEquiv.map_target _ yz, not_false_iff, true_and] · rw [e]; apply cp.image; apply (continuousOn_extChartAt_symm z).mono - exact _root_.trans cs (_root_.trans diff_subset inter_subset_left) } + exact _root_.trans cs (_root_.trans sdiff_subset inter_subset_left) } /-- A sufficient condition on `t` for `s \ t` to be preconnected, for `s` open and preconnected. Roughly, `t` has empty interior and there are arbitrarily small connected rings around each @@ -129,22 +129,22 @@ theorem IsPreconnected.open_diff {s t : Set X} (sc : IsPreconnected s) (so : IsO exact (o.eventually_mem xu).mp (.of_forall fun q m ↦ subset_union_left m) by_cases xt : x ∉ t · contrapose xu; clear xu - simp only [mem_union, mem_setOf, xt, false_and, and_false, or_false, ← hf] at m + simp only [mem_union, mem_ofPred, xt, false_and, and_false, or_false, ← hf] at m exact m simp only [not_not] at xt have n := m - simp only [mem_union, xt, xu, false_or, true_and, mem_setOf, + simp only [mem_union, xt, xu, false_or, true_and, mem_ofPred, eventually_nhdsWithin_iff, ← hf] at n refine (so.eventually_mem n.1).mp (n.2.eventually_nhds.mp (.of_forall fun y n m ↦ ?_)) by_cases yt : y ∈ t - simp only [mem_union, mem_setOf, eventually_nhdsWithin_iff, ← hf]; right; use m, yt, n + simp only [mem_union, mem_ofPred, eventually_nhdsWithin_iff, ← hf]; right; use m, yt, n exact mono _ (n.self_of_nhds yt) have mem : ∀ {x u c}, x ∈ s → x ∈ t → c ∈ 𝓝[tᶜ] x → c ⊆ u → x ∈ f u := by intro x u c m xt cn cu; rw [← hf]; right; use m, xt - simp only [Filter.eventually_iff, setOf_mem_eq]; exact Filter.mem_of_superset cn cu + simp only [Filter.eventually_iff, ofPred_mem_eq]; exact Filter.mem_of_superset cn cu have cover : s ⊆ f u ∪ f v := by intro x m - by_cases xt : x ∉ t; exact union_subset_union (mono _) (mono _) (suv (mem_diff_of_mem m xt)) + by_cases xt : x ∉ t; exact union_subset_union (mono _) (mono _) (suv (mem_sdiff_of_mem m xt)) simp only [not_not] at xt rcases ts.loc x s xt (so.mem_nhds m) with ⟨c, cst, cn, cp⟩ have d := inter_subset_inter_left (u ∩ v) cst; rw [duv, subset_empty_iff] at d @@ -152,11 +152,11 @@ theorem IsPreconnected.open_diff {s t : Set X} (sc : IsPreconnected s) (so : IsO exact subset_union_left (mem m xt cn cu) exact subset_union_right (mem m xt cn cv) have fdiff : ∀ {u}, f u \ t ⊆ u := by - intro u x m; simp only [mem_diff, mem_union, mem_setOf, ← hf] at m + intro u x m; simp only [mem_sdiff, mem_union, mem_ofPred, ← hf] at m simp only [m.2, false_and, and_false, or_false, not_false_iff, and_true] at m exact m have fnon : ∀ {x u}, IsOpen u → x ∈ f u → ∀ᶠ y in 𝓝[tᶜ] x, y ∈ u := by - intro x u o m; simp only [mem_union, mem_setOf, ← hf] at m + intro x u o m; simp only [mem_union, mem_ofPred, ← hf] at m cases' m with xu m; exact (o.eventually_mem xu).filter_mono nhdsWithin_le_nhds; exact m.2.2 have disj : s ∩ (f u ∩ f v) = ∅ := by contrapose duv; simp only [← ne_eq, ← nonempty_iff_ne_empty] at duv ⊢ @@ -166,11 +166,11 @@ theorem IsPreconnected.open_diff {s t : Set X} (sc : IsPreconnected s) (so : IsO simp only [eventually_nhdsWithin_iff] at b rcases eventually_nhds_iff.mp b with ⟨n, h, no, xn⟩ rcases ts.dense.exists_mem_open no ⟨_, xn⟩ with ⟨y, yt, yn⟩ - use y; simp only [mem_inter_iff, mem_diff, ← mem_compl_iff]; specialize h y yn yt + use y; simp only [mem_inter_iff, mem_sdiff, ← mem_compl_iff]; specialize h y yn yt exact ⟨⟨h.1,yt⟩,h.2.1,h.2.2⟩ cases' sc (f u) (f v) (fopen uo) (fopen vo) cover disj with su sv - left; exact _root_.trans (diff_subset_diff_left su) fdiff - right; exact _root_.trans (diff_subset_diff_left sv) fdiff + left; exact _root_.trans (sdiff_subset_sdiff_left su) fdiff + right; exact _root_.trans (sdiff_subset_sdiff_left sv) fdiff /-- ∅ is nonseparating -/ theorem Nonseparating.empty : Nonseparating (∅ : Set X) := @@ -179,13 +179,13 @@ theorem Nonseparating.empty : Nonseparating (∅ : Set X) := /-- Punctured complex balls are preconnected -/ theorem IsPreconnected.ball_diff_center {a : ℂ} {r : ℝ} : IsPreconnected (ball a r \ {a}) := by - by_cases rp : r ≤ 0; simp only [Metric.ball_eq_empty.mpr rp, empty_diff] + by_cases rp : r ≤ 0; simp only [Metric.ball_eq_empty.mpr rp, empty_sdiff] exact isPreconnected_empty simp only [not_le] at rp have e : ball a r \ {a} = (fun p : ℝ × ℝ ↦ a + p.1 * Complex.exp (p.2 * Complex.I)) '' Ioo 0 r ×ˢ univ := by apply Set.ext; intro z - simp only [mem_diff, mem_ball, Complex.dist_eq, mem_singleton_iff, mem_image, Prod.exists, + simp only [mem_sdiff, mem_ball, Complex.dist_eq, mem_singleton_iff, mem_image, Prod.exists, mem_prod_eq, mem_Ioo, mem_univ, and_true] constructor · intro ⟨zr, za⟩ @@ -217,8 +217,8 @@ theorem Complex.nonseparating_singleton (a : ℂ) : Nonseparating ({a} : Set ℂ loc := by intro z u m n; simp only [mem_singleton_iff] at m; simp only [m] at n ⊢; clear m z rcases Metric.mem_nhds_iff.mp n with ⟨r, rp, rs⟩ - use ball a r \ {a}; refine ⟨diff_subset_diff_left rs, ?_, IsPreconnected.ball_diff_center⟩ - exact diff_mem_nhdsWithin_compl (Metric.ball_mem_nhds _ rp) _ } + use ball a r \ {a}; refine ⟨sdiff_subset_sdiff_left rs, ?_, IsPreconnected.ball_diff_center⟩ + exact sdiff_mem_nhdsWithin_compl (Metric.ball_mem_nhds _ rp) _ } /-- `{z}ᶜ` is nonseparating in 1D complex manifolds -/ theorem AnalyticManifold.nonseparating_singleton (a : S) : Nonseparating ({a} : Set S) := by @@ -244,5 +244,5 @@ theorem IsPreconnected.open_diff_line {s : Set (ℂ × S)} (sc : IsPreconnected apply IsPreconnected.open_diff sc so have e : {p : ℂ × S | p.2 = a} = univ ×ˢ {a} := by apply Set.ext; intro ⟨c, z⟩ - simp only [mem_prod_eq, mem_setOf, mem_univ, true_and, mem_singleton_iff] + simp only [mem_prod_eq, mem_ofPred, mem_univ, true_and, mem_singleton_iff] rw [e]; exact Nonseparating.univ_prod (AnalyticManifold.nonseparating_singleton _) diff --git a/Ray/Manifold/Nontrivial.lean b/Ray/Manifold/Nontrivial.lean index 86c281b..21713d7 100644 --- a/Ray/Manifold/Nontrivial.lean +++ b/Ray/Manifold/Nontrivial.lean @@ -134,24 +134,25 @@ theorem allRootsOfUnity.ne_zero {z : ℂ} (m : z ∈ allRootsOfUnity) : z ≠ 0 /-- Roots of unity are totally disconnected -/ theorem IsTotallyDisconnected.allRootsOfUnity : IsTotallyDisconnected allRootsOfUnity := by apply IsCountable.isTotallyDisconnected - simp only [_root_.allRootsOfUnity, setOf_exists]; apply countable_iUnion; intro n + simp only [_root_.allRootsOfUnity, ofPred_exists]; apply countable_iUnion; intro n by_cases n0 : n = 0 - simp only [n0, Ne, not_true, false_and, setOf_false, countable_empty] + simp only [n0, Ne, not_true, false_and, ofPred_false, countable_empty] simp only [Ne, n0, not_false_iff, true_and] have np : 0 < n := Nat.pos_of_ne_zero n0 generalize hn' : (⟨n, np⟩ : ℕ+) = n' have e : {z : ℂ | z ^ n = 1} ⊆ (fun x : ℂˣ ↦ (x : ℂ)) '' (rootsOfUnity n' ℂ : Set ℂˣ) := by - intro z e; simp only [mem_setOf] at e + intro z e; simp only [mem_ofPred] at e simp only [mem_image, SetLike.mem_coe] by_cases z0 : z = 0 · simp only [z0, zero_pow n0, zero_ne_one] at e · use Units.mk0 z z0 simp [← hn', ← Units.val_inj, Units.val_pow_eq_pow_val, Units.val_mk0, e, Units.val_one, and_self] - apply Set.Countable.mono e; clear e; apply Countable.image; apply Set.Finite.countable - rw [Set.finite_def] - refine ⟨@_root_.rootsOfUnity.fintype ℂ _ ?_ _ _⟩ - simpa only [neZero_iff, ← hn', ne_eq] + apply Set.Countable.mono e; clear e; apply Countable.image + have : NeZero (n' : ℕ) := ⟨n'.2.ne'⟩ + have h : (rootsOfUnity (n' : ℕ) ℂ : Set ℂˣ).Finite := + Set.finite_coe_iff.mp (inferInstanceAs (Finite (rootsOfUnity (n' : ℕ) ℂ))) + exact h.countable /-- Given continuous `p : X → ℂ` on preconnected `X`, `p` is const if `f ∘ p` is const -/ theorem NontrivialAnalyticOn.const (n : NontrivialAnalyticOn f s) {p : X → ℂ} {t : Set X} @@ -213,7 +214,7 @@ public theorem ContMDiffAt.eventually_eq_or_eventually_ne [T2Space T] {f g : S apply (gc.eventually_mem (extChartAt_source_mem_nhds (I := I) (g z))).mp refine eventually_nhds_iff.mpr ⟨(_root_.extChartAt I z).source, fun x m gm fm ↦ ?_, isOpen_extChartAt_source _, mem_extChartAt_source z⟩ - simp only at fm gm; rw [← fg] at gm + rw [← fg] at gm simp only [← fg, PartialEquiv.left_inv _ m, PartialEquiv.left_inv _ fm, PartialEquiv.left_inv _ gm] · right; clear fa ga @@ -237,7 +238,7 @@ public theorem ContMDiffOn.const_of_locally_const [T2Space T] {f : S → T} {s : refine p.subset_of_closure_inter_subset ?_ ?_ ?_ · rw [isOpen_iff_eventually] intro z m - simp only [Set.mem_setOf_eq, ← ht] at m ⊢ + simp only [Set.mem_ofPred_eq, ← ht] at m ⊢ exact ((o.eventually_mem m.1).and m.2.eventually_nhds).mp (.of_forall fun y h ↦ h) · use z; simp only [Set.mem_inter_iff, ← ht]; exact ⟨zs, zs, c⟩ · intro z m; simp only [Set.mem_inter_iff, mem_closure_iff_frequently] at m @@ -445,7 +446,7 @@ public theorem ContMDiffOnNhd.eq_of_locally_eq [CompleteSpace F] {f g : M → N} apply ((isOpen_extChartAt_target x).eventually_mem (mem_extChartAt_target x)).mp refine .of_forall fun y m e ↦ ?_; simp only [← ht] at e apply ((continuousAt_extChartAt_symm'' m).eventually e).mp - refine .of_forall fun z e ↦ ?_; simp only at e + refine .of_forall fun z e ↦ ?_ simp only [← hd, Pi.zero_apply, sub_eq_zero, ex, e] have da : AnalyticAt ℂ d z := by rw [← hd, ← hz] diff --git a/Ray/Manifold/OneDimension.lean b/Ray/Manifold/OneDimension.lean index 9664266..bbefe78 100644 --- a/Ray/Manifold/OneDimension.lean +++ b/Ray/Manifold/OneDimension.lean @@ -35,64 +35,71 @@ variable {T : Type} [TopologicalSpace T] [ct : ChartedSpace ℂ T] variable {U : Type} [TopologicalSpace U] [cu : ChartedSpace ℂ U] /-- 1D tangent spaces are nontrivial -/ -instance one_dimension_tangentSpace_nontrivial (z : S) : Nontrivial (TangentSpace I z) := by - simp only [TangentSpace]; infer_instance +instance one_dimension_tangentSpace_nontrivial (z : S) : Nontrivial (TangentSpace I z) := + inferInstanceAs (Nontrivial ℂ) /-- 1D tangent spaces are `NormedAddCommGroup`s -/ instance oneDimensionTangentSpaceNormedAddCommGroup (z : S) : - NormedAddCommGroup (TangentSpace I z) := by - simp only [TangentSpace]; infer_instance + NormedAddCommGroup (TangentSpace I z) := + inferInstanceAs (NormedAddCommGroup ℂ) /-- 1D tangent spaces are `NormedSpace`s -/ -instance oneDimensionTangentSpaceNormedSpace (z : S) : NormedSpace ℂ (TangentSpace I z) := by - simp only [TangentSpace]; infer_instance +instance oneDimensionTangentSpaceNormedSpace (z : S) : NormedSpace ℂ (TangentSpace I z) := + inferInstanceAs (NormedSpace ℂ ℂ) /-- The tangent space norm is `abs`, if we unpack types -/ theorem tangentSpace_norm_eq_complex_norm (z : S) (x : TangentSpace I z) : ‖x‖ = Complex.instNorm.norm x := rfl +/-- Explicitly identify a 1D tangent space with `ℂ`. + `TangentSpace` is no longer reducible, so we use this to make instance resolution + see `ℂ` while remaining definitionally the identity. -/ +@[expose] public def tangentToC {z : S} (x : TangentSpace I z) : ℂ := x + +/-- Explicitly identify `ℂ` with a 1D tangent space (definitionally the identity) -/ +@[expose] public def tangentOfC {z : S} (x : ℂ) : TangentSpace I z := x + /-- 1D tangent space maps are (noncanonically!) equivalent to `ℂ` (linear equivalence) -/ def mderivToScalar' (z : S) (w : T) : (TangentSpace I z →L[ℂ] TangentSpace I w) ≃ₗ[ℂ] ℂ where - toFun := by intro x; have y : ℂ →L[ℂ] ℂ := x; exact y 1 - invFun := by intro x; have y : ℂ →L[ℂ] ℂ := x • ContinuousLinearMap.id ℂ ℂ; exact y - map_add' x y := ContinuousLinearMap.add_apply _ _ _ - map_smul' s x := by - simp only [RingHom.id_apply, smul_eq_mul] - exact Eq.trans (ContinuousLinearMap.smul_apply _ _ _) (smul_eq_mul _ _) + toFun x := tangentToC (x (tangentOfC 1)) + invFun x := x • ContinuousLinearMap.id ℂ ℂ + map_add' x y := rfl + map_smul' s x := rfl left_inv := by - intro x; simp only; apply ContinuousLinearMap.ext; intro s - simp only [ContinuousLinearMap.smul_apply, ContinuousLinearMap.id_apply, smul_eq_mul, mul_comm] - exact Eq.trans (smul_eq_mul _ _).symm (Eq.trans (ContinuousLinearMap.map_smul _ _ _).symm - (congr_arg _ (mul_one _))) - right_inv := by intro x - simp only [ContinuousLinearMap.smul_apply, ContinuousLinearMap.id_apply, smul_eq_mul, mul_one] + apply ContinuousLinearMap.ext; intro s + show tangentToC (z := w) (x (tangentOfC (z := z) 1)) * tangentToC (z := z) s + = tangentToC (z := w) (x s) + have h := x.map_smul (tangentToC (z := z) s) (tangentOfC (z := z) 1) + have e1 : tangentToC (z := z) s • tangentOfC (z := z) 1 = s := by + show tangentToC (z := z) s * 1 = tangentToC (z := z) s + exact mul_one _ + rw [e1] at h + rw [h] + show tangentToC (z := w) (x (tangentOfC (z := z) 1)) * tangentToC (z := z) s + = tangentToC (z := z) s * tangentToC (z := w) (x (tangentOfC (z := z) 1)) + exact mul_comm _ _ + right_inv := fun x ↦ mul_one x /-- 1D tangent space maps are (noncanonically!) equivalent to `ℂ` (continuous linear equivalence) -/ def mderivToScalar (z : S) (w : T) : (TangentSpace I z →L[ℂ] TangentSpace I w) ≃L[ℂ] ℂ where toLinearEquiv := mderivToScalar' z w continuous_toFun := by - simp only [mderivToScalar'] + show Continuous fun f : ℂ →L[ℂ] ℂ ↦ f 1 rw [Metric.continuous_iff]; intro x e ep; use e / 2, half_pos ep; intro y xy simp only [dist_eq_norm] at xy ⊢ - have b := ContinuousLinearMap.le_of_opNorm_le _ xy.le (1 : ℂ) - simp only [tangentSpace_norm_eq_complex_norm, norm_one, mul_one] at b ⊢ + have b := ContinuousLinearMap.le_of_opNorm_le (y - x) xy.le (1 : ℂ) + simp only [_root_.sub_apply, norm_one, mul_one] at b ⊢ exact lt_of_le_of_lt b (half_lt_self ep) continuous_invFun := by - simp only [mderivToScalar'] + show Continuous fun x : ℂ ↦ (x • ContinuousLinearMap.id ℂ ℂ : ℂ →L[ℂ] ℂ) rw [Metric.continuous_iff]; intro x e ep; use e / 2, half_pos ep; intro y xy simp only [dist_eq_norm] at xy ⊢ - refine lt_of_le_of_lt ?_ (half_lt_self ep) - apply ContinuousLinearMap.opNorm_le_bound' _ (half_pos ep).le; intro s _ - -- Something's wrong with the type at this point, so rewrite it to make things go through - have h : ‖(y • ContinuousLinearMap.id ℂ ℂ - x • ContinuousLinearMap.id ℂ ℂ) s‖ ≤ - e/2 * ‖s‖ := by - rw [ContinuousLinearMap.sub_apply, ContinuousLinearMap.smul_apply, - ContinuousLinearMap.smul_apply] - simp only [ContinuousLinearMap.id_apply, smul_eq_mul, ← mul_sub_right_distrib, norm_mul, - tangentSpace_norm_eq_complex_norm] at xy ⊢ - bound - exact h + refine lt_of_le_of_lt (ContinuousLinearMap.opNorm_le_bound _ (half_pos ep).le fun s ↦ ?_) + (half_lt_self ep) + show ‖y * s - x * s‖ ≤ e / 2 * ‖s‖ + rw [← sub_mul, norm_mul] + exact mul_le_mul_of_nonneg_right xy.le (norm_nonneg _) /-- Given nonzero `u`, a tangent space map `x` is `0` iff `x u = 0` -/ theorem mderiv_eq_zero_iff {z : S} {w : T} (f : TangentSpace I z →L[ℂ] TangentSpace I w) @@ -100,14 +107,15 @@ theorem mderiv_eq_zero_iff {z : S} {w : T} (f : TangentSpace I z →L[ℂ] Tange constructor · rw [or_iff_not_imp_right]; intro f0 u0 apply ContinuousLinearMap.ext; intro v - simp only [TangentSpace] at f u v u0 - have e : v = (v * u⁻¹) • u := by simp only [smul_eq_mul, mul_assoc, inv_mul_cancel₀ u0, mul_one] - rw [ContinuousLinearMap.zero_apply, e] - refine Eq.trans (f.map_smul _ _) ?_ - rw [smul_eq_zero]; right; exact f0 + show f v = 0 + have u0' : tangentToC u ≠ 0 := u0 + have e : v = (tangentToC v * (tangentToC u)⁻¹) • u := by + show tangentToC v = tangentToC v * (tangentToC u)⁻¹ * tangentToC u + rw [mul_assoc, inv_mul_cancel₀ u0', mul_one] + rw [e, f.map_smul, f0, smul_zero] · intro h; cases' h with h h - simp only [h, ContinuousLinearMap.zero_apply] - simp only [h, ContinuousLinearMap.map_zero] + · rw [h]; rfl + · rw [h]; exact f.map_zero /-- Given nonzero `u`, a tangent space map `x` is `0` iff `x u = 0` -/ theorem mderiv_eq_zero_iff' {z : S} {w : T} {f : TangentSpace I z →L[ℂ] TangentSpace I w} @@ -146,7 +154,8 @@ public theorem mderiv_comp_ne_zero {x : S} {y : T} {z : U} theorem has_mfderiv_at_of_mderiv_ne_zero {f : S → T} {x : S} (d0 : mfderiv I I f x ≠ 0) : MDifferentiableAt I I f x := by contrapose d0 - simp only [mfderiv, d0, if_false] + simp only [mfderiv, d0] + exact if_neg fun h ↦ h /-- If two functions have nonzero derivative, their composition has nonzero derivative -/ public theorem mderiv_comp_ne_zero' {f : T → U} {g : S → T} {x : S} : @@ -162,33 +171,55 @@ public theorem mderiv_comp_ne_zero' {f : T → U} {g : S → T} {x : S} : toFun := f map_add' := f.map_add' map_smul' := f.map_smul' - invFun := by - intro x - have f' : ℂ →L[ℂ] ℂ := f - unfold TangentSpace at f x - exact (f' 1)⁻¹ * x + invFun x := tangentOfC ((tangentToC (f (tangentOfC 1)))⁻¹ * tangentToC x) left_inv := by - generalize hu : (1:ℂ) = u - have u0 : u ≠ 0 := by rw [←hu]; norm_num - have h := mderiv_ne_zero_iff' (f := f) (u := (u : TangentSpace I z)) u0 - intro x; simp only [TangentSpace] at f x ⊢ - have e : f x = (f u) * x := by - rw [mul_comm, ← smul_eq_mul, ← f.map_smul, smul_eq_mul, ←hu, mul_one] - simp only [e, ← mul_assoc] - rw [inv_mul_cancel₀, one_mul] - exact h.mpr f0 + intro x + have u0 : tangentOfC (z := z) 1 ≠ 0 := by + show (1 : ℂ) ≠ 0 + exact one_ne_zero + have fu0 : tangentToC (f (tangentOfC 1)) ≠ 0 := (mderiv_ne_zero_iff' u0).mpr f0 + have e : ∀ y : TangentSpace I z, + tangentToC (f y) = tangentToC (f (tangentOfC 1)) * tangentToC y := by + intro y + have h := f.map_smul (tangentToC y) (tangentOfC (z := z) 1) + have e1 : tangentToC y • tangentOfC (z := z) 1 = y := by + show tangentToC y * 1 = tangentToC y + exact mul_one _ + rw [e1] at h + rw [h] + show tangentToC y * tangentToC (f (tangentOfC 1)) + = tangentToC (f (tangentOfC 1)) * tangentToC y + exact mul_comm _ _ + show (tangentToC (f (tangentOfC 1)))⁻¹ * tangentToC (f x) = tangentToC x + rw [e x, ← mul_assoc, inv_mul_cancel₀ fu0, one_mul] right_inv := by - generalize hu : (1:ℂ) = u - have u0 : u ≠ 0 := by rw [←hu]; norm_num - have h := mderiv_ne_zero_iff' (f := f) (u := (u : TangentSpace I z)) u0 - intro x; simp only [TangentSpace] at f x ⊢ - have e : ∀ y : ℂ, f y = (f u) * y := by - intro y; rw [mul_comm, ← smul_eq_mul, ← f.map_smul, smul_eq_mul, ←hu, mul_one] - rw [e ((f u)⁻¹ * x), ← mul_assoc, mul_inv_cancel₀, one_mul] - exact h.mpr f0 + intro x + have u0 : tangentOfC (z := z) 1 ≠ 0 := by + show (1 : ℂ) ≠ 0 + exact one_ne_zero + have fu0 : tangentToC (f (tangentOfC 1)) ≠ 0 := (mderiv_ne_zero_iff' u0).mpr f0 + have e : ∀ y : TangentSpace I z, + tangentToC (f y) = tangentToC (f (tangentOfC 1)) * tangentToC y := by + intro y + have h := f.map_smul (tangentToC y) (tangentOfC (z := z) 1) + have e1 : tangentToC y • tangentOfC (z := z) 1 = y := by + show tangentToC y * 1 = tangentToC y + exact mul_one _ + rw [e1] at h + rw [h] + show tangentToC y * tangentToC (f (tangentOfC 1)) + = tangentToC (f (tangentOfC 1)) * tangentToC y + exact mul_comm _ _ + show tangentToC (f (tangentOfC ((tangentToC (f (tangentOfC 1)))⁻¹ * tangentToC x))) + = tangentToC x + rw [e _] + show tangentToC (f (tangentOfC 1)) * ((tangentToC (f (tangentOfC 1)))⁻¹ * tangentToC x) + = tangentToC x + rw [← mul_assoc, mul_inv_cancel₀ fu0, one_mul] continuous_toFun := f.cont continuous_invFun := by - simp only [TangentSpace] at f ⊢; exact Continuous.mul continuous_const continuous_id + show Continuous fun x : ℂ ↦ (tangentToC (f (tangentOfC 1)))⁻¹ * x + exact continuous_const.mul continuous_id public theorem mderivEquiv_apply {z : S} {w : T} {f : TangentSpace I z →L[ℂ] TangentSpace I w} (f0 : f ≠ 0) (x : TangentSpace I z) : mderivEquiv f f0 x = f x := by rfl @@ -208,7 +239,9 @@ public theorem id_mderiv_ne_zero {z : S} : mfderiv I I (fun z ↦ z) z ≠ 0 := simp only [id, PartialEquiv.right_inv _ m] simp only [e.fderiv_eq, fderiv_id, Ne, ContinuousLinearMap.ext_iff, not_forall, ContinuousLinearMap.id_apply, Function.comp_def] - use 1, one_ne_zero + refine ⟨(1 : ℂ), ?_⟩ + show ¬(1 : ℂ) = 0 + exact one_ne_zero /-- Critical points of iterations are precritical points -/ public theorem critical_iter {f : S → S} {n : ℕ} {z : S} (fa : ContMDiff I I ω f) @@ -228,22 +261,20 @@ variable [IsManifold I ω S] [IsManifold I ω T] [IsManifold I ω U] /-- Chart derivatives are nonzero -/ public theorem extChartAt_mderiv_ne_zero' {z w : S} (m : w ∈ (extChartAt I z).source) : mfderiv I I (extChartAt I z) w ≠ 0 := by - rcases exists_ne (0 : TangentSpace I z) with ⟨t, t0⟩ + rcases exists_ne (0 : TangentSpace I w) with ⟨t, t0⟩ rw [← mderiv_ne_zero_iff' t0]; contrapose t0 have h := ContinuousLinearMap.ext_iff.mp (extChartAt_mderiv_left_inverse m) t - simp only [ContinuousLinearMap.comp_apply] at h - rw [←h.trans (ContinuousLinearMap.id_apply _), ContinuousLinearMap.apply_eq_zero_of_eq_zero] - exact t0 + simp only [ContinuousLinearMap.comp_apply, t0, map_zero, ContinuousLinearMap.id_apply] at h + exact h.symm /-- Chart derivatives are nonzero -/ public theorem extChartAt_symm_mderiv_ne_zero' {z : S} {w : ℂ} (m : w ∈ (extChartAt I z).target) : mfderiv I I (extChartAt I z).symm w ≠ 0 := by - rcases exists_ne (0 : TangentSpace I (extChartAt I z z)) with ⟨t, t0⟩ + rcases exists_ne (0 : TangentSpace I w) with ⟨t, t0⟩ rw [← mderiv_ne_zero_iff' t0]; contrapose t0 have h := ContinuousLinearMap.ext_iff.mp (extChartAt_mderiv_right_inverse m) t - simp only [ContinuousLinearMap.comp_apply] at h - rw [←h.trans (ContinuousLinearMap.id_apply _), ContinuousLinearMap.apply_eq_zero_of_eq_zero] - exact t0 + simp only [ContinuousLinearMap.comp_apply, t0, map_zero, ContinuousLinearMap.id_apply] at h + exact h.symm /-- Chart derivatives are nonzero -/ public theorem extChartAt_mderiv_ne_zero (z : S) : mfderiv I I (extChartAt I z) z ≠ 0 := @@ -260,8 +291,8 @@ public theorem mfderiv_eq_zero_iff_deriv_eq_zero {f : ℂ → ℂ} {z : ℂ} : by_cases d : DifferentiableAt ℂ f z · constructor · have h := d.mdifferentiableAt.hasMFDerivAt; intro e; rw [e] at h - have p := h.hasFDerivAt.hasDerivAt - simp only at p; exact p.deriv + have p : HasFDerivAt f (0 : ℂ →L[ℂ] ℂ) z := hasMFDerivAt_iff_hasFDerivAt.mp h + simpa using p.hasDerivAt.deriv · have h := d.hasDerivAt intro e rw [e] at h @@ -373,7 +404,7 @@ public theorem isOpen_noncritical {f : ℂ → S → T} (fa : ContMDiff II I ω public theorem isClosed_critical {f : ℂ → S → T} (fa : ContMDiff II I ω (uncurry f)) : IsClosed {p : ℂ × S | Critical (f p.1) p.2} := by have c := (isOpen_noncritical fa).isClosed_compl - simp only [compl_setOf, not_not] at c; exact c + simp only [compl_ofPred, not_not] at c; exact c /-- Osgood's theorem on 2D product manifolds: separate analyticity + continuity implies joint analyticity. I'm not sure if a Hartogs' analogue is possible, diff --git a/Ray/Manifold/OpenMapping.lean b/Ray/Manifold/OpenMapping.lean index 756f533..8dbf6e6 100644 --- a/Ray/Manifold/OpenMapping.lean +++ b/Ray/Manifold/OpenMapping.lean @@ -78,7 +78,7 @@ theorem AnalyticOnNhd.ball_subset_image_closedBall_param {f : ℂ → ℂ → (fun p : ℂ × ℂ ↦ (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r ∈ 𝓝 (c, f c z) := by have fn : ∀ d, d ∈ u → ∃ᶠ w in 𝓝 z, f d w ≠ f d z := by refine fun d m ↦ (nontrivial_local_of_global (fa.along_snd.mono ?_) rp ep (ef d m)).nonconst - simp only [mem_prod_eq, setOf_mem_eq, (iff_true _).mpr m, true_and, subset_refl] + simp only [mem_prod_eq, ofPred_mem_eq, (iff_true _).mpr m, true_and, subset_refl] have op : ∀ d, d ∈ u → ball (f d z) (e / 2) ⊆ f d '' closedBall z r := by intro d du; refine DiffContOnCl.ball_subset_image_closedBall ?_ rp (ef d du) (fn d du) have e : f d = uncurry f ∘ fun w ↦ (d, w) := rfl @@ -132,8 +132,8 @@ public theorem NontrivialMAnalyticAt.nhds_le_map_nhds_param' {f : ℂ → ℂ have er : ∃ r, 0 < r ∧ closedBall (c, z) r ⊆ s ∧ f c z ∉ f c '' sphere z r := by have h := n.eventually_ne; contrapose h simp only [not_exists, not_not, not_and, not_exists] at h - simp only [_root_.not_imp, not_not, Filter.eventually_iff, Metric.mem_nhds_iff, not_exists, - not_subset, mem_setOf, not_and] + simp only [Classical.not_imp, not_not, Filter.eventually_iff, Metric.mem_nhds_iff, not_exists, + not_subset, mem_ofPred, not_and] intro r rp; specialize h (min (e/2) (r/2)) ?_ ?_ · bound · exact _root_.trans (Metric.closedBall_subset_ball (lt_of_le_of_lt (min_le_left _ _) @@ -169,7 +169,7 @@ public theorem NontrivialMAnalyticAt.nhds_le_map_nhds_param' {f : ℂ → ℂ Function.uncurry, and_imp] at ft simp only [mem_ball, Complex.dist_eq, lt_min_iff] at dt have a1 : ‖f d w - f c w‖ ≤ e / 4 := - (ft d w dt.2.le (le_of_eq wr) c w (norm_sub_self_lt rp).le (le_of_eq wr) dt.1 + (ft d w dt.2.le (le_of_eq (mem_sphere_iff_norm.mp wr)) c w (norm_sub_self_lt rp).le (le_of_eq (mem_sphere_iff_norm.mp wr)) dt.1 (norm_sub_self_lt tp)).le have a2 : ‖f c z - f d z‖ ≤ e / 4 := by refine (ft c z (norm_sub_self_lt rp).le (norm_sub_self_lt rp).le d z @@ -200,7 +200,6 @@ theorem NontrivialMAnalyticAt.inCharts {f : S → T} {z : S} (n : NontrivialMAna apply ((isOpen_extChartAt_source z).eventually_mem (mem_extChartAt_source (I := I) z)).mp apply (n.mAnalyticAt.continuousAt.eventually_mem (extChartAt_source_mem_nhds (I := I) (f z))).mp refine .of_forall fun w fm m fn ↦ ?_ - simp only at fm m fn rw [PartialEquiv.left_inv _ m, PartialEquiv.left_inv _ (mem_extChartAt_source z)] at fn exact ((PartialEquiv.injOn _).eq_iff fm (mem_extChartAt_source _)).mp fn diff --git a/Ray/Manifold/RiemannSphere.lean b/Ray/Manifold/RiemannSphere.lean index 6146871..4f4dba3 100644 --- a/Ray/Manifold/RiemannSphere.lean +++ b/Ray/Manifold/RiemannSphere.lean @@ -213,10 +213,12 @@ public def invHomeomorph : 𝕊 ≃ₜ 𝕊 where @[simp] public lemma invEquiv_symm : invEquiv.symm = invEquiv := by simp only [Equiv.ext_iff, invEquiv, Equiv.coe_fn_symm_mk, Equiv.coe_fn_mk, forall_const] @[simp] public lemma invHomeomorph_apply (z : 𝕊) : invHomeomorph z = z⁻¹ := by - simp only [invHomeomorph, Homeomorph.homeomorph_mk_coe, invEquiv_apply] + simp only [invHomeomorph] + exact invEquiv_apply z @[simp] public lemma invHomeomorph_symm : invHomeomorph.symm = invHomeomorph := Homeomorph.ext (by - simp only [invHomeomorph, Homeomorph.homeomorph_mk_coe_symm, invEquiv_symm, - Homeomorph.homeomorph_mk_coe, forall_const]) + intro x + show invEquiv.symm x = invEquiv x + rw [invEquiv_symm]) /-- `coe : ℂ → 𝕊` as an equivalence -/ public def coePartialEquiv : PartialEquiv ℂ 𝕊 where @@ -248,7 +250,7 @@ public def invCoeOpenPartialHomeomorph : OpenPartialHomeomorph ℂ 𝕊 := @[simp] lemma invCoeOpenPartialHomeomorph_target : invCoeOpenPartialHomeomorph.target = {0}ᶜ := by ext z; simp only [invCoeOpenPartialHomeomorph, OpenPartialHomeomorph.trans_toPartialEquiv, PartialEquiv.trans_target, Homeomorph.toOpenPartialHomeomorph_target, - OpenPartialHomeomorph.coe_coe_symm, Homeomorph.toOpenPartialHomeomorph_symm_apply, + OpenPartialHomeomorph.coe_toPartialEquiv_symm, Homeomorph.toOpenPartialHomeomorph_symm_apply, invHomeomorph_symm, coeOpenPartialHomeomorph_target, preimage_compl, univ_inter, mem_compl_iff, mem_preimage, invHomeomorph_apply, mem_singleton_iff, inv_eq_inf] @[simp] public lemma coePartialEquiv_apply (z : ℂ) : coePartialEquiv z = ↑z := by rfl @@ -273,8 +275,8 @@ public instance : ChartedSpace ℂ 𝕊 where not_false_eq_true] chart_mem_atlas := by intro z; induction z using OnePoint.rec - · simp only [rec_inf, mem_setOf_eq, or_true] - · simp only [rec_coe, mem_setOf_eq, true_or] + · simp only [rec_inf, mem_ofPred_eq, or_true] + · simp only [rec_coe, mem_ofPred_eq, true_or] /-- There are just two charts on `𝕊` -/ theorem two_charts {e : OpenPartialHomeomorph 𝕊 ℂ} (m : e ∈ atlas ℂ 𝕊) : @@ -296,25 +298,31 @@ public theorem extChartAt_inf : simp only [extChartAt, invCoeOpenPartialHomeomorph, coeOpenPartialHomeomorph, invHomeomorph, OpenPartialHomeomorph.extend, chartAt_inf, OpenPartialHomeomorph.symm_toPartialEquiv, OpenPartialHomeomorph.trans_toPartialEquiv, modelWithCornersSelf_partialEquiv, - PartialEquiv.trans_refl, PartialEquiv.coe_trans_symm, OpenPartialHomeomorph.coe_coe_symm, + PartialEquiv.trans_refl, PartialEquiv.coe_trans_symm, + OpenPartialHomeomorph.coe_toPartialEquiv_symm, Homeomorph.toOpenPartialHomeomorph_symm_apply, Homeomorph.homeomorph_mk_coe_symm, - invEquiv_symm, PartialEquiv.coe_trans, Equiv.toPartialEquiv_apply] + invEquiv_symm, PartialEquiv.coe_trans, Equiv.toPartialEquiv_apply, Function.comp_apply] + show coePartialEquiv.symm (invEquiv.symm z) = coePartialEquiv.symm (invEquiv z) + rw [invEquiv_symm] · intro z simp only [extChartAt, invCoeOpenPartialHomeomorph, coeOpenPartialHomeomorph, invHomeomorph, invEquiv, OpenPartialHomeomorph.extend, chartAt_inf, OpenPartialHomeomorph.symm_toPartialEquiv, OpenPartialHomeomorph.trans_toPartialEquiv, modelWithCornersSelf_partialEquiv, PartialEquiv.trans_refl, PartialEquiv.symm_symm, - PartialEquiv.coe_trans, OpenPartialHomeomorph.coe_coe, + PartialEquiv.coe_trans, OpenPartialHomeomorph.coe_toPartialEquiv, Homeomorph.toOpenPartialHomeomorph_apply, Homeomorph.homeomorph_mk_coe, Equiv.coe_fn_mk, PartialEquiv.coe_trans_symm, Equiv.toPartialEquiv_symm_apply, Equiv.coe_fn_symm_mk] · simp only [extChartAt, invCoeOpenPartialHomeomorph, coeOpenPartialHomeomorph, invHomeomorph, OpenPartialHomeomorph.extend, chartAt_inf, OpenPartialHomeomorph.symm_toPartialEquiv, OpenPartialHomeomorph.trans_toPartialEquiv, modelWithCornersSelf_partialEquiv, PartialEquiv.trans_refl, PartialEquiv.symm_source, PartialEquiv.trans_target, - Homeomorph.toOpenPartialHomeomorph_target, OpenPartialHomeomorph.coe_coe_symm, + Homeomorph.toOpenPartialHomeomorph_target, OpenPartialHomeomorph.coe_toPartialEquiv_symm, Homeomorph.toOpenPartialHomeomorph_symm_apply, Homeomorph.homeomorph_mk_coe_symm, invEquiv_symm, PartialEquiv.trans_source, Equiv.toPartialEquiv_source, Equiv.toPartialEquiv_apply] + show univ ∩ ⇑invEquiv.symm ⁻¹' coePartialEquiv.target + = univ ∩ ⇑invEquiv ⁻¹' coePartialEquiv.target + rw [invEquiv_symm] public theorem extChartAt_inf_apply {x : 𝕊} : extChartAt I ∞ x = x⁻¹.toComplex := by simp only [extChartAt_inf, PartialEquiv.trans_apply, coePartialEquiv_symm_apply, Equiv.toPartialEquiv_apply, invEquiv_apply] @@ -525,7 +533,7 @@ public theorem mAnalyticAt_fill_inf [IsManifold I ⊤ T] {f : ℂ → T} {y : T} modelWithCornersSelf_partialEquiv, PartialEquiv.trans_refl, chartAt_inf, OpenPartialHomeomorph.symm_toPartialEquiv, PartialEquiv.symm_symm, OpenPartialHomeomorph.toFun_eq_coe, invCoeOpenPartialHomeomorph_apply, - OpenPartialHomeomorph.coe_coe_symm, invCoeOpenPartialHomeomorph_symm_apply, inv_inf, + OpenPartialHomeomorph.coe_toPartialEquiv_symm, invCoeOpenPartialHomeomorph_symm_apply, inv_inf, toComplex_zero] have e : (fun z : ℂ ↦ chartAt ℂ y (OnePoint.rec y f (↑z)⁻¹)) = fun z : ℂ ↦ extChartAt I y (if z = 0 then y else f z⁻¹) := by diff --git a/Ray/Misc/Annuli.lean b/Ray/Misc/Annuli.lean index 7bed18d..7a302fa 100644 --- a/Ray/Misc/Annuli.lean +++ b/Ray/Misc/Annuli.lean @@ -49,12 +49,12 @@ public lemma isClosed_norm_Ici {r : ℝ} : IsClosed (norm_Ici r) := by public lemma norm_Icc_eq_diff {r s : ℝ} : norm_Icc r s = closedBall 0 s \ ball 0 r := by ext z - simp only [norm_Icc, mem_preimage, mem_Icc, mem_diff, Metric.mem_closedBall, dist_zero_right, + simp only [norm_Icc, mem_preimage, mem_Icc, mem_sdiff, Metric.mem_closedBall, dist_zero_right, Metric.mem_ball, not_lt, and_comm] @[simp] public lemma norm_Ici_diff_norm_Ioi {r : ℝ} : norm_Ici r \ norm_Ioi r = sphere 0 r := by ext z - simp only [norm_Ici, norm_Ioi, mem_diff, mem_setOf_eq, not_lt, ← le_antisymm_iff, + simp only [norm_Ici, norm_Ioi, mem_sdiff, mem_ofPred_eq, not_lt, ← le_antisymm_iff, mem_sphere_iff_norm, sub_zero, eq_comm] public lemma isCompact_norm_Icc {r s : ℝ} : IsCompact (norm_Icc r s) := by @@ -64,24 +64,24 @@ public lemma isCompact_annulus_cc {c : ℂ} {r s : ℝ} : IsCompact (annulus_cc exact (isCompact_closedBall _ _).diff isOpen_ball public lemma norm_Ioi_subset_norm_Ici {r : ℝ} : norm_Ioi r ⊆ norm_Ici r := by - simp only [norm_Ioi, norm_Ici, setOf_subset_setOf]; intro _; exact le_of_lt + simp only [norm_Ioi, norm_Ici, ofPred_subset_ofPred]; intro _; exact le_of_lt public lemma norm_Icc_subset_norm_Ici {r s : ℝ} : norm_Icc r s ⊆ norm_Ici r := by - simp only [norm_Icc, norm_Ici, preimage_subset_iff, mem_Icc, mem_setOf_eq, and_imp] + simp only [norm_Icc, norm_Ici, preimage_subset_iff, mem_Icc, mem_ofPred_eq, and_imp] intro _ h _; exact h public lemma norm_Ici_mono {r s : ℝ} (rs : r ≤ s) : norm_Ici s ⊆ norm_Ici r := by - simp only [norm_Ici, setOf_subset_setOf]; intro _ h; linarith + simp only [norm_Ici, ofPred_subset_ofPred]; intro _ h; linarith @[simp] public lemma norm_Ici_eq_univ {r : ℝ} (r0 : r ≤ 0) : norm_Ici r = univ := by ext z - simp only [norm_Ici, mem_setOf_eq, mem_univ, iff_true] + simp only [norm_Ici, mem_ofPred_eq, mem_univ, iff_true] exact le_trans r0 (by bound) public lemma isPathConnected_norm_Ici {r : ℝ} : IsPathConnected (norm_Ici r) := by cases' lt_or_ge r 0 with r0 r0 · simp only [norm_Ici_eq_univ r0.le, isPathConnected_univ] - simp only [norm_Ici, ← Set.preimage_setOf_eq, Ici_def] + simp only [norm_Ici, ← Set.preimage_ofPred_eq, Ici_def] refine IsPathConnected.of_frontier ?_ continuous_norm isClosed_Ici simp only [nonempty_Iio, frontier_Ici'] convert Complex.isPathConnected_sphere (z := 0) r0 @@ -92,7 +92,7 @@ public lemma isPreconnected_norm_Ioi {r : ℝ} : IsPreconnected (norm_Ioi r) := set f : ℝᵒᵈ → Set ℂ := fun s ↦ norm_Ici (OrderDual.ofDual s) have e : norm_Ioi r = ⋃₀ (f '' Iio (OrderDual.toDual r)) := by ext z - simp only [norm_Ioi, mem_setOf_eq, norm_Ici, Iio_toDual, sUnion_image, mem_preimage, mem_Ioi, + simp only [norm_Ioi, mem_ofPred_eq, norm_Ici, Iio_toDual, sUnion_image, mem_preimage, mem_Ioi, mem_iUnion, exists_prop, OrderDual.exists, OrderDual.ofDual_toDual, f] constructor · intro rz; exact ⟨‖z‖, rz, le_refl _⟩ @@ -122,17 +122,17 @@ public lemma compl_norm_Ioi {r : ℝ} : (norm_Ioi r)ᶜ = closedBall 0 r := by @[simp] public lemma norm_Ioi_subset_norm_Ioi {r s : ℝ} (sr : s ≤ r) : norm_Ioi r ⊆ norm_Ioi s := by intro z m - simp only [mem_setOf_eq, norm_Ioi] at m ⊢ + simp only [mem_ofPred_eq, norm_Ioi] at m ⊢ order @[simp] public lemma norm_Ici_subset_norm_Ioi {r s : ℝ} (sr : s < r) : norm_Ici r ⊆ norm_Ioi s := by intro z m - simp only [norm_Ici, mem_setOf_eq, norm_Ioi] at m ⊢ + simp only [norm_Ici, mem_ofPred_eq, norm_Ioi] at m ⊢ order public lemma annulus_oc_subset_annulus_cc {c : ℂ} {r0 r1 : ℝ} : annulus_oc c r0 r1 ⊆ annulus_cc c r0 r1 := - diff_subset_diff (subset_refl _) Metric.ball_subset_closedBall + sdiff_subset_sdiff (subset_refl _) Metric.ball_subset_closedBall public lemma measurableSet_annulus_oc {c : ℂ} {r0 r1 : ℝ} : MeasurableSet (annulus_oc c r0 r1) := @@ -147,21 +147,21 @@ public lemma measurableSet_annulus_cc {c : ℂ} {r0 r1 : ℝ} : public lemma annulus_oc_subset_norm_Ioi {a r s : ℝ} (ar : a ≤ r) : annulus_oc 0 r s ⊆ norm_Ioi a := by intro z m - simp only [annulus_oc, mem_diff, Metric.mem_closedBall, dist_zero_right, not_le, norm_Ioi, - mem_setOf_eq] at m ⊢ + simp only [annulus_oc, mem_sdiff, Metric.mem_closedBall, dist_zero_right, not_le, norm_Ioi, + mem_ofPred_eq] at m ⊢ exact lt_of_le_of_lt ar m.2 public lemma annulus_cc_subset_norm_Ioi {a r s : ℝ} (ar : a < r) : annulus_cc 0 r s ⊆ norm_Ioi a := by intro z m - simp only [annulus_cc, mem_diff, Metric.mem_closedBall, dist_zero_right, Metric.mem_ball, not_lt, - norm_Ioi, mem_setOf_eq] at m ⊢ + simp only [annulus_cc, mem_sdiff, Metric.mem_closedBall, dist_zero_right, Metric.mem_ball, not_lt, + norm_Ioi, mem_ofPred_eq] at m ⊢ exact lt_of_lt_of_le ar m.2 public lemma symmDiff_annulus_oc_annulus_cc {c : ℂ} {r s : ℝ} (rs : r ≤ s) : (symmDiff (annulus_oc c r s) (annulus_cc c r s)) = sphere c r := by ext z - simp only [annulus_oc, annulus_cc, mem_symmDiff, mem_diff, Metric.mem_closedBall, dist_eq_norm, + simp only [annulus_oc, annulus_cc, mem_symmDiff, mem_sdiff, Metric.mem_closedBall, dist_eq_norm, not_le, Metric.mem_ball, not_lt, not_and, mem_sphere_iff_norm] -- `grind` used to close the goal at this point, but doesn't anymore due to a bug constructor diff --git a/Ray/Misc/Circle.lean b/Ray/Misc/Circle.lean index 3dcb3bf..c72e97e 100644 --- a/Ray/Misc/Circle.lean +++ b/Ray/Misc/Circle.lean @@ -23,36 +23,20 @@ noncomputable section variable {X : Type} [TopologicalSpace X] -instance : Neg Circle where - neg z := Circle.exp π * z +/-- `-z = Circle.exp π * z` (Mathlib now provides `Neg Circle` and `HasDistribNeg Circle`) -/ +lemma Circle.neg_def (z : Circle) : -z = Circle.exp π * z := by + apply Circle.ext + simp only [Circle.coe_neg, Circle.coe_mul, Circle.coe_exp, Complex.exp_pi_mul_I, neg_one_mul] -lemma Circle.neg_def (z : Circle) : -z = Circle.exp π * z := rfl - -instance : InvolutiveNeg Circle where - neg_neg z := by - have e : π + π = 2 * π := by ring - simp only [Circle.neg_def, ← mul_assoc, ← Circle.exp_add, mul_eq_right, e, Circle.exp_two_pi] - -instance : HasDistribNeg Circle where - neg_mul z w := by simp only [Circle.neg_def, mul_assoc] - mul_neg z w := by simp only [Circle.neg_def, ← mul_assoc, mul_comm _ (Circle.exp _)] - -@[simp] lemma Circle.neg_ne (z : Circle) : -z ≠ z := by - simp only [neg_def, ne_eq, mul_eq_right, exp_eq_one, ← mul_assoc, eq_comm (a := π), not_exists] - simp only [ne_eq, Real.pi_ne_zero, not_false_eq_true, mul_eq_right₀, - (by norm_num : (2 : ℝ) = (2 : ℤ)), ← Int.cast_one (R := ℝ), ← Int.cast_mul, Int.cast_inj] - omega - -@[simp] lemma Circle.coe_neg (z : Circle) : (-z).val = -z.val := by - simp only [neg_def, coe_mul, coe_exp, Complex.exp_pi_mul_I, neg_mul, one_mul] +@[simp] lemma Circle.neg_ne (z : Circle) : -z ≠ z := Circle.neg_ne_self z lemma Circle.arg_neg_one : arg (-1 : Circle).val = π := by - simp only [neg_def, mul_one, coe_exp, Complex.exp_pi_mul_I, Complex.arg_neg_one] + simp only [Circle.coe_neg, Circle.coe_one, Complex.arg_neg_one] @[simp] lemma Circle.mem_slitPlane (z : Circle) : z.val ∈ slitPlane ↔ z ≠ -1 := by simp only [Complex.mem_slitPlane_iff_arg, ne_eq, Circle.ext_iff, Complex.ext_norm_arg_iff, norm_zero, Complex.arg_zero, Circle.norm_coe, true_and, one_ne_zero, false_and, not_false_iff, - and_true, coe_neg, norm_neg, OneMemClass.coe_one, Complex.arg_neg_one, norm_one] + and_true, coe_neg, norm_neg, Circle.coe_one, Complex.arg_neg_one, norm_one] @[fun_prop] lemma Continuous.circle_exp {f : X → ℝ} (fc : Continuous f) : Continuous (fun x ↦ Circle.exp (f x)) := by fun_prop diff --git a/Ray/Misc/Cobounded.lean b/Ray/Misc/Cobounded.lean index aab1429..f286c3a 100644 --- a/Ray/Misc/Cobounded.lean +++ b/Ray/Misc/Cobounded.lean @@ -29,7 +29,7 @@ variable {𝕜 : Type} [NontriviallyNormedField 𝕜] public lemma hasBasis_cobounded_norm_lt : (cobounded X).HasBasis (fun _ ↦ True) (fun r ↦ {x | r < ‖x‖}) := by have b := Filter.hasBasis_cobounded_norm (E := X) - simp only [Filter.hasBasis_iff, setOf_subset, true_and] at b ⊢ + simp only [Filter.hasBasis_iff, ofPred_subset, true_and] at b ⊢ intro s rw [b s] constructor @@ -39,19 +39,19 @@ public lemma hasBasis_cobounded_norm_lt : public theorem tendsto_cobounded {f : α → X} {l : Filter α} : Tendsto f l (cobounded X) ↔ ∀ r, ∀ᶠ x in l, r < ‖f x‖ := by rw [hasBasis_cobounded_norm_lt.tendsto_right_iff] - simp only [true_imp_iff, mem_setOf] + simp only [true_imp_iff, mem_ofPred] /-- Characterization of `atTop → cobounded` convergence -/ theorem tendsto_atTop_cobounded {f : ℕ → X} : Tendsto f atTop (cobounded X) ↔ ∀ r, ∃ N, ∀ n, N ≤ n → r < ‖f n‖ := by - simpa only [mem_Ici, mem_setOf_eq, exists_true_left, forall_true_left, true_and] using + simpa only [mem_Ici, mem_ofPred_eq, exists_true_left, forall_true_left, true_and] using Filter.HasBasis.tendsto_iff (f := f) Filter.atTop_basis hasBasis_cobounded_norm_lt /-- `cobounded` convergence in terms of norm convergence -/ public theorem tendsto_cobounded_iff_norm_tendsto_atTop {f : Filter α} {g : α → X} : Tendsto (fun x ↦ g x) f (cobounded X) ↔ Tendsto (fun x ↦ ‖g x‖) f atTop := by rw [Filter.atTop_basis_Ioi.tendsto_right_iff] - simp only [hasBasis_cobounded_norm_lt.tendsto_right_iff, true_imp_iff, mem_setOf, mem_Ioi] + simp only [hasBasis_cobounded_norm_lt.tendsto_right_iff, true_imp_iff, mem_ofPred, mem_Ioi] /-- Characterization of `s ∈ cobounded` -/ theorem mem_cobounded_iff {s : Set X} : s ∈ cobounded X ↔ ∃ r, {x | r < ‖x‖} ⊆ s := by @@ -69,14 +69,14 @@ public theorem eventually_cobounded_iff_nhds_zero {p : 𝕜 → Prop} : · intro ⟨r,_,h⟩ refine ⟨(max r 1)⁻¹, by bound, fun x ⟨m,x0⟩ ↦ ?_⟩ refine @h x⁻¹ ?_ - simp only [Metric.mem_ball, dist_zero_right, mem_compl_iff, mem_singleton_iff, mem_setOf_eq, + simp only [Metric.mem_ball, dist_zero_right, mem_compl_iff, mem_singleton_iff, mem_ofPred_eq, norm_inv] at m x0 ⊢ rw [← lt_inv_comm₀ (by bound) (by simpa)] at m exact lt_of_le_of_lt (le_max_left _ _) m · intro ⟨i,i0,h⟩ refine ⟨i⁻¹, trivial, fun x m ↦ ?_⟩ refine inv_inv x ▸ @h x⁻¹ ?_ - simp only [mem_setOf_eq, mem_inter_iff, Metric.mem_ball, dist_zero_right, norm_inv, + simp only [mem_ofPred_eq, mem_inter_iff, Metric.mem_ball, dist_zero_right, norm_inv, mem_compl_iff, mem_singleton_iff, inv_eq_zero] at m ⊢ have x0 : x ≠ 0 := by have : 0 < ‖x‖ := lt_trans (by bound) m; simpa rw [← inv_lt_comm₀ i0 (by simpa)] @@ -92,13 +92,13 @@ public theorem tendsto_cobounded_iff_tendsto_nhds_zero {l : Filter α} by_cases rp : 0 < r · use r⁻¹; simp only [rp, inv_pos, true_and]; intro x xs; refine m ?_ simp only [mem_inter_iff, mem_ball_zero_iff, mem_compl_iff, mem_singleton_iff] at xs - simp only [← lt_inv_comm₀ (norm_pos_iff.mpr xs.2) rp, xs.1, mem_setOf_eq, norm_inv] + simp only [← lt_inv_comm₀ (norm_pos_iff.mpr xs.2) rp, xs.1, mem_ofPred_eq, norm_inv] · use 1; simp only [zero_lt_one, true_and]; intro x xs; refine m ?_ simp only [mem_inter_iff, mem_ball_zero_iff, mem_compl_iff, mem_singleton_iff] at xs - simp only [mem_setOf_eq, norm_inv]; simp only [not_lt] at rp + simp only [mem_ofPred_eq, norm_inv]; simp only [not_lt] at rp exact lt_of_le_of_lt rp (inv_pos.mpr (norm_pos_iff.mpr xs.2)) · intro h t tl; rcases h t tl with ⟨r, rp, m⟩; use r⁻¹; simp only [true_and] - intro x xs; simp only [mem_setOf_eq] at xs + intro x xs; simp only [mem_ofPred_eq] at xs have m := @m x⁻¹ ?_; · simp only [inv_inv] at m; exact m simp only [mem_inter_iff, mem_ball_zero_iff, norm_inv, mem_compl_iff, mem_singleton_iff, inv_eq_zero] diff --git a/Ray/Misc/Complex.lean b/Ray/Misc/Complex.lean index 637b290..bb18182 100644 --- a/Ray/Misc/Complex.lean +++ b/Ray/Misc/Complex.lean @@ -120,6 +120,7 @@ lemma AnalyticAt.norm {𝕜 E : Type} [RCLike 𝕜] [NormedAddCommGroup E] [Norm lemma Complex.real_hasFDerivAt {f : ℂ → ℂ} {z : ℂ} {f' : ℂ} (h : HasDerivAt f f' z) : HasFDerivAt f (lsmul ℝ ℂ f') z := by convert h.hasFDerivAt.restrictScalars ℝ + all_goals try rfl ext exact mul_comm _ _ @@ -139,6 +140,7 @@ lemma hasFDerivAt_arg {z : ℂ} (m : z ∈ slitPlane) : public lemma HasDerivAt.arg {p : ℝ → ℂ} {p' : ℂ} {t : ℝ} (h : HasDerivAt p p' t) (m : p t ∈ slitPlane) : HasDerivAt (fun t ↦ arg (p t)) ((p t)⁻¹ * p').im t := by convert ((hasFDerivAt_arg m).comp t h.hasFDerivAt).hasDerivAt + all_goals try rfl simp /-! diff --git a/Ray/Misc/Connected.lean b/Ray/Misc/Connected.lean index 0cdf28a..389b28b 100644 --- a/Ray/Misc/Connected.lean +++ b/Ray/Misc/Connected.lean @@ -35,10 +35,10 @@ theorem closure_inter_subset_compl {s u v : Set X} (vo : IsOpen v) (d : Disjoint theorem isClosed_closed_inter {s u v : Set X} (sc : IsClosed s) (vo : IsOpen v) (d : Disjoint u v) (suv : s ⊆ u ∪ v) : IsClosed (s ∩ u) := by - rw [←closure_subset_iff_isClosed, ←diff_eq_empty] + rw [←closure_subset_iff_isClosed, ←sdiff_eq_empty] by_contra h simp only [← ne_eq, ← nonempty_iff_ne_empty] at h - rcases h with ⟨x, h⟩; simp only [mem_diff, mem_inter_iff, not_and] at h + rcases h with ⟨x, h⟩; simp only [mem_sdiff, mem_inter_iff, not_and] at h have sus : closure (s ∩ u) ⊆ s := by nth_rw 2 [← sc.closure_eq]; apply closure_mono; apply inter_subset_left have xs := sus h.1 @@ -71,7 +71,7 @@ theorem isPreconnected_iff_subset_of_fully_disjoint_open [NormalSpace X] {s : Se /-- Directed intersections of preconnected compact sets are preconnected -/ public theorem IsPreconnected.directed_iInter {I : Type} {s : I → Set X} [Nonempty I] [T4Space X] - (d : Directed Superset s) (p : ∀ a, IsPreconnected (s a)) (c : ∀ a, IsCompact (s a)) : + (d : Directed (· ⊇ ·) s) (p : ∀ a, IsPreconnected (s a)) (c : ∀ a, IsCompact (s a)) : IsPreconnected (⋂ a, s a) := by contrapose p have ci : IsClosed (⋂ a, s a) := isClosed_iInter fun i ↦ (c i).isClosed @@ -81,12 +81,12 @@ public theorem IsPreconnected.directed_iInter {I : Type} {s : I → Set X} [None have e : ∃ a, s a ⊆ u ∪ v := by by_contra h; simp only [not_exists, Set.not_subset] at h suffices n : (⋂ a, s a \ (u ∪ v)).Nonempty by - rcases n with ⟨x, n⟩; simp only [mem_iInter, mem_diff, forall_and, forall_const] at n + rcases n with ⟨x, n⟩; simp only [mem_iInter, mem_sdiff, forall_and, forall_const] at n rw [← mem_iInter] at n; simp only [suv n.1, not_true] at n; exact n.2 apply IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed intro a b; rcases d a b with ⟨c, ac, bc⟩ - use c, diff_subset_diff_left ac, diff_subset_diff_left bc - intro a; rcases h a with ⟨x, xa, xuv⟩; exact ⟨x, mem_diff_of_mem xa xuv⟩ + use c, (sdiff_subset_sdiff_left ac.le).ge, (sdiff_subset_sdiff_left bc.le).ge + intro a; rcases h a with ⟨x, xa, xuv⟩; exact ⟨x, mem_sdiff_of_mem xa xuv⟩ intro a; exact (c a).diff (uo.union vo) intro a; exact ((c a).diff (uo.union vo)).isClosed rcases e with ⟨a, auv⟩ @@ -104,15 +104,15 @@ theorem IsPreconnected.limits_atTop [CompactSpace X] [T4Space X] {P : Type} [Sem generalize hs : (fun a ↦ closure (r '' Ici a)) = s have m : Antitone s := by intro a b ab; rw [← hs]; exact closure_mono (monotone_image (Ici_subset_Ici.mpr ab)) - have d : Directed Superset s := by - intro a b; exact ⟨a ⊔ b, m le_sup_left, m le_sup_right⟩ + have d : Directed (· ⊇ ·) s := by + intro a b; exact ⟨a ⊔ b, (m le_sup_left).ge, (m le_sup_right).ge⟩ have p : ∀ a, IsPreconnected (s a) := by intro a; rw [← hs]; exact ((p _).image _ rc.continuousOn).closure have c : ∀ a, IsCompact (s a) := by intro a; rw [← hs]; exact isClosed_closure.isCompact have e : {x | MapClusterPt x atTop r} = ⋂ a, s a := by ext x - simp only [mem_setOf, mem_iInter, mapClusterPt_iff_frequently, mem_closure_iff_nhds, + simp only [mem_ofPred, mem_iInter, mapClusterPt_iff_frequently, mem_closure_iff_nhds, Set.Nonempty, @forall_comm P, ← hs] apply forall_congr'; intro t simp only [mem_inter_iff, mem_image, mem_Ici, @and_comm (_ ∈ t), exists_exists_and_eq_and, @@ -136,14 +136,15 @@ public theorem IsPreconnected.limits_Ioc [CompactSpace X] [T4Space X] {r : ℝ (rc : ContinuousOn r (Ioc a b)) : IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r} := by by_cases ab : ¬a < b · simp only [Ioc_eq_empty ab, nhdsWithin_empty, MapClusterPt, Filter.map_bot, ClusterPt.bot, - setOf_false, isPreconnected_empty] + ofPred_false, isPreconnected_empty] simp only [not_not] at ab generalize hs : (fun t : Ioc a b ↦ closure (r '' Ioc a t)) = s have n : Nonempty (Ioc a b) := ⟨b, right_mem_Ioc.mpr ab⟩ have m : Monotone s := by intro a b ab; rw [← hs]; refine closure_mono (monotone_image ?_) exact Ioc_subset_Ioc (le_refl _) (Subtype.coe_le_coe.mpr ab) - have d : Directed Superset s := fun a b ↦ ⟨min a b, m (min_le_left _ _), m (min_le_right _ _)⟩ + have d : Directed (· ⊇ ·) s := fun a b ↦ + ⟨min a b, (m (min_le_left _ _)).ge, (m (min_le_right _ _)).ge⟩ have p : ∀ t, IsPreconnected (s t) := by intro ⟨t, m⟩; rw [← hs]; refine (isPreconnected_Ioc.image _ (rc.mono ?_)).closure simp only [mem_Ioc] at m @@ -151,7 +152,7 @@ public theorem IsPreconnected.limits_Ioc [CompactSpace X] [T4Space X] {r : ℝ have c : ∀ t, IsCompact (s t) := by intro t; rw [← hs]; exact isClosed_closure.isCompact have e : {x | MapClusterPt x (𝓝[Ioc a b] a) r} = ⋂ t, s t := by apply Set.ext; intro x - simp only [mem_setOf, mem_iInter, mapClusterPt_iff_frequently, mem_closure_iff_nhds, + simp only [mem_ofPred, mem_iInter, mapClusterPt_iff_frequently, mem_closure_iff_nhds, Set.Nonempty, @forall_comm _ (Set X), ← hs] apply forall_congr'; intro u simp only [Filter.frequently_iff, @forall_comm _ (u ∈ 𝓝 x)]; apply forall_congr'; intro _ @@ -204,11 +205,11 @@ public theorem IsPathConnected.image_of_continuousOn {X Y : Type} [TopologicalSp have uc : IsPathConnected (univ : Set s) := by convert sc.preimage_coe (subset_refl _); apply Set.ext; intro x simp only [mem_univ, mem_preimage, Subtype.mem] - have e : f '' s = s.restrict f '' univ := by + have e : f '' s = s.domRestrict f '' univ := by apply Set.ext; intro y; constructor intro ⟨x, m, e⟩; use⟨x, m⟩, mem_univ _, e intro ⟨⟨x, m⟩, _, e⟩; use x, m, e - rw [e]; exact uc.image (continuousOn_iff_continuous_restrict.mp fc) + rw [e]; exact uc.image (continuousOn_iff_continuous_domRestrict.mp fc) /-- Circles are path connected -/ public theorem Complex.isPathConnected_sphere {z : ℂ} {r : ℝ} (r0 : 0 ≤ r) : @@ -254,7 +255,7 @@ public theorem IsPathConnected.of_frontier {X Y : Type} [TopologicalSpace X] [To rw [← Path.extend_extends']; apply lo; rw [t1]; unit_interval replace t1 : t < 1 := Ne.lt_of_le t1 m.2 have ft : f (p ⟨t, m⟩) ∈ frontier s := by - simp only [frontier, mem_diff, sc.closure_eq]; constructor + simp only [frontier, mem_sdiff, sc.closure_eq]; constructor · convert lo t (le_refl _) simp only [Path.extend_apply _ m] · have e : p ⟨t, m⟩ = p.extend t := by @@ -299,10 +300,10 @@ theorem IsPreconnected.subset_of_disjoint_frontier {s t : Set X} (sp : IsPreconn s ⊆ t := by have e : s = s ∩ t ∪ (s \ closure t) := by simp only [closure_eq_interior_union_frontier, ot.interior_eq, union_comm t, diff_union, - inter_union_diff, i.sdiff_eq_right] + inter_union_sdiff, i.sdiff_eq_right] have d : s ∩ (s ∩ t ∩ (s \ closure t)) = ∅ := by ext x - simp only [mem_inter_iff, mem_diff, mem_empty_iff_false, iff_false, not_and, not_not, and_imp, + simp only [mem_inter_iff, mem_sdiff, mem_empty_iff_false, iff_false, not_and, not_not, and_imp, forall_self_imp] intro _ m _ exact subset_closure m diff --git a/Ray/Misc/Deriv.lean b/Ray/Misc/Deriv.lean index a28f262..13285ce 100644 --- a/Ray/Misc/Deriv.lean +++ b/Ray/Misc/Deriv.lean @@ -22,11 +22,17 @@ public lemma hasFDeriv_zero_of_comp_right {f : F → G} {g : E → F} {y : F} {x (df : DifferentiableAt 𝕜 f y) (dg : HasFDerivAt g (0 : E →L[𝕜] F) x) (e : g x = y) : HasFDerivAt (fun x ↦ f (g x)) (0 : E →L[𝕜] G) x := by convert df.hasFDerivAt.comp_of_eq _ dg e - simp only [ContinuousLinearMap.comp_zero] + · rfl + · rw [ContinuousLinearMap.comp_zero] /-- Version of `HasDerivAt.inv` that works nicely over field towers -/ public theorem HasDerivAt.inv_tower [NormedAlgebra 𝕜 𝕝] {x : 𝕜} {c : 𝕜 → 𝕝} {c' : 𝕝} (dc : HasDerivAt c c' x) (c0 : c x ≠ 0) : HasDerivAt c⁻¹ (-c' / c x ^ 2) x := by have di := (hasFDerivAt_inv c0).restrictScalars 𝕜 have d := (di.comp x dc.hasFDerivAt).hasDerivAt - simpa [Function.comp_def, ← neg_div, ← div_eq_mul_inv] using d + simp only [Function.comp_def] at d + have e : c⁻¹ = fun x ↦ (c x)⁻¹ := rfl + rw [e] + convert d using 1 + · rfl + · simp [ContinuousLinearMap.toSpanSingleton_apply, div_eq_mul_inv, mul_neg] diff --git a/Ray/Misc/Finset.lean b/Ray/Misc/Finset.lean index 7d9c81a..23d09d5 100644 --- a/Ray/Misc/Finset.lean +++ b/Ray/Misc/Finset.lean @@ -41,22 +41,36 @@ public theorem push_pop {N : Finset ℕ} : push (pop N) = insert 0 N := by /-- `push` is monotone -/ theorem push_le_push {A B : Finset ℕ} : push A ≤ push B ↔ A ≤ B := by - simp; rw [push]; rw [push] + rw [push, push] constructor · intro AB; rw [Finset.subset_iff] at AB ⊢; intro x xA have h : x + 1 ∈ insert 0 (Finset.image (fun n : ℕ ↦ n + 1) A) := by simpa specialize AB h; simp at AB; assumption · intro AB; apply Finset.insert_subset_insert; apply Finset.image_mono; assumption +/-- `push` and sums interact nicely, `Stream'.get` version to keep terms type-correct + at low transparency -/ +public theorem push_sum_get {X : Type} [AddCommGroup X] {a : X} {g : Stream' X} {N : Finset ℕ} : + a + N.sum g.get = (push N).sum (cons a g).get := by + rw [push, Finset.sum_insert (by simp), Finset.sum_image (fun x _ y _ h ↦ by omega)] + rfl + /-- `push` and sums interact nicely -/ public theorem push_sum {X : Type} [AddCommGroup X] {a : X} {f : ℕ → X} {N : Finset ℕ} : - a + N.sum f = (push N).sum (cons a f) := by - rw [push]; simp; rfl + a + N.sum f = (push N).sum (cons a f) := + push_sum_get + +/-- `push` and products interact nicely, `Stream'.get` version to keep terms type-correct + at low transparency -/ +public theorem push_prod_get {a : H} {g : Stream' H} {N : Finset ℕ} : + a * N.prod g.get = (push N).prod (cons a g).get := by + rw [push, Finset.prod_insert (by simp), Finset.prod_image (fun x _ y _ h ↦ by omega)] + rfl /-- `push` and products interact nicely -/ public theorem push_prod {a : H} {f : ℕ → H} {N : Finset ℕ} : - a * N.prod f = (push N).prod (cons a f) := by - rw [push]; simp; rfl + a * N.prod f = (push N).prod (cons a f) := + push_prod_get /-- The range of `push` is `Finset`s containing 0 -/ theorem push_range : Set.range push = {N : Finset ℕ | 0 ∈ N} := by diff --git a/Ray/Misc/Linear.lean b/Ray/Misc/Linear.lean index 54d74ec..0d3a132 100644 --- a/Ray/Misc/Linear.lean +++ b/Ray/Misc/Linear.lean @@ -1,14 +1,9 @@ module -import Mathlib.Topology.Algebra.Module.LinearMap +import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic /-! ## Continuous linear map facts --/ -@[simp] lemma ContinuousLinearMap.smulRight_zero {M₁ : Type} [TopologicalSpace M₁] - [AddCommMonoid M₁] {M₂ : Type} [TopologicalSpace M₂] [AddCommMonoid M₂] {R : Type} {S : Type} - [Semiring R] [Semiring S] [Module R M₁] [Module R M₂] [Module R S] [Module S M₂] - [IsScalarTower R S M₂] [TopologicalSpace S] [ContinuousSMul S M₂] (c : M₁ →L[R] S) - : (c.smulRight (0 : M₂) : M₁ →L[R] M₂) = 0 := by - ext - simp only [ContinuousLinearMap.smulRight_apply, smul_zero, ContinuousLinearMap.zero_apply] +`ContinuousLinearMap.smulRight_zero` is now provided by Mathlib with an identical statement, +so this file no longer declares anything. +-/ diff --git a/Ray/Misc/Measure.lean b/Ray/Misc/Measure.lean index 290782f..c29a6da 100644 --- a/Ray/Misc/Measure.lean +++ b/Ray/Misc/Measure.lean @@ -8,7 +8,7 @@ public import Mathlib.MeasureTheory.Integral.Average public import Mathlib.MeasureTheory.Integral.IntegrableOn public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic public import Mathlib.MeasureTheory.Measure.Lebesgue.Complex -public import Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms +public import Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass import Mathlib.Data.Set.Basic import Mathlib.Data.Set.Prod import Mathlib.MeasureTheory.Group.Measure @@ -47,12 +47,12 @@ variable {μ : Measure M} theorem ae_minus_null {s t : Set M} (tz : volume t = 0) : s =ᵐ[volume] s \ t := by simp only [Filter.EventuallyEq, Pi.sdiff_apply, eq_iff_iff] have e : ∀ x, x ∉ t → (x ∈ s ↔ x ∈ s \ t) := by - intro x h; simp only [Set.mem_diff, h, not_false_iff, and_true] + intro x h; simp only [Set.mem_sdiff, h, not_false_iff, and_true] refine Filter.Eventually.mono ?_ e exact measure_eq_zero_iff_ae_notMem.mp tz /-- Removing a point isn't significant measure-wise (if there are no atoms) -/ -public theorem ae_minus_point [NoAtoms (volume : Measure M)] {s : Set M} {x : M} : +public theorem ae_minus_point [NullSingletonClass (volume : Measure M)] {s : Set M} {x : M} : s =ᵐ[volume] (s \ {x} : Set M) := ae_minus_null (measure_singleton x) @@ -88,12 +88,12 @@ public instance Complex.isAddHaarMeasure_volume : (volume : Measure ℂ).IsAddHa · rw [←e]; exact Complex.equivRealProdCLM.symm.toHomeomorph.toCocompactMap.cocompact_tendsto' /-- `ℂ` has no atoms -/ -public instance Complex.noAtoms_volume : NoAtoms (volume : Measure ℂ) where +public instance Complex.noAtoms_volume : NullSingletonClass (volume : Measure ℂ) where measure_singleton := by intro z rw [← (MeasurePreserving.symm _ Complex.volume_preserving_equiv_real_prod).measure_preimage] · rw [← MeasurableEquiv.image_eq_preimage_symm, Set.image_singleton, - MeasureTheory.NoAtoms.measure_singleton] + MeasureTheory.measure_singleton] · apply MeasurableSet.singleton /-- The property that a set has finite, positive measure. @@ -246,7 +246,7 @@ public theorem mean_squeeze {f : X → ℝ} {s : Set X} {b : ℝ} (sn : NiceVolu have tf : volume t < ⊤ := lt_of_le_of_lt (measure_mono ts) sn.finite have tm : MeasurableSet t := by rw [← ht]; exact MeasurableSet.inter sn.measurable measurableSet_ball - have sc : s \ t ∪ t = s := Set.diff_union_of_subset ts + have sc : s \ t ∪ t = s := Set.sdiff_union_of_subset ts nth_rw 2 [← sc] rw [setIntegral_union] simp only [MeasurableSet.univ, measureReal_restrict_apply, Set.univ_inter, gt_iff_lt] @@ -261,12 +261,12 @@ public theorem mean_squeeze {f : X → ℝ} {s : Set X} {b : ℝ} (sn : NiceVolu _ < (b + b) / 2 := (div_lt_div_iff_of_pos_right (by norm_num)).mpr (by bound) _ = b := by ring have i0 : ∫ x in s \ t, f x ≤ (vs - vt) * b := by - have df : volume (s \ t) < ⊤ := lt_of_le_of_lt (measure_mono Set.diff_subset) sn.finite + have df : volume (s \ t) < ⊤ := lt_of_le_of_lt (measure_mono Set.sdiff_subset) sn.finite have dm : MeasurableSet (s \ t) := MeasurableSet.diff sn.measurable tm have fb := setIntegral_mono_on (μ := volume) (f := f) (g := fun _ ↦ b) (s := s \ t) - (fi.mono Set.diff_subset (le_refl _)) (integrableOn_const df.ne_top) dm ?_ + (fi.mono Set.sdiff_subset (le_refl _)) (integrableOn_const df.ne_top) dm ?_ · simp only [integral_const, MeasurableSet.univ, measureReal_restrict_apply, Set.univ_inter, - MeasureTheory.measureReal_diff ts tm sn.ne_top, smul_eq_mul] at fb + MeasureTheory.measureReal_sdiff ts tm sn.ne_top, smul_eq_mul] at fb exact fb · intro y yd; simp at yd; exact hi y yd.left have i1 : ∫ x in t, f x ≤ vt * m := by @@ -289,7 +289,7 @@ public theorem mean_squeeze {f : X → ℝ} {s : Set X} {b : ℝ} (sn : NiceVolu _ = b * vs := by ring · rw [disjoint_comm]; exact Set.disjoint_sdiff_right · exact tm - · exact fi.mono Set.diff_subset (le_refl _) + · exact fi.mono Set.sdiff_subset (le_refl _) · exact fi.mono ts (le_refl _) public theorem ContinuousOn.intervalIntegral {M : Type} [TopologicalSpace M] diff --git a/Ray/Misc/MonotoneSeries.lean b/Ray/Misc/MonotoneSeries.lean index e272bf5..4dadeff 100644 --- a/Ray/Misc/MonotoneSeries.lean +++ b/Ray/Misc/MonotoneSeries.lean @@ -38,7 +38,8 @@ theorem NNReal.hasSum_ciSup {f : ℕ → ι → ℝ≥0} {a : ℕ → ℝ≥0} ( apply mono nm have sum' : ∀ n, HasSum (f' n) (a' n) := by intro n - simpa [Function.comp_def] using ENNReal.continuous_coe.continuousAt.tendsto.comp (sum n) + simpa [HasSum, f', a', Function.comp_def] using + ENNReal.continuous_coe.continuousAt.tendsto.comp (sum n) have bdd_f : ∀ {i}, BddAbove (range (fun n ↦ f n i)) := by refine fun {i} ↦ bound.range_mono _ fun n ↦ ?_ trans ∑ i ∈ {i}, f n i @@ -46,7 +47,7 @@ theorem NNReal.hasSum_ciSup {f : ℕ → ι → ℝ≥0} {a : ℕ → ℝ≥0} ( · exact sum_le_hasSum _ (by simp) (sum n) have h := (ENNReal.continuousAt_toNNReal ?_).tendsto.comp (ENNReal.hasSum_iSup mono') · simpa only [(sum' _).tsum_eq, HasSum, f', a', Function.comp_def, ← ENNReal.coe_iSup bdd_f, - ← ENNReal.coe_finset_sum, ENNReal.toNNReal_coe, ← ENNReal.coe_iSup bound] using h + ← ENNReal.ofNNReal_finsetSum, ENNReal.toNNReal_coe, ← ENNReal.coe_iSup bound] using h · simp [f', ENNReal.tsum_coe_eq (sum _), ENNReal.iSup_coe_eq_top.not, bound] /-- Monotone convergence theorem for series, `ℝ` `HasSum` version -/ @@ -66,7 +67,7 @@ theorem Real.hasSum_ciSup [Nonempty ι] {f : ℕ → ι → ℝ} {a : ℕ → have sum' : ∀ n, HasSum (f' n) (a' n) := fun n ↦ ((sum n).sub (sum 0)).toNNReal (by bound) have mono' : Monotone f' := by intro n m nm; simp only [Pi.le_def]; bound have bound_a' : BddAbove (range a') := - bound_a.range_comp (g := fun x ↦ (x - a 0).toNNReal) fun x y xy ↦ by bound + bound_a.range_comp_left (g := fun x ↦ (x - a 0).toNNReal) fun x y xy ↦ by bound have s := NNReal.hasSum_ciSup sum' mono' bound_a' simp [← NNReal.hasSum_coe, f', a', max_eq_left a_nonneg, max_eq_left f_nonneg, ← ciSup_sub bound_a, ← ciSup_sub (bound_f _)] at s diff --git a/Ray/Misc/Multilinear.lean b/Ray/Misc/Multilinear.lean index 7058ca7..f33c4d5 100644 --- a/Ray/Misc/Multilinear.lean +++ b/Ray/Misc/Multilinear.lean @@ -188,7 +188,6 @@ theorem smulCmmap_norm [NormedAddCommGroup A] [NormedSpace 𝕜 A] [NormedAddCom simp only [Finset.univ_unique, Fin.default_eq_zero, Finset.prod_const, Finset.card_singleton, pow_one] at xb xsb have e0 := Fin.prod_cons ‖z 0‖ fun i : Fin n ↦ ‖z i.succ‖ - simp only at e0 have e1 : ‖z 0‖ = (fun i : Fin (n + 1) ↦ ‖z i‖) 0 := rfl have e2 : (fun i : Fin n ↦ ‖z i.succ‖) = Fin.tail fun i : Fin (n + 1) ↦ ‖z i‖ := rfl nth_rw 1 [e1] at e0; nth_rw 1 [e2] at e0; rw [Fin.cons_self_tail (fun i ↦ ‖z i‖)] at e0 @@ -214,12 +213,10 @@ public theorem termCmmap_apply [NormedAddCommGroup E] [NormedSpace 𝕜 E] [SMul zero_tsub, one_smul] · rw [termCmmap, smulCmmap_apply, h] by_cases nk : n < k - · simp [nk] - rw [fstCmmap_apply] - have nsk : n.succ ≤ k := Nat.succ_le_iff.mpr nk - rw [min_eq_right nk.le, min_eq_right nsk, Nat.sub_eq_zero_of_le nk.le, - Nat.sub_eq_zero_of_le nsk] - simp only [pow_zero, one_smul, ← smul_assoc, smul_eq_mul, Nat.succ_eq_add_one, pow_succ'] + · have nsk : n.succ ≤ k := Nat.succ_le_iff.mpr nk + simp only [nk, if_true, fstCmmap_apply, min_eq_right nk.le, min_eq_right nsk, + Nat.sub_eq_zero_of_le nk.le, Nat.sub_eq_zero_of_le nsk, pow_zero, one_smul, smul_smul, + pow_succ'] · simp [nk]; simp at nk rw [sndCmmap_apply] have nsk : k ≤ n.succ := Nat.le_succ_of_le nk @@ -274,15 +271,15 @@ public lemma ContinuousLinearMap.smulRight_ne_zero {R A B : Type} [Ring R] [Topo (c0 : c ≠ 0) (f0 : f ≠ 0) : c.smulRight f ≠ 0 := by rcases ContinuousLinearMap.exists_ne_zero c0 with ⟨x,cx⟩ - simp only [Ne, ContinuousLinearMap.ext_iff, not_forall, ContinuousLinearMap.zero_apply, - ContinuousLinearMap.smulRight_apply, smul_eq_zero, not_or] - use x + simp only [Ne, ContinuousLinearMap.ext_iff, not_forall, _root_.zero_apply, + ContinuousLinearMap.smulRight_apply] + exact ⟨x, fun h ↦ (eq_zero_or_eq_zero_of_smul_eq_zero h).elim cx f0⟩ /-- `1 ≠ 0`, `ContinuousLinearMap` case -/ public lemma ContinuousLinearMap.one_ne_zero {R A : Type} [Ring R] [TopologicalSpace A] [AddCommMonoid A] [Module R A] [Nontrivial A] : (1 : A →L[R] A) ≠ 0 := by - simp only [Ne, ContinuousLinearMap.ext_iff, not_forall, ContinuousLinearMap.zero_apply, - ContinuousLinearMap.one_apply] + simp only [Ne, ContinuousLinearMap.ext_iff, not_forall, _root_.zero_apply, + _root_.one_apply_eq_self] apply exists_ne /-- `mkPiRing` is continuous -/ @@ -296,7 +293,7 @@ public lemma ContinuousMultilinearMap.continuous_mkPiRing {𝕜 ι E : Type} [No refine lt_of_le_of_lt (b := e / 2) ?_ (by bound) rw [dist_eq_norm, ContinuousMultilinearMap.opNorm_le_iff (by bound)] intro m - simp only [ContinuousMultilinearMap.sub_apply, ContinuousMultilinearMap.mkPiRing_apply, + simp only [_root_.sub_apply, ContinuousMultilinearMap.mkPiRing_apply, ← smul_sub] refine le_trans (norm_smul_le _ _) ?_ rw [mul_comm] diff --git a/Ray/Misc/Prod.lean b/Ray/Misc/Prod.lean index 5871276..938a2d7 100644 --- a/Ray/Misc/Prod.lean +++ b/Ray/Misc/Prod.lean @@ -23,9 +23,6 @@ noncomputable section variable {A B C : Type} variable {𝕜 : Type} [NontriviallyNormedField 𝕜] -/-- `flip` is an involution -/ -public theorem flip_flip (f : A → B → C) : flip (flip f) = f := rfl - /-- `swap` is an involution -/ public theorem swap_swap (s : Set (A × B)) : swap '' (swap '' s) = s := by ext x; simp only [Set.mem_image, Prod.exists]; constructor diff --git a/Ray/Misc/Set.lean b/Ray/Misc/Set.lean index 27ee3f9..43f638d 100644 --- a/Ray/Misc/Set.lean +++ b/Ray/Misc/Set.lean @@ -1,5 +1,6 @@ module public import Mathlib.Data.Set.Basic +public import Mathlib.Order.BooleanAlgebra.Set /-! ## `Set` facts @@ -9,6 +10,5 @@ open Set variable {α : Type} -public lemma Set.diff_union {s u v : Set α} : s \ (u ∪ v) = (s \ u) \ v := by - ext x - aesop +public lemma Set.diff_union {s u v : Set α} : s \ (u ∪ v) = (s \ u) \ v := + Set.sdiff_sdiff.symm diff --git a/Ray/Misc/Subexp.lean b/Ray/Misc/Subexp.lean index c146748..7c051a5 100644 --- a/Ray/Misc/Subexp.lean +++ b/Ray/Misc/Subexp.lean @@ -6,7 +6,7 @@ public import Mathlib.Analysis.Normed.Ring.Basic public import Mathlib.Topology.Algebra.InfiniteSum.Defs import Mathlib.Analysis.CStarAlgebra.Basic import Mathlib.Analysis.SpecificLimits.Normed -import Mathlib.Data.Real.Sqrt +import Mathlib.Analysis.Real.Sqrt /-! ## Sequences that grow subexponentially diff --git a/Ray/Misc/Topology.lean b/Ray/Misc/Topology.lean index 6106204..c706d30 100644 --- a/Ray/Misc/Topology.lean +++ b/Ray/Misc/Topology.lean @@ -41,18 +41,18 @@ public theorem UniformCauchySeqOn.bounded {X Y : Type} [TopologicalSpace X] [Nor · rw [← hb]; exact add_nonneg (by norm_num) (_root_.trans (cs 0).1 (Finset.le_max' _ _ c0)) · intro n x xs by_cases nN : n ≤ N - · have cn : c n ∈ bs := by simp [← hbs]; exists n; simp [Nat.lt_add_one_iff.mpr nN] + · have cn : c n ∈ bs := by simp [← hbs]; exists n exact _root_.trans ((cs n).2 x xs) (_root_.trans (Finset.le_max' _ _ cn) (by simp only [le_add_iff_nonneg_left, zero_le_one, ← hb])) · simp at nN specialize H N le_rfl n nN.le x xs - have cN : c N ∈ bs := by simp [← hbs]; exists N; simp + have cN : c N ∈ bs := by simp [← hbs]; exists N have bN := _root_.trans ((cs N).2 x xs) (Finset.le_max' _ _ cN) rw [dist_eq_norm] at H calc ‖f n x‖ = ‖f N x - (f N x - f n x)‖ := by rw [sub_sub_cancel] _ ≤ ‖f N x‖ + ‖f N x - f n x‖ := norm_sub_le _ _ _ ≤ bs.max' _ + 1 := add_le_add bN H.le - _ = 1 + bs.max' _ := by ring + _ = 1 + bs.max' ⟨_, c0⟩ := by rw [add_comm] _ = b := by simp only [hb] /-- `{b | (a,b) ∈ s}` is open if `s` is open -/ @@ -213,7 +213,7 @@ lemma eventuallyEq_inter {X : Type} [TopologicalSpace X] {s t u : Set X} {x : X} public lemma exists_ball_superset {X : Type} [MetricSpace X] [ProperSpace X] {s : Set X} {x : X} {r : ℝ} (sub : closedBall x r ⊆ s) (o : IsOpen s) : ∃ t, r < t ∧ ball x t ⊆ s := by by_cases n : closedBall x (r + 1) \ s = ∅ - · simp only [diff_eq_empty] at n + · simp only [sdiff_eq_empty] at n exact ⟨r + 1, by linarith, subset_trans Metric.ball_subset_closedBall n⟩ simp only [← nonempty_iff_ne_empty] at n have c : IsCompact (closedBall x (r + 1) \ s) := (isCompact_closedBall x (r + 1)).diff o @@ -226,7 +226,8 @@ public lemma exists_ball_superset {X : Type} [MetricSpace X] [ProperSpace X] {s simpa only [Metric.mem_closedBall, dist_comm] · intro z m by_contra zs - simp only [isMinOn_iff, mem_diff, Metric.mem_closedBall, dist_comm, and_imp, mem_ball] at h m yr + simp only [isMinOn_iff, Set.mem_sdiff, Metric.mem_closedBall, dist_comm, and_imp, + mem_ball] at h m yr specialize h z (le_trans m.le yr) zs linarith @@ -300,4 +301,4 @@ public lemma ENNReal.continuousAt_toNNReal {x : ℝ≥0∞} (h : x ≠ ⊤) : ContinuousAt (fun x ↦ x.toNNReal) x := by apply ENNReal.continuousOn_toNNReal.continuousAt apply ENNReal.isOpen_ne_top.mem_nhds - simpa only [ne_eq, Set.mem_setOf_eq] + simpa only [ne_eq, Set.mem_ofPred_eq] diff --git a/Ray/Misc/TotallyDisconnected.lean b/Ray/Misc/TotallyDisconnected.lean index e3d41b3..dff664c 100644 --- a/Ray/Misc/TotallyDisconnected.lean +++ b/Ray/Misc/TotallyDisconnected.lean @@ -71,7 +71,7 @@ public theorem Countable.totallyDisconnectedSpace {X : Type} [MetricSpace X] [Co generalize hR : {r | ∃ x y : X, dist x y = r} = R have rc : R.Countable := by have e : R = range (uncurry (dist (α := X))) := by - apply Set.ext; intro r; simp only [mem_setOf, mem_range, Prod.exists, uncurry, ← hR] + apply Set.ext; intro r; simp only [mem_ofPred, mem_range, Prod.exists, uncurry, ← hR] rw [e]; exact countable_range _ refine @TotallySeparatedSpace.totallyDisconnectedSpace _ _ ?_ rw [totallySeparatedSpace_iff_exists_isClopen] @@ -81,7 +81,7 @@ public theorem Countable.totallyDisconnectedSpace {X : Type} [MetricSpace X] [Co simp only [not_subset, mem_Ioo] at h; rcases h with ⟨r, ⟨rp, rxy⟩, rr⟩ have e : ball x r = closedBall x r := by apply Set.ext; intro z; simp only [mem_ball, mem_closedBall] - simp only [mem_setOf, not_exists, ← hR] at rr; simp only [Ne.le_iff_lt (rr z x)] + simp only [mem_ofPred, not_exists, ← hR] at rr; simp only [Ne.le_iff_lt (rr z x)] refine ⟨ball x r, ⟨?_, isOpen_ball⟩, ?_⟩ rw [e]; exact isClosed_closedBall; use mem_ball_self rp simp only [mem_compl_iff, mem_ball, dist_comm, not_lt] diff --git a/Ray/Multibrot/Area.lean b/Ray/Multibrot/Area.lean index 3c22e7d..26d6164 100644 --- a/Ray/Multibrot/Area.lean +++ b/Ray/Multibrot/Area.lean @@ -47,7 +47,7 @@ public lemma ray_eq_pray (m : z ∈ ball (0 : ℂ) 1) : ray d z = (z / pray d z /-- `ray` in terms of `pray`, `norm_Ioi` version -/ lemma ray_inv_eq_pray (m : z ∈ norm_Ioi 1) : ray d z⁻¹ = z * pray d z⁻¹ := by - simp only [norm_Ioi, mem_setOf_eq] at m + simp only [norm_Ioi, mem_ofPred_eq] at m have m' : z⁻¹ ∈ ball (0 : ℂ) 1 := by simp only [mem_ball, dist_zero_right, norm_inv]; bound rw [ray_eq_pray m', RiemannSphere.inv_coe] · simp [mul_comm] @@ -91,21 +91,21 @@ lemma multibrot_eq_pray : (multibrot d)ᶜ = (fun z ↦ z * pray d z⁻¹) '' no · exact norm_bottcher_lt_one m · simp only [norm_pos_iff, ne_eq, bottcher_coe_ne_zero, not_false_eq_true] refine ⟨(bottcher d z)⁻¹, ?_, ?_⟩ - · simp only [norm_Ioi, mem_setOf_eq, norm_inv, b1] + · simp only [norm_Ioi, mem_ofPred_eq, norm_inv, b1] · rw [← RiemannSphere.coe_eq_coe, ← ray_inv_eq_pray, inv_inv, ray_bottcher m] - simp only [norm_Ioi, mem_setOf_eq, norm_inv, b1] + simp only [norm_Ioi, mem_ofPred_eq, norm_inv, b1] · intro ⟨w,w1,wz⟩ rw [← RiemannSphere.coe_eq_coe, ← ray_inv_eq_pray w1] at wz rw [← wz] apply ray_mem_multibrotExt - simp only [norm_Ioi, mem_setOf_eq, mem_ball, dist_zero_right, norm_inv] at w1 ⊢ + simp only [norm_Ioi, mem_ofPred_eq, mem_ball, dist_zero_right, norm_inv] at w1 ⊢ exact inv_lt_one_of_one_lt₀ w1 /-- `ray` in terms of `pray` is injective -/ lemma pray_inj : InjOn (fun z ↦ z * pray d z⁻¹) (norm_Ioi 1) := by intro z z1 w w1 e simp only [← RiemannSphere.coe_eq_coe, ← ray_inv_eq_pray, z1, w1] at e - simp only [norm_Ioi, mem_setOf_eq] at z1 w1 + simp only [norm_Ioi, mem_ofPred_eq] at z1 w1 rwa [ray_inj.eq_iff, inv_inj] at e all_goals rw [mem_ball, dist_zero_right, norm_inv]; exact inv_lt_one_of_one_lt₀ (by assumption) diff --git a/Ray/Multibrot/Basic.lean b/Ray/Multibrot/Basic.lean index b9a05ca..e22b90e 100644 --- a/Ray/Multibrot/Basic.lean +++ b/Ray/Multibrot/Basic.lean @@ -132,7 +132,7 @@ public theorem superNearF (d : ℕ) [Fact (2 ≤ d)] (c : ℂ) : · exact isOpen_lt continuous_norm continuous_const · exact isOpen_lt (continuous_norm.comp (by continuity)) continuous_const t0 := by - simp only [superNearT, one_div, mem_setOf_eq, norm_zero, inv_pos, Nat.ofNat_pos, + simp only [superNearT, one_div, mem_ofPred_eq, norm_zero, inv_pos, Nat.ofNat_pos, zero_pow (d_ne_zero d), mul_zero, div_pos_iff_of_pos_left, and_self] t2 := fun {z} m ↦ le_trans (zb m).le (by norm_num) fa := by @@ -147,7 +147,7 @@ public theorem superNearF (d : ℕ) [Fact (2 ≤ d)] (c : ℂ) : intro z m specialize cz1 m specialize zb m - simp only [fl_f, mem_setOf, norm_div, norm_pow, superNearT] at m ⊢ + simp only [fl_f, mem_ofPred, norm_div, norm_pow, superNearT] at m ⊢ have le : ‖z‖ ^ d / ‖1 + c * z ^ d‖ ≤ 5 / 27 := by calc ‖z‖ ^ d / ‖1 + c * z ^ d‖ _ ≤ (1 / 3) ^ d / (3 / 5) := by bound @@ -172,7 +172,7 @@ public theorem superNearF (d : ℕ) [Fact (2 ≤ d)] (c : ℂ) : theorem critical_f {z : 𝕊} : Critical (f d c) z ↔ z = 0 ∨ z = (∞ : 𝕊) := by induction' z using OnePoint.rec with z · simp only [(superF d).critical_a, or_true] - · have zx : ∀ x : ℂ, (0 : ℂ →L[ℂ] ℂ) x = 0 := fun x ↦ ContinuousLinearMap.zero_apply _ + · have zx : ∀ x : ℂ, (0 : ℂ →L[ℂ] ℂ) x = 0 := fun x ↦ rfl simp only [Critical, mfderiv, (mAnalyticAt_f (c, z)).along_snd.mdifferentiableAt (by decide), if_pos, ModelWithCorners.Boundaryless.range_eq_univ, fderivWithin_univ, writtenInExtChartAt_coe_f, RiemannSphere.extChartAt_coe, coePartialEquiv_symm_apply, @@ -182,17 +182,30 @@ theorem critical_f {z : 𝕊} : Critical (f d c) z ↔ z = 0 ∨ z = (∞ : 𝕊 pow_eq_zero_iff, false_or] constructor · intro h - specialize h 1 - simpa only [one_ne_zero, false_or] using h - · exact fun h x ↦ Or.inr h + have h1 : (if True then ContinuousLinearMap.toSpanSingleton ℂ ((d : ℂ) * z ^ (d - 1)) + else 0 : ℂ →L[ℂ] ℂ) (1 : ℂ) = 0 := h (1 : ℂ) + rw [if_pos trivial] at h1 + have h2 : (1 : ℂ) • ((d : ℂ) * z ^ (d - 1)) = 0 := h1 + rw [one_smul, mul_eq_zero] at h2 + rcases h2 with h2 | h2 + · exact absurd (Nat.cast_eq_zero.mp h2) (d_ne_zero _) + · exact (pow_eq_zero_iff (d_minus_one_pos _).ne').mp h2 + · intro h x + have e : ∀ y : ℂ, (if True then ContinuousLinearMap.toSpanSingleton ℂ ((d : ℂ) * z ^ (d - 1)) + else 0 : ℂ →L[ℂ] ℂ) y = 0 := by + intro y + rw [if_pos trivial] + show y • ((d : ℂ) * z ^ (d - 1)) = 0 + simp only [h, zero_pow (d_minus_one_pos _).ne', mul_zero, smul_zero] + exact e x /-- The multibrot set is all `c`'s s.t. `0` doesn't reach `∞` -/ theorem multibrot_basin' : c ∈ multibrot d ↔ (c, (c : 𝕊)) ∉ (superF d).basin := by - simp only [multibrot, mem_setOf, Super.basin_iff_attracts, Attracts] + simp only [multibrot, mem_ofPred, Super.basin_iff_attracts, Attracts] theorem multibrot_basin : c ∈ multibrot d ↔ (c, (0 : 𝕊)) ∉ (superF d).basin := by set s := superF d - simp only [multibrot_basin', not_iff_not, Super.basin, mem_setOf] + simp only [multibrot_basin', not_iff_not, Super.basin, mem_ofPred] have e : ∀ n, (f d c)^[n] c = (f d c)^[n + 1] 0 := by intro n; induction' n with n h · simp only [Function.iterate_zero_apply, zero_add, Function.iterate_one, f_0] @@ -205,7 +218,7 @@ public theorem multibrot_p : (superF d).p c = (superF d).potential c 0 := by set s := superF d have e : s.ps c = {1, s.potential c 0} := by apply Set.ext; intro p - simp only [Super.ps, mem_singleton_iff, mem_setOf, critical_f, Ne, mem_insert_iff, + simp only [Super.ps, mem_singleton_iff, mem_ofPred, critical_f, Ne, mem_insert_iff, mem_singleton_iff] constructor · intro h; cases' h with h h; left; exact h; right; rcases h with ⟨p0, z, e, h⟩ @@ -281,7 +294,7 @@ public theorem f_f'_iter {d : ℕ} (n : ℕ) {z : ℂ} : (f d c)^[n] ↑z = ↑( public theorem multibrot_coe {d : ℕ} : c ∈ multibrot d ↔ ¬Tendsto (fun n ↦ (f' d c)^[n] c) atTop (cobounded ℂ) := by - simp only [multibrot, mem_setOf, f_f'_iter, tendsto_inf_iff_tendsto_cobounded] + simp only [multibrot, mem_ofPred, f_f'_iter, tendsto_inf_iff_tendsto_cobounded] /-- Closed Julia sets are not outside radius `max 2 (abs c)` -/ public theorem julia_two_lt {z : ℂ} (z2 : 2 < ‖z‖) (cz : ‖c‖ ≤ ‖z‖) : @@ -335,7 +348,7 @@ public theorem multibrot_of_repeat {d a b : ℕ} (ab : a < b) (h : (f d c)^[a] c use k + 1, Nat.succ_le_iff.mpr (Ne.lt_of_le e kb) rw [← hg, ← hg, Function.iterate_succ_apply', Function.iterate_succ_apply', hg, hg, nk] simp only [multibrot_coe, hasBasis_cobounded_norm_lt.tendsto_right_iff, true_imp_iff, not_forall, - Filter.not_eventually, mem_setOf, not_lt, hg] + Filter.not_eventually, mem_ofPred, not_lt, hg] use partialSups (fun k ↦ ‖g k‖) b refine .of_forall ?_; intro k; rcases lo k with ⟨l, lb, kl⟩ rw [kl]; exact le_partialSups_of_le (fun k ↦ ‖g k‖) lb @@ -414,7 +427,7 @@ public theorem isOpen_multibrotExt : IsOpen (multibrotExt d) := by -/ lemma mem_superNearT {c : ℂ} (lo : 3 < ‖c‖) : c⁻¹ ∈ superNearT d c := by - simp only [superNearT, one_div, mem_setOf_eq, norm_inv, inv_pow] + simp only [superNearT, one_div, mem_ofPred_eq, norm_inv, inv_pow] refine ⟨by bound, ?_⟩ calc ‖c‖ * (‖c‖ ^ d)⁻¹ _ ≤ ‖c‖ * (‖c‖ ^ 2)⁻¹ := by bound @@ -473,7 +486,7 @@ theorem bottcher_tendsto_zero : Tendsto (bottcher' d) (cobounded ℂ) (𝓝 0) : intro r rp rw [hasBasis_cobounded_norm_lt.eventually_iff] use max 3 (superK / r) - simp only [true_and, mem_setOf, Complex.dist_eq, sub_zero, max_lt_iff] + simp only [true_and, mem_ofPred, Complex.dist_eq, sub_zero, max_lt_iff] intro z ⟨lo, rz⟩; apply lt_of_le_of_lt (bottcher_bound lo) rw [div_lt_iff₀ rp] at rz rw [norm_inv, mul_inv_lt_iff₀ (lt_trans (by norm_num) lo)] @@ -493,7 +506,7 @@ public theorem bottcherMAnalytic (d : ℕ) [Fact (2 ≤ d)] : intro c m; induction c using OnePoint.rec · refine mAnalyticAt_fill_inf ?_ bottcher_tendsto_zero rw [hasBasis_cobounded_norm_lt.eventually_iff]; use 2 - simp only [true_and, mem_setOf] + simp only [true_and, mem_ofPred] intro z a; exact (bottcher_analytic _ (multibrot_two_lt a)).mAnalyticAt I I · simp only [multibrotExt_coe] at m exact mAnalyticAt_fill_coe ((bottcher_analytic (d := d) _ m).mAnalyticAt I I) @@ -534,7 +547,7 @@ public theorem potential_lt_one {c : 𝕊} : potential d c < 1 ↔ c ∈ multibr · constructor · intro h; contrapose h simp only [not_not, not_lt, multibrot_basin', potential, fill_coe, Super.basin, - mem_setOf, multibrotExt_coe] at h ⊢ + mem_ofPred, multibrotExt_coe] at h ⊢ rw [s.potential_eq_one]; exact h · intro m; rw [← norm_bottcher]; simp only [bottcher, fill_coe] simp only [multibrotExt_coe] at m @@ -666,7 +679,7 @@ public theorem bottcher_large_approx (d : ℕ) [Fact (2 ≤ d)] (c : ℂ) : have m := bottcherNear_monic (s.superNearC.s (mem_univ c)) simp only [hasDerivAt_iff_tendsto, sub_zero, bottcherNear_zero, smul_eq_mul, mul_one, Metric.tendsto_nhds_nhds, Real.dist_eq, Complex.dist_eq] at m - simp only [Metric.tendsto_nhds, hasBasis_cobounded_norm_lt.eventually_iff, true_and, mem_setOf, + simp only [Metric.tendsto_nhds, hasBasis_cobounded_norm_lt.eventually_iff, true_and, mem_ofPred, Complex.dist_eq] intro e ep; rcases m e ep with ⟨r, rp, h⟩; use 1 / r; intro z zr have az0 : ‖z‖ ≠ 0 := (lt_trans (one_div_pos.mpr rp) zr).ne' diff --git a/Ray/Multibrot/Bottcher.lean b/Ray/Multibrot/Bottcher.lean index 255f802..972c6b6 100644 --- a/Ray/Multibrot/Bottcher.lean +++ b/Ray/Multibrot/Bottcher.lean @@ -54,7 +54,7 @@ variable {d : ℕ} [Fact (2 ≤ d)] /-- `z⁻¹` is in the `superNearC` region for large `z` -/ lemma inv_mem_t (z3 : 3 < ‖z‖) (cz : ‖c‖ ≤ ‖z‖) : z⁻¹ ∈ superNearT d c := by - simp only [mem_setOf, norm_inv, superNearT, one_div] + simp only [mem_ofPred, norm_inv, superNearT, one_div] refine ⟨by bound, ?_⟩ by_cases c0 : c = 0 · simp [c0] @@ -385,17 +385,16 @@ public theorem potential_approx_strong_10 (d : ℕ) [Fact (2 ≤ d)] (z10 : 10 /-- bottcher is monic at `∞` (has derivative 1) -/ public theorem bottcher_hasDerivAt_one : HasDerivAt (bottcher_inv d) 1 0 := by - rw [HasDerivAt, HasDerivAtFilter, bottcher_inv_def, bottcher, hasFDerivAtFilter_iff_isLittleO, - coe_zero, inv_zero', fill_inf] - simp only [sub_zero, ContinuousLinearMap.toSpanSingleton_apply, smul_eq_mul, mul_one] + rw [hasDerivAt_iff_isLittleO] + simp only [bottcher_inv_zero, sub_zero, smul_eq_mul, mul_one] rw [Asymptotics.isLittleO_iff] intro k k0; rw [Metric.eventually_nhds_iff] refine ⟨min 16⁻¹ (k / 16), by bound, ?_⟩; intro z le simp only [dist_eq_norm, sub_zero, lt_min_iff] at le by_cases z0 : z = 0 - · simp only [z0, coe_zero, inv_zero', fill_inf, sub_zero, norm_zero, + · simp only [z0, bottcher_inv_zero, sub_zero, norm_zero, MulZeroClass.mul_zero, le_refl] - simp only [inv_coe z0, fill_coe] + simp only [bottcher_inv_def, bottcher, inv_coe z0, fill_coe] have b := bottcher_approx d (c := z⁻¹) ?_ · simp only [inv_inv] at b; apply le_trans b simp only [norm_inv, inv_inv, pow_two, ← mul_assoc] @@ -415,7 +414,8 @@ public theorem bottcher_mfderiv_inf_ne_zero : mfderiv I I (bottcher d) ∞ ≠ 0 PartialEquiv.symm_symm, coePartialEquiv_apply, Equiv.toPartialEquiv_symm_apply, invEquiv_symm, ModelWithCorners.Boundaryless.range_eq_univ, fderivWithin_univ] rw [← bottcher_inv_def, bottcher_hasDerivAt_one.hasFDerivAt.fderiv] - rw [Ne, ContinuousLinearMap.ext_iff, not_forall]; use 1 - simp only [ContinuousLinearMap.toSpanSingleton_apply, smul_eq_mul, mul_one] - convert one_ne_zero - exact NeZero.one + intro h + have h1 : (ContinuousLinearMap.toSpanSingleton ℂ (1 : ℂ)) (1 : ℂ) = 0 := + ContinuousLinearMap.ext_iff.mp h (1 : ℂ) + simp only [ContinuousLinearMap.toSpanSingleton_apply, smul_eq_mul, mul_one] at h1 + exact one_ne_zero h1 diff --git a/Ray/Multibrot/Connected.lean b/Ray/Multibrot/Connected.lean index 91b02fe..d0eeac7 100644 --- a/Ray/Multibrot/Connected.lean +++ b/Ray/Multibrot/Connected.lean @@ -108,7 +108,7 @@ public theorem isConnected_compl_multibrot (d : ℕ) [Fact (2 ≤ d)] : have e : (_root_.multibrot d)ᶜ = (fun z : 𝕊 ↦ z.toComplex) '' (multibrotExt d \ {∞}) := by apply Set.ext; intro z; simp only [mem_compl_iff, mem_image]; constructor · intro m; use z - simp only [multibrotExt_coe, m, toComplex_coe, not_false_iff, mem_diff, and_true, + simp only [multibrotExt_coe, m, toComplex_coe, not_false_iff, mem_sdiff, and_true, mem_singleton_iff, coe_ne_inf] · intro ⟨w, ⟨m, wi⟩, wz⟩; induction w using OnePoint.rec · contrapose wi; clear wi; simp only [mem_singleton_iff] diff --git a/Ray/Multibrot/Defs.lean b/Ray/Multibrot/Defs.lean index b4e7b1c..0413a42 100644 --- a/Ray/Multibrot/Defs.lean +++ b/Ray/Multibrot/Defs.lean @@ -62,7 +62,7 @@ public theorem analytic_f' {d : ℕ} : AnalyticOnNhd ℂ (uncurry (f' d)) univ : theorem tendsto_f'_cobounded (c : ℂ) : Tendsto (uncurry (f' d)) (𝓝 c ×ˢ cobounded ℂ) (cobounded ℂ) := by - simp only [hasBasis_cobounded_norm_lt.tendsto_right_iff, Set.mem_setOf_eq, + simp only [hasBasis_cobounded_norm_lt.tendsto_right_iff, Set.mem_ofPred_eq, forall_true_left, uncurry, Metric.eventually_nhds_prod_iff] intro r; use 1, zero_lt_one, fun z ↦ max r 0 + ‖c‖ + 1 < ‖z‖; constructor · refine (eventually_cobounded (max r 0 + ‖c‖ + 1)).mp (.of_forall fun w h ↦ ?_) diff --git a/Ray/Multibrot/Isomorphism.lean b/Ray/Multibrot/Isomorphism.lean index 18098dc..1d6ca35 100644 --- a/Ray/Multibrot/Isomorphism.lean +++ b/Ray/Multibrot/Isomorphism.lean @@ -73,8 +73,8 @@ public theorem bottcher_inj : InjOn (bottcher d) (multibrotExt d) := by set t2 := {q : 𝕊 × 𝕊 | q.1 ≠ q.2 ∧ q ∈ t1} have t2ne : t2.Nonempty := by refine ⟨⟨x, y⟩, xy, bxy, ?_, ?_⟩ - · simp only [mem_setOf, ← hb, le_refl, u] - · simp only [mem_setOf, ← hb, ← norm_bottcher, bxy, le_refl, u] + · simp only [mem_ofPred, ← hb, le_refl, u] + · simp only [mem_ofPred, ← hb, ← norm_bottcher, bxy, le_refl, u] clear x xm y ym bxy xy hb have ue : u ⊆ multibrotExt d := by intro c m; rw [← potential_lt_one]; exact lt_of_le_of_lt m b1 have t01 : t1 ⊆ t0 := inter_subset_right diff --git a/Ray/Multibrot/KoebeInf.lean b/Ray/Multibrot/KoebeInf.lean index f8bcc05..e344601 100644 --- a/Ray/Multibrot/KoebeInf.lean +++ b/Ray/Multibrot/KoebeInf.lean @@ -80,7 +80,7 @@ public lemma small_mem_ext (xc : ‖x‖ < rinv 4⁻¹ c / 4) : (c, x) ∈ (supe obtain ⟨z,_,_,zp,zx⟩ := sbottcher_inv_small_mem_preimage (d := d) xc simp only [sbottcher_inv_def] at zx have t := ((superF d).homeomorphSlice c).map_target (x := z⁻¹) - simp only [Super.target_homeomorphSlice, mem_setOf_eq, zp, Super.source_homeomorphSlice, + simp only [Super.target_homeomorphSlice, mem_ofPred_eq, zp, Super.source_homeomorphSlice, Super.invFun_homeomorphSlice, forall_const] at t simpa [zx] using t diff --git a/Ray/Multibrot/Log1p.lean b/Ray/Multibrot/Log1p.lean index 9066f61..cce8e06 100644 --- a/Ray/Multibrot/Log1p.lean +++ b/Ray/Multibrot/Log1p.lean @@ -35,7 +35,8 @@ public lemma Complex.norm_log_one_add_le' {z : ℂ} (z1 : ‖z‖ < 1) : HasDerivAt (fun t : ℝ ↦ -Real.log (1 - t * ‖z‖)) (- (-‖z‖ / (1 - t * ‖z‖))) t := by intro t m simp only [zero_le_one, uIcc_of_le, mem_Icc] at m - exact (((hasDerivAt_mul_const _).const_sub _).log ((sub_pos.mpr (m1 _ m.2)).ne')).neg + exact (((hasDerivAt_mul_const (x := t) ‖z‖).const_sub 1).log + ((sub_pos.mpr (m1 _ m.2)).ne')).neg have ic : IntervalIntegrable (fun t ↦ z / (1 + t*z)) MeasureTheory.volume 0 1 := by apply ContinuousOn.intervalIntegrable_of_Icc zero_le_one apply continuousOn_const.div (Continuous.continuousOn (by continuity)) diff --git a/Ray/Multibrot/RayEqn.lean b/Ray/Multibrot/RayEqn.lean index 275a980..fb6b234 100644 --- a/Ray/Multibrot/RayEqn.lean +++ b/Ray/Multibrot/RayEqn.lean @@ -98,8 +98,9 @@ public lemma cascade_succ (m : z ∈ ball (0 : ℂ) 1) : unfold f rw [toComplex_lift', f', mul_add, mul_pow, add_right_inj, ray'_eq_pray m, div_eq_inv_mul, ← mul_assoc, pow_sub₀ _ z0 (by bound), pow_one, pow_mul] - rw [ne_eq, s.ray_eq_a_iff em] - simp only [pow_eq_zero_iff', z0, ne_eq, not_and, not_not, false_and, not_false_eq_true] + intro h + have h2 := (s.ray_eq_a_iff em).mp h + simp only [pow_eq_zero_iff', z0, ne_eq, false_and] at h2 /-- The whole `cascade` is analytic -/ public lemma cascade_analytic (m : z ∈ ball (0 : ℂ) 1) : ContDiffAt ℂ ⊤ (cascade d n) z := by diff --git a/Ray/Multibrot/Rinv.lean b/Ray/Multibrot/Rinv.lean index c22787a..96f5422 100644 --- a/Ray/Multibrot/Rinv.lean +++ b/Ray/Multibrot/Rinv.lean @@ -51,11 +51,11 @@ public lemma le_rinv : x ≤ rinv r c ↔ x ≤ r ∧ ‖c‖ * x ≤ 1 := by simp only [div_eq_mul_inv, inv_rinv r0] @[simp] public lemma mem_ball_rinv : z ∈ ball 0 (rinv r c) ↔ ‖z‖ < r ∧ ‖c‖ * ‖z‖ < 1 := by - simp only [ball, dist_zero_right, lt_rinv, mem_setOf_eq] + simp only [ball, dist_zero_right, lt_rinv, mem_ofPred_eq] @[simp] public lemma mem_closedBall_rinv : z ∈ closedBall 0 (rinv r c) ↔ ‖z‖ ≤ r ∧ ‖c‖ * ‖z‖ ≤ 1 := by - simp only [closedBall, dist_zero_right, le_rinv, mem_setOf_eq] + simp only [closedBall, dist_zero_right, le_rinv, mem_ofPred_eq] @[simp] public lemma zero_mem_ball_rinv (r0 : 0 < r := by norm_num) : 0 ∈ ball (0 : ℂ) (rinv r c) := by simp; bound diff --git a/Ray/Schwarz/SchwarzPick.lean b/Ray/Schwarz/SchwarzPick.lean index 23b9ad6..93647bf 100644 --- a/Ray/Schwarz/SchwarzPick.lean +++ b/Ray/Schwarz/SchwarzPick.lean @@ -60,7 +60,8 @@ lemma ContDiffOn.norm_le_norm_of_mapsTo_closedBall (fa : ContDiffOn ℂ ω f (ba · have w0 := f0 ▸ c 0 (by simp [r0]) rw [c _ (by simp [zr]), ← w0, norm_zero] bound - · exact Complex.norm_le_norm_of_mapsTo_ball_self (fa.differentiableOn (by decide)) m f0 zr + · exact Complex.norm_le_norm_of_mapsTo_ball (fa.differentiableOn (by decide)) + (m.mono_right Metric.ball_subset_closedBall) f0 zr /-! ### Unit ball versions @@ -85,7 +86,8 @@ public lemma ContDiffOn.dist_le_mul_mobius_of_mapsTo_unit_ball (fa : ContDiffOn have u1 : ‖u‖ < 1 := norm_mobius_lt_one z1 w1 simpa only [g, Function.comp_apply, mobius_def (f z), u, mobius_mobius z1 w1, norm_div, div_le_iff₀ (norm_mobius_denom_pos fz1 fw1), mul_comm ‖mobius _ _‖] using - Complex.norm_le_norm_of_mapsTo_ball_self (ga.differentiableOn (by decide)) gm g0 u1 + Complex.norm_le_norm_of_mapsTo_ball (ga.differentiableOn (by decide)) + (gm.mono_right Metric.ball_subset_closedBall) g0 u1 /-- Derivative version of Schwarz-Pick for the unit disk -/ public lemma ContDiffOn.norm_deriv_le_div_of_mapsTo_unit_ball (fa : ContDiffOn ℂ ω f (ball 0 1)) @@ -109,6 +111,7 @@ public lemma ContDiffOn.norm_deriv_le_div_of_mapsTo_unit_ball (fa : ContDiffOn simp only [mobius_def, Complex.norm_div, ← mul_div_assoc, mul_div_right_comm] at s rw [← div_le_iff₀ (norm_pos_iff.mpr (by grind))] at s simpa [slope, ← div_eq_inv_mul, norm_sub_rev (f w), norm_sub_rev w] + have fc : ContinuousAt f z := df.continuousAt have dc : ContinuousAt (fun w ↦ ‖1 - conj (f z) * f w‖ / ‖1 - conj z * w‖) z := ContinuousAt.div (by fun_prop) (by fun_prop) (norm_mobius_denom_pos z1 z1).ne' have t1 := (continuous_norm.tendsto _).comp df.hasDerivAt.tendsto_slope diff --git a/lake-manifest.json b/lake-manifest.json index 0dc38fc..697a179 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,21 +1,21 @@ -{"version": "1.1.0", +{"version": "1.2.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "725c803ee924f55342e93f2c75976051ab902b54", + "rev": "db584cd6d46c92f209a44c0f1c829460d327499d", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.33.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b3dd6c3ebc0a71685e86bea9223be39ea4c299fb", + "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28", + "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "cff9dd30f2c161b9efd7c657cafed1f967645890", + "rev": "16f02aa7642864af59f1ff0e384a015994db9118", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,17 +45,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ef8377f31b5535430b6753a974d685b0019d0681", + "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.84", + "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "fa78cf032194308a950a264ed87b422a2a7c1c6c", + "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8920dcbb96a4e8bf641fc399ac9c0888e4a6be72", + "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2e16f91af2a97975e5d2fac906494cd6c17ba255", + "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,11 +85,12 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "726b98c53e2da249c1de768fbbbb5e67bc9cef60", + "rev": "6130a47896ce867c6a4a55373441e59e565bad0f", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.27.0-rc1", + "inputRev": "v4.33.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "ray", - "lakeDir": ".lake"} + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lakefile.lean b/lakefile.lean index dc7fd2b..de23a16 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -9,7 +9,7 @@ package ray where ⟨`experimental.module, true⟩, ] -require "leanprover-community" / "mathlib" @ git "master" +require "leanprover-community" / "mathlib" @ git "v4.33.0" @[default_target] lean_lib Ray diff --git a/lean-toolchain b/lean-toolchain index bd19bde..025e595 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.27.0-rc1 +leanprover/lean4:v4.33.0