From 5ff919f92b47f4b36d667968c09d0970befdaa75 Mon Sep 17 00:00:00 2001 From: Geoffrey Irving Date: Sat, 14 Sep 2024 15:52:32 +0100 Subject: [PATCH] lake update --- Ray/Analytic/Analytic.lean | 4 +- Ray/Analytic/Within.lean | 27 +++++--- Ray/AnalyticManifold/AnalyticManifold.lean | 69 ++++++++++--------- Ray/AnalyticManifold/GlobalInverse.lean | 2 +- Ray/AnalyticManifold/Inverse.lean | 8 +-- Ray/AnalyticManifold/Nonseparating.lean | 38 +++++----- Ray/AnalyticManifold/Nontrivial.lean | 14 ++-- Ray/AnalyticManifold/OneDimension.lean | 8 +-- Ray/AnalyticManifold/OpenMapping.lean | 10 +-- Ray/AnalyticManifold/RiemannSphere.lean | 40 ++++++----- .../SmoothManifoldWithCorners.lean | 2 +- Ray/Dynamics/BottcherNear.lean | 4 +- Ray/Dynamics/BottcherNearM.lean | 30 ++++---- Ray/Dynamics/Grow.lean | 20 +++--- Ray/Dynamics/Multibrot/Basic.lean | 26 +++---- Ray/Dynamics/Multibrot/Bottcher.lean | 4 +- Ray/Dynamics/Multibrot/Connected.lean | 6 +- Ray/Dynamics/Multibrot/Isomorphism.lean | 2 +- Ray/Dynamics/Multibrot/Iterates.lean | 4 +- Ray/Dynamics/Multibrot/Log1p.lean | 2 +- Ray/Dynamics/Multibrot/Potential.lean | 4 +- Ray/Dynamics/Multiple.lean | 10 +-- Ray/Dynamics/Postcritical.lean | 2 +- Ray/Dynamics/Potential.lean | 18 ++--- Ray/Dynamics/Ray.lean | 4 +- Ray/Hartogs/FubiniBall.lean | 7 +- Ray/Hartogs/Hartogs.lean | 12 ++-- Ray/Hartogs/MaxLog.lean | 8 +-- Ray/Hartogs/Subharmonic.lean | 6 +- Ray/Misc/AtInf.lean | 6 +- Ray/Misc/Bounds.lean | 2 +- Ray/Misc/Connected.lean | 4 +- Ray/Misc/Measure.lean | 4 +- Ray/Render/Color.lean | 2 +- Ray/Render/Iterate.lean | 10 +-- Ray/Render/Potential.lean | 2 +- lake-manifest.json | 26 ++++--- lakefile.lean | 3 +- lean-toolchain | 2 +- 39 files changed, 233 insertions(+), 219 deletions(-) diff --git a/Ray/Analytic/Analytic.lean b/Ray/Analytic/Analytic.lean index 09d4e69..5139477 100644 --- a/Ray/Analytic/Analytic.lean +++ b/Ray/Analytic/Analytic.lean @@ -182,7 +182,7 @@ lemma FormalMultilinearSeries.unshift_radius' (p : FormalMultilinearSeries 𝕜 intro n; induction' n with n _ · simp only [FormalMultilinearSeries.unshift_coeff_zero, FormalMultilinearSeries.norm_apply_eq_norm_coef, pow_zero, mul_one, le_max_iff, le_refl, - true_or_iff] + true_or] · simp only [FormalMultilinearSeries.norm_apply_eq_norm_coef] at h simp only [FormalMultilinearSeries.unshift_coeff_succ, pow_succ, ← mul_assoc, FormalMultilinearSeries.norm_apply_eq_norm_coef, le_max_iff] @@ -331,7 +331,7 @@ theorem orderAt_const_smul {f : 𝕜 → E} {c a : 𝕜} (a0 : a ≠ 0) : by_cases fa : AnalyticAt 𝕜 f c · rcases fa with ⟨p, fp⟩ have e : ∀ n, a • p n ≠ 0 ↔ p n ≠ 0 := fun n ↦ by - simp only [a0, Ne, smul_eq_zero, false_or_iff] + simp only [a0, Ne, smul_eq_zero, false_or] simp only [fp.orderAt_unique, fp.const_smul.orderAt_unique, FormalMultilinearSeries.order, e] · have ga := fa; rw [← analyticAt_iff_const_smul a0] at ga simp only [orderAt, fa, ga]; rw [dif_neg, dif_neg] diff --git a/Ray/Analytic/Within.lean b/Ray/Analytic/Within.lean index 9082b6d..69d48e0 100644 --- a/Ray/Analytic/Within.lean +++ b/Ray/Analytic/Within.lean @@ -27,21 +27,26 @@ lemma AnalyticWithinAt.congr_set {f : E → F} {s t : Set E} {x : E} (hf : Analy r_pos := by bound hasSum := by intro y m n - simp only [EMetric.mem_ball, lt_min_iff, edist_lt_ofReal, dist_zero_right] at m n ⊢ - exact hp.hasSum (by simpa only [mem_def, dist_self_add_left, n.1, @st (x + y)]) n.2 - continuousWithinAt := by - have e : 𝓝[s] x = 𝓝[t] x := nhdsWithin_eq_iff_eventuallyEq.mpr hst - simpa only [ContinuousWithinAt, e] using hp.continuousWithinAt }⟩ + apply hp.hasSum + simp only [mem_insert_iff, add_right_eq_self, EMetric.mem_ball, lt_min_iff, edist_lt_ofReal, + dist_zero_right] at m n ⊢ + rcases m with m | m + · exact .inl m + · specialize @st (x + y) _ + · simpa only [dist_self_add_left] using n.1 + · simp only [eq_iff_iff] at st + exact Or.inr (st.mpr m) + · simp only [EMetric.mem_ball, lt_min_iff, edist_lt_ofReal, dist_zero_right] at n ⊢ + exact n.2 }⟩ /-- Analyticity within is open (within the set) -/ lemma AnalyticWithinAt.eventually_analyticWithinAt [CompleteSpace F] {f : E → F} {s : Set E} {x : E} (hf : AnalyticWithinAt 𝕜 f s x) : ∀ᶠ y in 𝓝[s] x, AnalyticWithinAt 𝕜 f s y := by - obtain ⟨_, g, fg, ga⟩ := analyticWithinAt_iff_exists_analyticAt.mp hf + obtain ⟨g, fg, ga⟩ := analyticWithinAt_iff_exists_analyticAt.mp hf simp only [Filter.EventuallyEq, eventually_nhdsWithin_iff] at fg ⊢ filter_upwards [fg.eventually_nhds, ga.eventually_analyticAt] intro z fg ga zs - refine analyticWithinAt_iff_exists_analyticAt.mpr ⟨?_, g, ?_, ga⟩ - · refine ga.continuousAt.continuousWithinAt.congr_of_eventuallyEq ?_ (fg.self_of_nhds zs) - rw [← eventually_nhdsWithin_iff] at fg - exact fg - · simpa only [Filter.EventuallyEq, eventually_nhdsWithin_iff] + refine analyticWithinAt_iff_exists_analyticAt.mpr ⟨g, ?_, ga⟩ + rw [← eventually_nhdsWithin_iff] at fg + refine fg.filter_mono (nhdsWithin_mono _ ?_) + simp only [zs, insert_eq_of_mem, subset_insert] diff --git a/Ray/AnalyticManifold/AnalyticManifold.lean b/Ray/AnalyticManifold/AnalyticManifold.lean index 4122163..f7268dd 100644 --- a/Ray/AnalyticManifold/AnalyticManifold.lean +++ b/Ray/AnalyticManifold/AnalyticManifold.lean @@ -161,7 +161,7 @@ theorem MAnalyticOn.continuousOn {f : M → N} {s : Set M} (h : MAnalyticOn I J /-- Constants are analytic -/ theorem mAnalyticAt_const {x : M} {c : N} : MAnalyticAt I J (fun _ ↦ c) x := by rw [mAnalyticAt_iff]; use continuousAt_const - simp only [Prod.fst_comp_mk, Function.comp] + simp only [Prod.fst_comp_mk, Function.comp_def] exact analyticAt_const.analyticWithinAt /-- Constants are analytic -/ @@ -304,9 +304,39 @@ theorem MAnalyticAt.congr [CompleteSpace F] {f g : M → N} {x : M} (fa : MAnaly refine Filter.EventuallyEq.fun_comp ?_ (_root_.extChartAt J (g x)) have t := (continuousAt_extChartAt_symm I x).tendsto rw [PartialEquiv.left_inv _ (mem_extChartAt_source I x)] at t - exact e.comp_tendsto (t.mono_left nhdsWithin_le_nhds) + exact (e.comp_tendsto (t.mono_left nhdsWithin_le_nhds)).symm · simp only [e.self_of_nhds, Function.comp, PartialEquiv.left_inv _ (mem_extChartAt_source _ _)] +/-- `MAnalyticAt` for `x ↦ (f x, g x)` -/ +theorem MAnalyticAt.prod {f : O → M} {g : O → N} {x : O} + (fh : MAnalyticAt K I f x) (gh : MAnalyticAt K J g x) : + MAnalyticAt K (I.prod J) (fun x ↦ (f x, g x)) x := by + rw [mAnalyticAt_iff] at fh gh ⊢; use fh.1.prod gh.1 + refine (fh.2.prod gh.2).congr_of_eventuallyEq ?_ ?_ + simp only [eventuallyEq_nhdsWithin_iff] + refine .of_forall fun y _ ↦ ?_ + simp only [extChartAt_prod, Function.comp, PartialEquiv.prod_coe] + simp only [mfld_simps] + +/-- `MAnalytic` for `x ↦ (f x, g x)` -/ +theorem MAnalytic.prod {f : O → M} {g : O → N} (fh : MAnalytic K I f) (gh : MAnalytic K J g) : + MAnalytic K (I.prod J) fun x ↦ (f x, g x) := fun x ↦ (fh x).prod (gh x) + +/-- `id` is analytic -/ +theorem mAnalyticAt_id {x : M} : MAnalyticAt I I (fun x ↦ x) x := by + rw [mAnalyticAt_iff] + use continuousAt_id + refine (analyticAt_id _ _).analyticWithinAt.congr_of_eventuallyEq ?_ ?_ + · simp only [mfld_simps, Filter.EventuallyEq, id, ← I.map_nhds_eq, Filter.eventually_map] + filter_upwards [(chartAt A x).open_target.eventually_mem (mem_chart_target _ _)] + intro y m + simp only [(chartAt A x).right_inv m] + · simp only [mfld_simps] + +/-- `id` is analytic -/ +theorem mAnalytic_id : MAnalytic I I fun x : M ↦ x := + fun _ ↦ mAnalyticAt_id + variable [CompleteSpace E] [CompleteSpace F] /-- MAnalytic functions compose -/ @@ -347,17 +377,6 @@ theorem MAnalyticAt.comp_of_eq {f : N → M} {g : O → N} {x : O} {y : N} MAnalyticAt K I (fun x ↦ f (g x)) x := by rw [← e] at fh; exact fh.comp gh -/-- `MAnalyticAt` for `x ↦ (f x, g x)` -/ -theorem MAnalyticAt.prod {f : O → M} {g : O → N} {x : O} - (fh : MAnalyticAt K I f x) (gh : MAnalyticAt K J g x) : - MAnalyticAt K (I.prod J) (fun x ↦ (f x, g x)) x := by - rw [mAnalyticAt_iff] at fh gh ⊢; use fh.1.prod gh.1 - refine (fh.2.prod gh.2).congr_of_eventuallyEq ?_ ?_ - simp only [eventuallyEq_nhdsWithin_iff] - refine .of_forall fun y _ ↦ ?_ - simp only [extChartAt_prod, Function.comp, PartialEquiv.prod_coe] - simp only [mfld_simps] - /-- `MAnalyticAt.comp` for a function of two arguments -/ theorem MAnalyticAt.comp₂ [CompleteSpace H] {h : N × M → P} {f : O → N} {g : O → M} {x : O} @@ -365,10 +384,6 @@ theorem MAnalyticAt.comp₂ [CompleteSpace H] {h : N × M → P} {f : O → N} (ga : MAnalyticAt K I g x) : MAnalyticAt K L (fun x ↦ h (f x, g x)) x := ha.comp (g := fun x ↦ (f x, g x)) (fa.prod ga) -/-- `MAnalytic` for `x ↦ (f x, g x)` -/ -theorem MAnalytic.prod {f : O → M} {g : O → N} (fh : MAnalytic K I f) (gh : MAnalytic K J g) : - MAnalytic K (I.prod J) fun x ↦ (f x, g x) := fun x ↦ (fh x).prod (gh x) - /-- `MAnalyticAt.comp₂`, with a separate argument for point equality -/ theorem MAnalyticAt.comp₂_of_eq [CompleteSpace H] {h : N × M → P} {f : O → N} {g : O → M} {x : O} {y : N × M} (ha : MAnalyticAt (J.prod I) L h y) (fa : MAnalyticAt K J f x) @@ -407,21 +422,6 @@ theorem MAnalyticAt.analyticAt (I : ModelWithCorners 𝕜 E A) [I.Boundaryless] MAnalyticAt I J f x → AnalyticAt 𝕜 f x := (analyticAt_iff_mAnalyticAt _ _).mpr -/-- `id` is analytic -/ -theorem mAnalyticAt_id {x : M} : MAnalyticAt I I (fun x ↦ x) x := by - rw [mAnalyticAt_iff] - use continuousAt_id - refine (analyticAt_id _ _).analyticWithinAt.congr_of_eventuallyEq ?_ ?_ - · simp only [mfld_simps, Filter.EventuallyEq, id, ← I.map_nhds_eq, Filter.eventually_map] - filter_upwards [(chartAt A x).open_target.eventually_mem (mem_chart_target _ _)] - intro y m - simp only [(chartAt A x).right_inv m] - · simp only [mfld_simps] - -/-- `id` is analytic -/ -theorem mAnalytic_id : MAnalytic I I fun x : M ↦ x := - fun _ ↦ mAnalyticAt_id - /-- Curried analytic functions are analytic in the first coordinate -/ theorem MAnalyticAt.along_fst [CompleteSpace G] [CompleteSpace H] [AnalyticManifold I M] {f : M → O → P} {x : M} {y : O} (fa : MAnalyticAt (I.prod K) L (uncurry f) (x, y)) : @@ -521,10 +521,11 @@ theorem MAnalyticAt.eventually [I.Boundaryless] [J.Boundaryless] [AnalyticManifo clear a have h' := (MAnalyticAt.extChartAt_symm (PartialEquiv.map_source _ fm.self_of_nhds)).comp_of_eq (h.comp (MAnalyticAt.extChartAt m)) ?_ - · apply h'.congr; clear h h' + · apply h'.congr + clear h h' apply ((isOpen_extChartAt_source I x).eventually_mem m).mp refine fm.mp (.of_forall fun z mf m ↦ ?_) - simp only [PartialEquiv.left_inv _ m, PartialEquiv.left_inv _ mf] + simp only [PartialEquiv.left_inv _ m, PartialEquiv.left_inv _ mf, Function.comp_def] · simp only [Function.comp, PartialEquiv.left_inv _ m] /-- The domain of analyticity is open -/ diff --git a/Ray/AnalyticManifold/GlobalInverse.lean b/Ray/AnalyticManifold/GlobalInverse.lean index 65285e6..caa68b4 100644 --- a/Ray/AnalyticManifold/GlobalInverse.lean +++ b/Ray/AnalyticManifold/GlobalInverse.lean @@ -120,7 +120,7 @@ theorem weak_global_complex_inverse_fun_open {f : S → T} [Nonempty S] {s : Set rcases global_complex_inverse_fun_open fa' nc' inj' (isOpen_univ.prod so) with ⟨g, ga, gf⟩ use g 0; constructor · intro z ⟨w, m⟩; refine (ga ⟨0, z⟩ ⟨⟨0, w⟩, ⟨mem_univ _, m.1⟩, ?_⟩).along_snd - simp only [Prod.ext_iff, eq_self_iff_true, true_and_iff]; exact m.2 + simp only [Prod.ext_iff, eq_self_iff_true, true_and]; exact m.2 · intro z m; exact gf ⟨0, z⟩ ⟨mem_univ _, m⟩ /-- The global 1D inverse function theorem (open case): if `f : S → T` is injective on an diff --git a/Ray/AnalyticManifold/Inverse.lean b/Ray/AnalyticManifold/Inverse.lean index 322ab7d..afbb339 100644 --- a/Ray/AnalyticManifold/Inverse.lean +++ b/Ray/AnalyticManifold/Inverse.lean @@ -213,11 +213,11 @@ theorem Cinv.left_inv (i : Cinv f c z) : ∀ᶠ x : ℂ × S in 𝓝 (c, z), i.g exact (continuousOn_extChartAt _ _).isOpen_inter_preimage (isOpen_extChartAt_source _ _) i.he.open_source have m : (c, z) ∈ t := by - simp only [mem_inter_iff, mem_preimage, mem_extChartAt_source, true_and_iff, ← ht] + simp only [mem_inter_iff, mem_preimage, mem_extChartAt_source, true_and, ← ht] exact ContDiffAt.mem_toPartialHomeomorph_source i.ha.contDiffAt i.has_dhe le_top apply Filter.eventuallyEq_of_mem (o.mem_nhds m); intro x m simp only [mem_inter_iff, mem_preimage, extChartAt_prod, extChartAt_eq_refl, ← ht, - PartialEquiv.prod_source, PartialEquiv.refl_source, mem_prod_eq, mem_univ, true_and_iff, + PartialEquiv.prod_source, PartialEquiv.refl_source, mem_prod_eq, mem_univ, true_and, PartialEquiv.prod_coe, PartialEquiv.refl_coe, id] at m have inv := i.he.left_inv m.2 simp only [Cinv.g] @@ -249,7 +249,7 @@ theorem Cinv.right_inv (i : Cinv f c z) : simp only [Cinv.h, Cinv.z', Cinv.f', PartialEquiv.left_inv _ (mem_extChartAt_source _ _)] rw [e] at m; exact m have m : (c, f c z) ∈ t := by - simp only [m', mem_inter_iff, mem_preimage, mem_extChartAt_source, true_and_iff, ← ht, + simp only [m', mem_inter_iff, mem_preimage, mem_extChartAt_source, true_and, ← ht, extChartAt_prod, PartialEquiv.prod_coe, extChartAt_eq_refl, PartialEquiv.refl_coe, id, PartialEquiv.prod_source, prod_mk_mem_set_prod_eq, PartialEquiv.refl_source, mem_univ] have fm : ∀ᶠ x : ℂ × T in 𝓝 (c, f c z), @@ -273,7 +273,7 @@ theorem Cinv.right_inv (i : Cinv f c z) : refine fm.mp (Filter.eventually_of_mem (o.mem_nhds m) ?_) intro x m mf simp only [mem_inter_iff, mem_preimage, extChartAt_prod, extChartAt_eq_refl, - PartialEquiv.prod_source, PartialEquiv.refl_source, mem_prod_eq, mem_univ, true_and_iff, + PartialEquiv.prod_source, PartialEquiv.refl_source, mem_prod_eq, mem_univ, true_and, PartialEquiv.prod_coe, PartialEquiv.refl_coe, id, ← ht] at m have inv := i.he.right_inv m.2 simp only [Cinv.g] diff --git a/Ray/AnalyticManifold/Nonseparating.lean b/Ray/AnalyticManifold/Nonseparating.lean index 04db288..2f5e4c6 100644 --- a/Ray/AnalyticManifold/Nonseparating.lean +++ b/Ray/AnalyticManifold/Nonseparating.lean @@ -33,15 +33,15 @@ theorem Nonseparating.univ_prod [LocallyConnectedSpace X] {t : Set Y} (n : Nonse Nonseparating ((univ : Set X) ×ˢ t) := by have e : ((univ : Set X) ×ˢ t)ᶜ = univ ×ˢ tᶜ := by apply Set.ext; intro ⟨a, x⟩; rw [mem_compl_iff] - simp only [prod_mk_mem_set_prod_eq, mem_univ, mem_compl_iff, true_and_iff] + simp only [prod_mk_mem_set_prod_eq, mem_univ, mem_compl_iff, true_and] constructor; · rw [e]; exact dense_univ.prod n.dense - · intro ⟨a, x⟩ u m un; simp only [mem_prod_eq, mem_univ, true_and_iff] at m + · intro ⟨a, x⟩ u m un; simp only [mem_prod_eq, mem_univ, true_and] at m rcases mem_nhds_prod_iff.mp un with ⟨u0, n0, u1, n1, uu⟩ rcases n.loc x u1 m n1 with ⟨c1, cs1, cn1, cp1⟩ rcases locallyConnectedSpace_iff_open_connected_subsets.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_iff] at m' ⊢ + · intro ⟨b, y⟩ m'; simp only [mem_prod_eq, mem_diff, 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 @@ -61,17 +61,17 @@ theorem Nonseparating.complexManifold {t : Set S} (isOpen_extChartAt_target I z) uo have vn : v.Nonempty := by use extChartAt I z z - simp only [mem_inter_iff, mem_extChartAt_target, true_and_iff, mem_preimage, + simp only [mem_inter_iff, mem_extChartAt_target, true_and, mem_preimage, PartialEquiv.left_inv _ (mem_extChartAt_source I z), m, ← hv] rcases dense_iff_inter_open.mp (h z).dense v vo vn with ⟨y, m⟩ use(extChartAt I z).symm y simp only [mem_inter_iff, mem_preimage, mem_compl_iff, not_and, ← hv] at m rcases m with ⟨⟨ym, yu⟩, yt⟩ - simp only [mem_inter_iff, ym, yu, true_and_iff, mem_compl_iff]; exact yt ym + simp only [mem_inter_iff, ym, yu, true_and, mem_compl_iff]; exact yt ym loc := by intro z u zt un have m : extChartAt I z z ∈ (extChartAt I z).target ∩ (extChartAt I z).symm ⁻¹' t := by - simp only [mem_inter_iff, mem_extChartAt_target I z, true_and_iff, mem_preimage, + simp only [mem_inter_iff, mem_extChartAt_target I z, true_and, mem_preimage, PartialEquiv.left_inv _ (mem_extChartAt_source I z), zt] have n : (extChartAt I z).target ∩ (extChartAt I z).symm ⁻¹' u ∈ 𝓝 (extChartAt I z z) := by apply Filter.inter_mem @@ -88,7 +88,7 @@ theorem Nonseparating.complexManifold {t : Set S} 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_iff, + simp only [mem_diff, 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 @@ -104,7 +104,7 @@ theorem Nonseparating.complexManifold {t : Set S} simp only [PartialEquiv.left_inv _ xz, xt, PartialEquiv.map_source _ xz, not_false_iff, and_self_iff, eq_self_iff_true] · intro ⟨⟨y, ⟨⟨yz, yt⟩, yx⟩⟩, _⟩ - simp only [← yx, yt, PartialEquiv.map_target _ yz, not_false_iff, true_and_iff] + simp only [← yx, yt, PartialEquiv.map_target _ yz, not_false_iff, true_and] · rw [e]; apply cp.image; apply (continuousOn_extChartAt_symm I z).mono exact _root_.trans cs (_root_.trans diff_subset inter_subset_left) } @@ -124,11 +124,11 @@ 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_iff, and_false_iff, or_false_iff, ← hf] at m + simp only [mem_union, mem_setOf, xt, false_and, and_false, or_false, ← hf] at m simp only [not_not]; exact m simp only [not_not] at xt have n := m - simp only [mem_union, xt, xu, false_or_iff, true_and_iff, mem_setOf, + simp only [mem_union, xt, xu, false_or, true_and, mem_setOf, 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 @@ -148,7 +148,7 @@ theorem IsPreconnected.open_diff {s t : Set X} (sc : IsPreconnected s) (so : IsO 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 - simp only [m.2, false_and_iff, and_false_iff, or_false_iff, not_false_iff, and_true_iff] 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 @@ -181,15 +181,15 @@ theorem IsPreconnected.ball_diff_center {a : ℂ} {r : ℝ} : IsPreconnected (ba (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, - mem_prod_eq, mem_Ioo, mem_univ, and_true_iff] + mem_prod_eq, mem_Ioo, mem_univ, and_true] constructor · intro ⟨zr, za⟩; use abs (z - a), Complex.arg (z - a) simp only [AbsoluteValue.pos_iff, Ne, Complex.abs_mul_exp_arg_mul_I, - add_sub_cancel, eq_self_iff_true, sub_eq_zero, za, zr, not_false_iff, and_true_iff] + add_sub_cancel, eq_self_iff_true, sub_eq_zero, za, zr, not_false_iff, and_true] · intro ⟨s, t, ⟨s0, sr⟩, e⟩ simp only [← e, add_sub_cancel_left, Complex.abs.map_mul, Complex.abs_ofReal, abs_of_pos s0, - Complex.abs_exp_ofReal_mul_I, mul_one, sr, true_and_iff, add_right_eq_self, mul_eq_zero, - Complex.exp_ne_zero, or_false_iff, Complex.ofReal_eq_zero] + Complex.abs_exp_ofReal_mul_I, mul_one, sr, true_and, add_right_eq_self, mul_eq_zero, + Complex.exp_ne_zero, or_false, Complex.ofReal_eq_zero] exact s0.ne' rw [e]; apply IsPreconnected.image; exact isPreconnected_Ioo.prod isPreconnected_univ apply Continuous.continuousOn; continuity @@ -204,8 +204,8 @@ theorem Complex.nonseparating_singleton (a : ℂ) : Nonseparating ({a} : Set ℂ rcases Metric.isOpen_iff.mp uo a m with ⟨r, rp, rs⟩ use a + r / 2 simp only [mem_inter_iff, mem_compl_iff, mem_singleton_iff, add_right_eq_self, - div_eq_zero_iff, Complex.ofReal_eq_zero, one_ne_zero, or_false_iff, - rp.ne', not_false_iff, and_true_iff, false_or, two_ne_zero] + div_eq_zero_iff, Complex.ofReal_eq_zero, one_ne_zero, or_false, + rp.ne', not_false_iff, and_true, false_or, two_ne_zero] apply rs simp only [mem_ball, dist_self_add_left, Complex.norm_eq_abs, map_div₀, Complex.abs_ofReal, Complex.abs_two, abs_of_pos rp, half_lt_self rp] @@ -220,7 +220,7 @@ theorem AnalyticManifold.nonseparating_singleton (a : S) : Nonseparating ({a} : apply Nonseparating.complexManifold; intro z by_cases az : a ∈ (extChartAt I z).source · convert Complex.nonseparating_singleton (extChartAt I z a) - simp only [eq_singleton_iff_unique_mem, mem_inter_iff, PartialEquiv.map_source _ az, true_and_iff, + simp only [eq_singleton_iff_unique_mem, mem_inter_iff, PartialEquiv.map_source _ az, true_and, mem_preimage, mem_singleton_iff, PartialEquiv.left_inv _ az, eq_self_iff_true] intro x ⟨m, e⟩; simp only [← e, PartialEquiv.right_inv _ m] · convert Nonseparating.empty @@ -239,5 +239,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_iff, mem_singleton_iff] + simp only [mem_prod_eq, mem_setOf, mem_univ, true_and, mem_singleton_iff] rw [e]; exact Nonseparating.univ_prod (AnalyticManifold.nonseparating_singleton _) diff --git a/Ray/AnalyticManifold/Nontrivial.lean b/Ray/AnalyticManifold/Nontrivial.lean index 4cd0bb3..ef3a81c 100644 --- a/Ray/AnalyticManifold/Nontrivial.lean +++ b/Ray/AnalyticManifold/Nontrivial.lean @@ -89,7 +89,7 @@ theorem IsPreconnected.nontrivialAnalyticOn (p : IsPreconnected s) (fa : Analyti /-- Nonconstant entire functions are nontrivial -/ theorem Entire.nontrivialAnalyticOn (fa : AnalyticOn ℂ f univ) (ne : ∃ a b, f a ≠ f b) : NontrivialAnalyticOn f univ := by - refine isPreconnected_univ.nontrivialAnalyticOn fa ?_; simpa only [Set.mem_univ, true_and_iff] + refine isPreconnected_univ.nontrivialAnalyticOn fa ?_; simpa only [Set.mem_univ, true_and] /-- The roots of a nontrivial analytic function form a discrete topology -/ theorem NontrivialAnalyticOn.discreteTopology (n : NontrivialAnalyticOn f s) (a : ℂ) : @@ -128,8 +128,8 @@ theorem IsTotallyDisconnected.allRootsOfUnity : IsTotallyDisconnected allRootsOf apply IsCountable.isTotallyDisconnected simp only [_root_.allRootsOfUnity, setOf_exists]; apply countable_iUnion; intro n by_cases n0 : n = 0 - simp only [n0, Ne, eq_self_iff_true, not_true, false_and_iff, setOf_false, countable_empty] - simp only [Ne, n0, not_false_iff, true_and_iff] + simp only [n0, Ne, eq_self_iff_true, not_true, false_and, setOf_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 @@ -187,7 +187,7 @@ theorem eq_of_pow_eq {p q : X → ℂ} {t : Set X} {d : ℕ} (pc : ContinuousOn theorem MAnalyticAt.eventually_eq_or_eventually_ne [T2Space T] {f g : S → T} {z : S} (fa : MAnalyticAt I I f z) (ga : MAnalyticAt I I g z) : (∀ᶠ w in 𝓝 z, f w = g w) ∨ ∀ᶠ w in 𝓝[{z}ᶜ] z, f w ≠ g w := by - simp only [mAnalyticAt_iff_of_boundaryless, Function.comp] at fa ga + simp only [mAnalyticAt_iff_of_boundaryless, Function.comp_def] at fa ga rcases fa with ⟨fc, fa⟩; rcases ga with ⟨gc, ga⟩ by_cases fg : f z ≠ g z · right; contrapose fg; simp only [not_not] @@ -198,7 +198,7 @@ theorem MAnalyticAt.eventually_eq_or_eventually_ne [T2Space T] {f g : S → T} { · left; clear fa ga replace e := (continuousAt_extChartAt I z).eventually e replace e := Filter.EventuallyEq.fun_comp e (_root_.extChartAt I (f z)).symm - apply e.congr; simp only [Function.comp]; clear e + apply e.congr; simp only [Function.comp_def]; clear e apply (fc.eventually_mem (extChartAt_source_mem_nhds I (f z))).mp apply (gc.eventually_mem (extChartAt_source_mem_nhds I (g z))).mp refine eventually_nhds_iff.mpr ⟨(_root_.extChartAt I z).source, @@ -329,7 +329,7 @@ theorem nontrivialMAnalyticAt_id [AnalyticManifold I S] (z : S) : rw [← hu] exact (continuousOn_extChartAt_symm I z).isOpen_inter_preimage (isOpen_extChartAt_target _ _) ot have zu : extChartAt I z z ∈ u := by - simp only [mem_inter_iff, mem_extChartAt_target, true_and_iff, mem_preimage, + simp only [mem_inter_iff, mem_extChartAt_target, true_and, mem_preimage, PartialEquiv.left_inv _ (mem_extChartAt_source I z), zt, ← hu] rcases Metric.isOpen_iff.mp uo _ zu with ⟨r, rp, ru⟩ generalize ha : extChartAt I z z + r / 2 = a @@ -342,7 +342,7 @@ theorem nontrivialMAnalyticAt_id [AnalyticManifold I S] (z : S) : rw [← (PartialEquiv.injOn _).ne_iff ((extChartAt I z).map_target au.1) (mem_extChartAt_source I z)] rw [PartialEquiv.right_inv _ au.1, ← ha] simp only [Ne, add_right_eq_self, div_eq_zero_iff, Complex.ofReal_eq_zero, - one_ne_zero, or_false_iff, rp.ne', not_false_iff]; norm_num + one_ne_zero, or_false, rp.ne', not_false_iff]; norm_num /-- If `orderAt f z ≠ 0` (`f` has a zero of positive order), then `f` is nontrivial at `z` -/ theorem nontrivialMAnalyticAt_of_order {f : ℂ → ℂ} {z : ℂ} (fa : AnalyticAt ℂ f z) diff --git a/Ray/AnalyticManifold/OneDimension.lean b/Ray/AnalyticManifold/OneDimension.lean index 26e203b..481a4af 100644 --- a/Ray/AnalyticManifold/OneDimension.lean +++ b/Ray/AnalyticManifold/OneDimension.lean @@ -113,7 +113,7 @@ theorem mderiv_eq_zero_iff {z : S} {w : T} (f : TangentSpace I z →L[ℂ] Tange /-- 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} {u : TangentSpace I z} (u0 : u ≠ 0) : f u = 0 ↔ f = 0 := by - simp only [mderiv_eq_zero_iff, u0, or_false_iff] + simp only [mderiv_eq_zero_iff, u0, or_false] /-- Given nonzero `u`, a tangent space map `x` is `≠ 0` iff `x u ≠ 0` -/ theorem mderiv_ne_zero_iff {z : S} {w : T} (f : TangentSpace I z →L[ℂ] TangentSpace I w) @@ -232,7 +232,7 @@ theorem id_mderiv_ne_zero {z : S} : mfderiv I I (fun z ↦ z) z ≠ 0 := by refine .of_forall fun w m ↦ ?_ simp only [id, PartialEquiv.right_inv _ m] simp only [e.fderiv_eq, fderiv_id, Ne, ContinuousLinearMap.ext_iff, not_forall, - ContinuousLinearMap.zero_apply, ContinuousLinearMap.id_apply] + ContinuousLinearMap.zero_apply, ContinuousLinearMap.id_apply, Function.comp_def] use 1, one_ne_zero /-- Nonzeroness of `mfderiv` reduces to nonzeroness of `deriv` -/ @@ -310,13 +310,13 @@ theorem inChart_critical {f : ℂ → S → T} {c : ℂ} {z : S} apply ((isOpen_extChartAt_source II (c, z)).eventually_mem (mem_extChartAt_source _ _)).mp refine fa.eventually.mp (.of_forall ?_); intro ⟨e, w⟩ fa m fm simp only [extChartAt_prod, PartialEquiv.prod_source, extChartAt_eq_refl, PartialEquiv.refl_source, - mem_prod, mem_univ, true_and_iff] at m + mem_prod, mem_univ, true_and] at m simp only [uncurry] at fm have m' := PartialEquiv.map_source _ m simp only [← mfderiv_eq_zero_iff_deriv_eq_zero] have cd : MAnalyticAt I I (extChartAt I (f c z)) (f e w) := MAnalyticAt.extChartAt fm have fd : MAnalyticAt I I (f e ∘ (extChartAt I z).symm) (extChartAt I z w) := by - simp only [Function.comp] + simp only [Function.comp_def] exact MAnalyticAt.comp_of_eq fa.along_snd (MAnalyticAt.extChartAt_symm m') (PartialEquiv.right_inv _ m) have ce : inChart f c z e = extChartAt I (f c z) ∘ f e ∘ (extChartAt I z).symm := rfl diff --git a/Ray/AnalyticManifold/OpenMapping.lean b/Ray/AnalyticManifold/OpenMapping.lean index 9642612..194b8c0 100644 --- a/Ray/AnalyticManifold/OpenMapping.lean +++ b/Ray/AnalyticManifold/OpenMapping.lean @@ -67,15 +67,15 @@ theorem AnalyticOn.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 [← closedBall_prod_same, mem_prod_eq, setOf_mem_eq, iff_true_iff.mpr m, - true_and_iff, subset_refl] + simp only [← closedBall_prod_same, mem_prod_eq, setOf_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 rw [e]; apply DifferentiableOn.diffContOnCl; apply AnalyticOn.differentiableOn refine fa.comp (analyticOn_const.prod (analyticOn_id _)) ?_ intro w wr; simp only [closure_ball _ rp.ne'] at wr - simp only [← closedBall_prod_same, mem_prod_eq, du, wr, true_and_iff, du] + simp only [← closedBall_prod_same, mem_prod_eq, du, wr, true_and, du] rcases Metric.continuousAt_iff.mp (fa (c, z) (mk_mem_prod (mem_of_mem_nhds un) (mem_closedBall_self rp.le))).continuousAt (e / 4) (by linarith) with @@ -97,7 +97,7 @@ theorem AnalyticOn.ball_subset_image_closedBall_param {f : ℂ → ℂ → ℂ} specialize op d m.1.1 wm rcases (mem_image _ _ _).mp op with ⟨y, yr, yw⟩ use⟨d, y⟩ - simp only [mem_prod_eq, Prod.ext_iff, yw, and_true_iff, eq_self_iff_true, true_and_iff, yr, m.1.1] + simp only [mem_prod_eq, Prod.ext_iff, yw, and_true, eq_self_iff_true, true_and, yr, m.1.1] /-- A trivial lemma used repeatedly below -/ theorem abs_sub_self_lt {z : ℂ} {r : ℝ} (rp : 0 < r) : abs (z - z) < r := by @@ -215,7 +215,7 @@ theorem NontrivialMAnalyticAt.nhds_eq_map_nhds [AnalyticManifold I T] {f : S → simp only [← extChartAt_map_nhds' I z, Filter.map_map] at h replace h := @Filter.map_mono _ _ (extChartAt I (f z)).symm _ _ h simp only [← hg] at h; rw [PartialEquiv.left_inv _ (mem_extChartAt_source I z)] at h - simp only [extChartAt_symm_map_nhds' I (f z), Filter.map_map, Function.comp] at h + simp only [extChartAt_symm_map_nhds' I (f z), Filter.map_map, Function.comp_def] at h have e : (fun w ↦ (extChartAt I (f z)).symm (extChartAt I (f z) (f ((extChartAt I z).symm (extChartAt I z w))))) =ᶠ[𝓝 z] f := by apply ((isOpen_extChartAt_source I z).eventually_mem (mem_extChartAt_source I z)).mp diff --git a/Ray/AnalyticManifold/RiemannSphere.lean b/Ray/AnalyticManifold/RiemannSphere.lean index 04a0039..73c6dba 100644 --- a/Ray/AnalyticManifold/RiemannSphere.lean +++ b/Ray/AnalyticManifold/RiemannSphere.lean @@ -110,7 +110,7 @@ theorem inv_coe {z : ℂ} (z0 : z ≠ 0) : (z : 𝕊)⁻¹ = ↑(z : ℂ)⁻¹ : · simp only [inv_inf, eq_self_iff_true] · simp only [inv_def, inv, toComplex_coe] by_cases z0 : (z : 𝕊) = 0; simp only [if_pos, z0, inf_ne_zero, inf_ne_zero.symm] - simp only [if_neg z0, coe_ne_inf, iff_false_iff]; rw [coe_eq_zero, _root_.inv_eq_zero] + simp only [if_neg z0, coe_ne_inf, iff_false]; rw [coe_eq_zero, _root_.inv_eq_zero] simpa only [coe_eq_zero] using z0 theorem toComplex_inv {z : 𝕊} : z⁻¹.toComplex = z.toComplex⁻¹ := by induction' z using OnePoint.rec with z @@ -145,7 +145,7 @@ theorem continuous_inv : Continuous fun z : 𝕊 ↦ z⁻¹ := by simp only [gt_iff_lt, Complex.norm_eq_abs, AbsoluteValue.pos_iff] at z0; rw [inv_coe z0] apply Filter.Tendsto.congr' e exact Filter.Tendsto.comp continuous_coe.continuousAt inv_tendsto_atInf' - · simp only [OnePoint.continuousAt_coe, Function.comp, inv_def, inv, WithTop.coe_eq_zero, + · simp only [OnePoint.continuousAt_coe, Function.comp_def, inv_def, inv, WithTop.coe_eq_zero, toComplex_coe] by_cases z0 : z = 0 · simp only [z0, ContinuousAt, OnePoint.nhds_infty_eq, eq_self_iff_true, if_true, @@ -154,7 +154,9 @@ theorem continuous_inv : Continuous fun z : 𝕊 ↦ z⁻¹ := by constructor · refine Filter.Tendsto.mono_right ?_ le_sup_left apply tendsto_nhdsWithin_congr (f := fun z : ℂ ↦ (↑z⁻¹ : 𝕊)) - · intro z m; rw [mem_compl_singleton_iff] at m; simp only [coe_eq_zero, m, ite_false] + · intro z m + rw [mem_compl_singleton_iff] at m + simp only [coe_eq_zero, m, ite_false] · simp only [coe_zero, ite_true]; apply coe_tendsto_inf'.comp rw [← @tendsto_atInf_iff_tendsto_nhds_zero ℂ ℂ _ _ fun z : ℂ ↦ z] exact Filter.tendsto_id @@ -244,8 +246,8 @@ instance : ChartedSpace ℂ 𝕊 where not_false_eq_true] chart_mem_atlas := by intro z; induction z using OnePoint.rec - · simp only [rec_inf, eq_self_iff_true, mem_setOf_eq, or_true_iff] - · simp only [rec_coe, mem_setOf_eq, eq_self_iff_true, true_or_iff] + · simp only [rec_inf, eq_self_iff_true, mem_setOf_eq, or_true] + · simp only [rec_coe, mem_setOf_eq, eq_self_iff_true, true_or] /-- There are just two charts on `𝕊` -/ theorem two_charts {e : PartialHomeomorph 𝕊 ℂ} (m : e ∈ atlas ℂ 𝕊) : @@ -307,10 +309,10 @@ instance : HasGroupoid 𝕊 (analyticGroupoid I) where · cases' two_charts ga with gh gh · simp only [←fh, gh]; constructor; repeat apply extChartAt_self_analytic · simp [fh, gh, invCoePartialHomeomorph, coePartialHomeomorph, coePartialEquiv, invHomeomorph, - invEquiv, Function.comp, e0, e1, and_self, a] + invEquiv, Function.comp_def, e0, e1, and_self, a] · cases' two_charts ga with gh gh · simp [fh, gh, invCoePartialHomeomorph, coePartialHomeomorph, coePartialEquiv, invHomeomorph, - invEquiv, Function.comp, e0, e1, and_self, a] + invEquiv, Function.comp_def, e0, e1, and_self, a] · simp only [←fh, gh]; constructor; repeat apply extChartAt_self_analytic /-- `𝕊` is an analytic manifold -/ @@ -337,7 +339,7 @@ theorem isOpenMap_coe : IsOpenMap (fun z : ℂ ↦ (z : 𝕊)) := by apply Set.ext; intro z simp only [mem_image, mem_inter_iff, mem_compl_singleton_iff, mem_preimage] constructor - intro ⟨x, m, e⟩; simp only [← e, toComplex_coe, m, and_true_iff]; exact inf_ne_coe.symm + intro ⟨x, m, e⟩; simp only [← e, toComplex_coe, m, and_true]; exact inf_ne_coe.symm intro ⟨n, m⟩; use z.toComplex, m, coe_toComplex n rw [e]; exact continuousOn_toComplex.isOpen_inter_preimage isOpen_compl_singleton o @@ -359,11 +361,11 @@ theorem prod_mem_inf_of_mem_atInf {s : Set (X × ℂ)} {x : X} (f : s ∈ (𝓝 refine Filter.mem_prod_iff.mpr ⟨t, tx, (fun z : ℂ ↦ (z : 𝕊)) '' u ∪ {∞}, mem_inf_of_mem_atInf ui, ?_⟩ intro ⟨y, z⟩ ⟨yt, m⟩ - simp only [mem_prod_eq, mem_image, mem_union, mem_singleton_iff, mem_univ, true_and_iff, + simp only [mem_prod_eq, mem_image, mem_union, mem_singleton_iff, mem_univ, true_and, Prod.ext_iff] at yt m ⊢ induction' z using OnePoint.rec with z - · simp only [eq_self_iff_true, or_true_iff] - · simp only [coe_eq_inf_iff, or_false_iff, coe_eq_coe] at m ⊢ + · simp only [eq_self_iff_true, or_true] + · simp only [coe_eq_inf_iff, or_false, coe_eq_coe] at m ⊢ rcases m with ⟨w, wu, wz⟩; refine ⟨⟨y, z⟩, sub (mk_mem_prod yt ?_), rfl, rfl⟩; rw [← wz] exact wu @@ -390,12 +392,12 @@ theorem mAnalytic_inv : MAnalytic I I fun z : 𝕊 ↦ z⁻¹ := by use continuous_inv intro z induction' z using OnePoint.rec with z - · simp only [inv_inf, extChartAt_inf, ← coe_zero, extChartAt_coe, Function.comp, + · simp only [inv_inf, extChartAt_inf, ← coe_zero, extChartAt_coe, Function.comp_def, PartialEquiv.trans_apply, Equiv.toPartialEquiv_apply, invEquiv_apply, coePartialEquiv_symm_apply, toComplex_coe, PartialEquiv.coe_trans_symm, PartialEquiv.symm_symm, coePartialEquiv_apply, Equiv.toPartialEquiv_symm_apply, invEquiv_symm, inv_inv] apply analyticAt_id - · simp only [extChartAt_coe, PartialEquiv.symm_symm, Function.comp, coePartialEquiv_apply, + · simp only [extChartAt_coe, PartialEquiv.symm_symm, Function.comp_def, coePartialEquiv_apply, coePartialEquiv_symm_apply, toComplex_coe] by_cases z0 : z = 0 · simp only [z0, coe_zero, extChartAt_inf, PartialEquiv.trans_apply, coePartialEquiv_symm_apply, @@ -441,13 +443,13 @@ theorem lift_eq_fill : lift f y = fill (fun z ↦ (f z : 𝕊)) y := rfl /-- `fill` is continuous at finite values -/ theorem continuousAt_fill_coe {f : ℂ → X} {y : X} (fc : ContinuousAt f z) : ContinuousAt (fill f y) z := by - simp only [OnePoint.continuousAt_coe, Function.comp, fill_coe, fc] + simp only [OnePoint.continuousAt_coe, Function.comp_def, fill_coe, fc] /-- `fill` is continuous at `∞` -/ theorem continuousAt_fill_inf {f : ℂ → X} {y : X} (fi : Tendsto f atInf (𝓝 y)) : ContinuousAt (fill f y) ∞ := by simp only [OnePoint.continuousAt_infty', lift_inf, Filter.coclosedCompact_eq_cocompact, ← - atInf_eq_cocompact, Function.comp, fill_coe, fill_inf, fi] + atInf_eq_cocompact, Function.comp_def, fill_coe, fill_inf, fi] /-- `fill` is continuous -/ theorem continuous_fill {f : ℂ → X} {y : X} (fc : Continuous f) (fi : Tendsto f atInf (𝓝 y)) : @@ -472,7 +474,7 @@ theorem mAnalyticAt_fill_inf [AnalyticManifold I T] {f : ℂ → T} {y : T} MAnalyticAt I I (fill f y) ∞ := by rw [mAnalyticAt_iff_of_boundaryless] use continuousAt_fill_inf fi - simp only [Function.comp, extChartAt, PartialHomeomorph.extend, fill, rec_inf, + simp only [Function.comp_def, extChartAt, PartialHomeomorph.extend, fill, rec_inf, modelWithCornersSelf_partialEquiv, PartialEquiv.trans_refl, chartAt_inf, PartialHomeomorph.symm_toPartialEquiv, PartialEquiv.symm_symm, PartialHomeomorph.toFun_eq_coe, invCoePartialHomeomorph_apply, PartialHomeomorph.coe_coe_symm, invCoePartialHomeomorph_symm_apply, @@ -520,7 +522,7 @@ theorem mAnalytic_fill [AnalyticManifold I T] {f : ℂ → T} {y : T} (fa : MAna theorem continuousAt_lift_coe' (gc : ContinuousAt (uncurry g) (x, z)) : ContinuousAt (uncurry (lift' g y)) (x, ↑z) := by simp only [lift', ContinuousAt, uncurry, rec_coe, OnePoint.nhds_coe_eq, prod_nhds_eq, - Filter.tendsto_map'_iff, Function.comp] + Filter.tendsto_map'_iff, Function.comp_def] exact Filter.Tendsto.comp Filter.tendsto_map gc /-- `lift'` is continuous at `∞` -/ @@ -535,8 +537,8 @@ theorem continuousAt_lift_inf' (gi : Tendsto (uncurry g) ((𝓝 x).prod atInf) a (fun x : X × ℂ ↦ (x.1, (x.2 : 𝕊))) '' ((fun x : X × ℂ ↦ (g x.1 x.2 : 𝕊)) ⁻¹' s) ∪ univ ×ˢ {∞} := by apply Set.ext; intro ⟨x, z⟩; induction z using OnePoint.rec - · simp only [mem_preimage, mem_image, mem_union, mem_prod_eq, mem_univ, true_and_iff, - mem_singleton_iff, eq_self_iff_true, or_true_iff, iff_true_iff, uncurry, lift', rec_inf, + · simp only [mem_preimage, mem_image, mem_union, mem_prod_eq, mem_univ, true_and, + mem_singleton_iff, eq_self_iff_true, or_true, iff_true, uncurry, lift', rec_inf, m.2] · simp only [uncurry, lift', mem_preimage, rec_coe, prod_singleton, image_univ, mem_union, mem_image, Prod.ext_iff, coe_eq_coe, Prod.exists, exists_eq_right_right, exists_eq_right, diff --git a/Ray/AnalyticManifold/SmoothManifoldWithCorners.lean b/Ray/AnalyticManifold/SmoothManifoldWithCorners.lean index ee60f45..87e4d1d 100644 --- a/Ray/AnalyticManifold/SmoothManifoldWithCorners.lean +++ b/Ray/AnalyticManifold/SmoothManifoldWithCorners.lean @@ -102,7 +102,7 @@ theorem AnalyticManifold.punctured_nhds_neBot (I : ModelWithCorners 𝕜 E A) [I [Nontrivial E] (x : M) : (𝓝[{x}ᶜ] x).NeBot := by have p := Module.punctured_nhds_neBot 𝕜 E (extChartAt I x x) simp only [← Filter.frequently_true_iff_neBot, frequently_nhdsWithin_iff, ← - extChartAt_symm_map_nhds' I x, Filter.frequently_map, true_and_iff, + extChartAt_symm_map_nhds' I x, Filter.frequently_map, true_and, mem_compl_singleton_iff] at p ⊢ apply p.mp apply ((isOpen_extChartAt_target I x).eventually_mem (mem_extChartAt_target I x)).mp diff --git a/Ray/Dynamics/BottcherNear.lean b/Ray/Dynamics/BottcherNear.lean index a42bc58..d6e0164 100644 --- a/Ray/Dynamics/BottcherNear.lean +++ b/Ray/Dynamics/BottcherNear.lean @@ -601,11 +601,11 @@ theorem SuperAtC.superNearC' (s : SuperAtC f d u) {w : Set (ℂ × ℂ)} (wo : I intro p m; simp only [← ball_prod_same, Set.mem_prod] at m exact Metric.ball_subset_ball (by linarith) m.1 s := by - intro c' m; simp only [← ball_prod_same, Set.mem_prod, m, true_and_iff] + intro c' m; simp only [← ball_prod_same, Set.mem_prod, m, true_and] apply (s.s (rc m)).super_on_ball rp rh · apply fa.comp₂ analyticOn_const (analyticOn_id _) intro z zm; apply Metric.ball_subset_ball (by bound : r ≤ r2) - simp only [← ball_prod_same, Set.mem_prod, m, true_and_iff]; exact zm + simp only [← ball_prod_same, Set.mem_prod, m, true_and]; exact zm · simp only [Complex.dist_eq, Prod.dist_eq, sub_zero, max_lt_iff, and_imp, g2, g0] at gs simp only [Metric.mem_ball, Complex.dist_eq] at m intro z zr; exact @gs ⟨c', z⟩ (lt_of_lt_of_le m rr4) (lt_of_lt_of_le zr rr4) diff --git a/Ray/Dynamics/BottcherNearM.lean b/Ray/Dynamics/BottcherNearM.lean index ddb1866..1716da6 100644 --- a/Ray/Dynamics/BottcherNearM.lean +++ b/Ray/Dynamics/BottcherNearM.lean @@ -176,7 +176,7 @@ theorem Super.critical_a (s : Super f d a) (c : ℂ) : Critical (f c) a := by have h := s.critical_0 c have e := PartialEquiv.left_inv _ (mem_extChartAt_source I a) contrapose h; simp only [Critical, Super.fl, fl, ← ne_eq] at h ⊢ - simp only [mfderiv_eq_fderiv, _root_.fl, Function.comp] + simp only [mfderiv_eq_fderiv, _root_.fl, Function.comp_def] rw [fderiv_sub_const, ←mfderiv_eq_fderiv] apply mderiv_comp_ne_zero' (extChartAt_mderiv_ne_zero' ?_) · apply mderiv_comp_ne_zero' (f := f c) @@ -195,13 +195,13 @@ theorem Super.f_nontrivial (s : Super f d a) (c : ℂ) : NontrivialMAnalyticAt ( · simp only [s.fl0, uncurry] at e; exact e · simp only [Super.fl, s.fd, uncurry]; exact s.d0 contrapose n - simp only [Filter.not_frequently, not_not, Super.fl, fl, Function.comp, sub_eq_zero] at n ⊢ + simp only [Filter.not_frequently, not_not, Super.fl, fl, Function.comp_def, sub_eq_zero] at n ⊢ have gc : ContinuousAt (fun x ↦ (extChartAt I a).symm (x + extChartAt I a a)) 0 := by refine (continuousAt_extChartAt_symm I a).comp_of_eq ?_ (by simp only [zero_add]) exact continuousAt_id.add continuousAt_const simp only [ContinuousAt, zero_add, PartialEquiv.left_inv _ (mem_extChartAt_source _ _)] at gc refine (gc.eventually n).mp (.of_forall ?_) - intro x h; simp only [_root_.fl, Function.comp, h, sub_self] + intro x h; simp only [_root_.fl, Function.comp_def, h, sub_self] /-- Close enough to `a`, `f c z ∈ (ext_chart_at I a).source` -/ theorem Super.stays_in_chart (s : Super f d a) (c : ℂ) : @@ -302,7 +302,7 @@ theorem Super.isOpen_near (s : Super f d a) : IsOpen s.near := by /-- `(c,a)` is near -/ 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_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] exact (s.superNearC.s (Set.mem_univ _)).t0 @@ -324,7 +324,7 @@ theorem Super.mem_near_to_near' (s : Super f d a) {p : ℂ × S} (m : p ∈ s.ne theorem Super.stays_near (s : Super f d a) {c : ℂ} {z : S} (m : (c, z) ∈ s.near) : (c, f c z) ∈ 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_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] at m ⊢ rcases mem_iUnion.mp (s.near_subset' m.2) with ⟨b, mb⟩ @@ -334,22 +334,23 @@ theorem Super.stays_near (s : Super f d a) {c : ℂ} {z : S} (m : (c, z) ∈ s.n · apply s.fr_stays b (c, z) simp only [m.1, 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_iff, Set.mem_preimage, PartialEquiv.prod_coe, PartialEquiv.refl_coe, id, + Set.mem_univ, true_and, Set.mem_preimage, PartialEquiv.prod_coe, PartialEquiv.refl_coe, id, Set.mem_setOf_eq, sub_self] simp only [m.1, mb.1, mb.2, 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_iff, Set.mem_preimage, PartialEquiv.prod_coe, PartialEquiv.refl_coe, id, + Set.mem_univ, true_and, Set.mem_preimage, PartialEquiv.prod_coe, PartialEquiv.refl_coe, id, Set.mem_setOf_eq, sub_self, mem_ball_iff_norm, Prod.norm_def, max_lt_iff, Prod.fst_sub, Prod.snd_sub, sub_zero] · have h := (s.superNearC.s (Set.mem_univ c)).ft m.2 - simp only [Super.fl, _root_.fl, Function.comp, sub_add_cancel, PartialEquiv.left_inv _ m.1] at h + simp only [Super.fl, _root_.fl, Function.comp_def, sub_add_cancel, + PartialEquiv.left_inv _ m.1] at h exact h /-- Once we're in `s.near`, we stay there forever -/ theorem Super.iter_stays_near (s : Super f d a) {c : ℂ} {z : S} (m : (c, z) ∈ s.near) (n : ℕ) : (c, (f c)^[n] z) ∈ s.near := by induction' n with n h; simp only [Function.iterate_zero, id, m] - simp only [Nat.add_succ, Function.iterate_succ', s.stays_near h, Function.comp] + simp only [Nat.add_succ, Function.iterate_succ', s.stays_near h, Function.comp_def] /-- More iterations stay in `s.near` -/ theorem Super.iter_stays_near' (s : Super f d a) {a b : ℕ} (m : (c, (f c)^[a] z) ∈ s.near) @@ -377,7 +378,7 @@ theorem Super.attracts (s : Super f d a) {n : ℕ} (r : (c, (f c)^[n] z) ∈ s.n have g0 : g 0 = a := by simp only [← hg]; simp only [zero_add]; exact PartialEquiv.left_inv _ (mem_extChartAt_source _ _) have h := gc.tendsto.comp t; clear t gc m - simp only [Function.comp, g0] at h + simp only [Function.comp_def, g0] at h rw [← attracts_shift n] refine Filter.Tendsto.congr ?_ h; clear h intro k; simp only [← hg]; induction' k with k h @@ -385,7 +386,7 @@ theorem Super.attracts (s : Super f d a) {n : ℕ} (r : (c, (f c)^[n] z) ∈ s.n exact PartialEquiv.left_inv _ (s.near_subset_chart r) simp only [Function.iterate_succ_apply'] generalize hx : (s.fl c)^[k] (extChartAt I a ((f c)^[n] z) - extChartAt I a a) = x; rw [hx] at h - simp only [Super.fl, _root_.fl, Function.comp, sub_add_cancel, h, + simp only [Super.fl, _root_.fl, Function.comp_def, sub_add_cancel, h, ←Function.iterate_succ_apply' (f c)] apply PartialEquiv.left_inv _ (s.near_subset_chart (s.iter_stays_near r _)) @@ -483,7 +484,7 @@ theorem Super.bottcherNear_eqn (s : Super f d a) (m : (c, z) ∈ s.near) : simp only [Super.bottcherNear] have e : extChartAt I a (f c z) - extChartAt I a a = s.fl c (extChartAt I a z - extChartAt I a a) := by - simp only [Function.comp, Super.fl, _root_.fl, sub_add_cancel, + simp only [Function.comp_def, Super.fl, _root_.fl, sub_add_cancel, PartialEquiv.left_inv _ (s.near_subset_chart m)] rw [e, _root_.bottcherNear_eqn (s.superNearC.s (Set.mem_univ c)) (s.mem_near_to_near' m)] @@ -568,7 +569,7 @@ theorem Super.f_noncritical_near_a (s : Super f d a) (c : ℂ) : clear m0 d0 generalize hg : (fun w ↦ extChartAt I (f c a) (f e ((extChartAt I a).symm w))) = g have hg' : extChartAt I a ∘ f e ∘ (extChartAt I a).symm = g := by - rw [← hg]; simp only [Function.comp, s.f0] + rw [← hg]; simp only [Function.comp_def, s.f0] rw [_root_.fl, hg']; clear hg'; rw [Iff.comm] have dg : DifferentiableAt ℂ g (extChartAt I a z) := by rw [← hg]; apply AnalyticAt.differentiableAt; apply MAnalyticAt.analyticAt I I @@ -584,7 +585,8 @@ theorem Super.f_noncritical_near_a (s : Super f d a) (c : ℂ) : exact differentiableAt_id.add (differentiableAt_const _) simp only [deriv.comp _ (d0 _) d1, deriv_sub_const, deriv_id'', one_mul] rw [deriv.comp _ _ _] - · simp only [deriv_add_const, deriv_sub_const, deriv_id'', mul_one, sub_add_cancel, Function.comp] + · simp only [deriv_add_const, deriv_sub_const, deriv_id'', mul_one, sub_add_cancel, + Function.comp_def] · simp only [sub_add_cancel, dg] · exact differentiableAt_id.add (differentiableAt_const _) diff --git a/Ray/Dynamics/Grow.lean b/Ray/Dynamics/Grow.lean index 600782d..9f48193 100644 --- a/Ray/Dynamics/Grow.lean +++ b/Ray/Dynamics/Grow.lean @@ -111,7 +111,7 @@ theorem mem_domain (c : ℂ) {p : ℝ} (p0 : 0 ≤ p) : theorem mem_domain_self {c x : ℂ} : (c, x) ∈ ({c} ×ˢ closedBall 0 (Complex.abs x) : Set (ℂ × ℂ)) := by simp only [mem_prod_eq, mem_singleton_iff, eq_self_iff_true, mem_closedBall, Complex.dist_eq, - sub_zero, true_and_iff, le_refl] + sub_zero, true_and, le_refl] /-- Our domain is preconnected -/ theorem domain_preconnected (c : ℂ) (p : ℝ) : @@ -194,7 +194,7 @@ theorem eqn_noncritical {x : ℂ × ℂ} (e : ∀ᶠ y in 𝓝 x, Eqn s n r y) ( rw [x0] at d replace d := Eq.trans d (ContinuousLinearMap.zero_apply _) rw [deriv_pow, mul_eq_zero, Nat.cast_eq_zero, pow_eq_zero_iff', pow_eq_zero_iff'] at d - simp only [s.d0, false_and_iff, false_or_iff] at d; exact d.1 + simp only [s.d0, false_and, false_or] at d; exact d.1 /-- `p < 1` for any `p` in `Grow` -/ theorem Grow.p1 (g : Grow s c p n r) : p < 1 := by @@ -204,7 +204,7 @@ theorem Grow.p1 (g : Grow s c p n r) : p < 1 := by rw [e.potential, Complex.abs.map_one, lt_self_iff_false] at lt exact lt · simp only [p1, singleton_prod, mem_image, mem_closedBall_zero_iff, Complex.norm_eq_abs, - Prod.mk.inj_iff, eq_self_iff_true, true_and_iff, exists_eq_right, Complex.abs.map_one] + Prod.mk.inj_iff, eq_self_iff_true, true_and, exists_eq_right, Complex.abs.map_one] /-- `r` is analytic throughout the domain -/ theorem Grow.holo (g : Grow s c p n r) : MAnalyticOn II I (uncurry r) ({c} ×ˢ closedBall 0 p) := @@ -327,7 +327,7 @@ theorem GrowOpen.point (g : GrowOpen s c p r) [OnePreimage s] {x : ℂ} (ax : ab ∃ᶠ y in 𝓝 x, y ∈ ball (0 : ℂ) p ∧ r' c y = r c y := by -- If z = a, we can use r by_cases za : abs x = 0 - · use r; simp only [Complex.abs.eq_zero] at za; simp only [za, eq_self_iff_true, and_true_iff] + · use r; simp only [Complex.abs.eq_zero] at za; simp only [za, eq_self_iff_true, and_true] constructor refine g.eqn.filter_mono (nhds_le_nhdsSet ?_); exact mk_mem_prod rfl (mem_ball_self g.pos) exact (isOpen_ball.eventually_mem (mem_ball_self g.pos)).frequently @@ -465,9 +465,9 @@ theorem GrowOpen.grow (g : GrowOpen s c p r) [OnePreimage s] : ∃ r', Grow s c { eqn := e start := fun h ↦ (y0 h).elim } · refine ct.frequently (rr.mp (.of_forall ?_)); intro x ⟨m, e⟩ - simp only [mem_prod_eq, mem_singleton_iff, eq_self_iff_true, true_and_iff]; use m, e + simp only [mem_prod_eq, mem_singleton_iff, eq_self_iff_true, true_and]; use m, e · use uncurry r; simp only [not_not] at x0 - simp only [m.1, x0, eq_self_iff_true, and_true_iff] at ct ⊢; constructor + simp only [m.1, x0, eq_self_iff_true, and_true] at ct ⊢; constructor · refine (g.eqn.filter_mono (nhds_le_nhdsSet ?_)).eventually_nhds.mp (.of_forall fun y e ↦ ?_) @@ -477,7 +477,7 @@ theorem GrowOpen.grow (g : GrowOpen s c p r) [OnePreimage s] : ∃ r', Grow s c start := by simp only [Filter.EventuallyEq.refl, imp_true_iff, Filter.eventually_true] } · refine ct.frequently (Filter.Eventually.frequently ?_) - simp only [mem_prod_eq, mem_singleton_iff, eq_self_iff_true, true_and_iff] + simp only [mem_prod_eq, mem_singleton_iff, eq_self_iff_true, true_and] exact isOpen_ball.eventually_mem (mem_ball_self g.pos) unique := by intro r0 r1 t _ pre e0 e1 r01 @@ -485,7 +485,7 @@ theorem GrowOpen.grow (g : GrowOpen s c p r) [OnePreimage s] : ∃ r', Grow s c simp only [Function.uncurry_curry] at u; exact u simp only [Function.uncurry_curry]; exact r01 } have m0 : (c, (0 : ℂ)) ∈ ({c} ×ˢ ball 0 p : Set (ℂ × ℂ)) := by - simp only [mem_prod_eq, mem_singleton_iff, eq_self_iff_true, true_and_iff, mem_ball_self g.pos] + simp only [mem_prod_eq, mem_singleton_iff, eq_self_iff_true, true_and, mem_ball_self g.pos] use curry b.u exact { nonneg := g.pos.le @@ -562,11 +562,11 @@ theorem joined_growOpen (s : Super f d a) {p : ℕ → ℝ} {ps : ℝ} {r : ℕ eqn := by apply mem_nhdsSet_iff_forall.mpr; intro ⟨c', x⟩ lt simp only [mem_prod_eq, mem_singleton_iff, mem_ball, Complex.dist_eq, sub_zero] at lt - simp only [lt.1, eq_self_iff_true, true_and_iff, ← Filter.eventually_iff] at lt ⊢; clear c' + simp only [lt.1, eq_self_iff_true, true_and, ← Filter.eventually_iff] at lt ⊢; clear c' rcases tend.exists_lt lt with ⟨k, ltp⟩ have m : (c, x) ∈ {c} ×ˢ closedBall (0 : ℂ) (p k) := by simp only [mem_prod_eq, mem_singleton_iff, Metric.mem_closedBall, eq_self_iff_true, - true_and_iff, Complex.dist_eq, sub_zero, ltp.le] + true_and, Complex.dist_eq, sub_zero, ltp.le] have lt' : ∀ᶠ y : ℂ × ℂ in 𝓝 (c, x), abs y.2 < ps := (Complex.continuous_abs.continuousAt.comp continuousAt_snd).eventually_lt continuousAt_const lt diff --git a/Ray/Dynamics/Multibrot/Basic.lean b/Ray/Dynamics/Multibrot/Basic.lean index 76e6fb0..cc1c3cd 100644 --- a/Ray/Dynamics/Multibrot/Basic.lean +++ b/Ray/Dynamics/Multibrot/Basic.lean @@ -75,7 +75,7 @@ def multibrotExt (d : ℕ) : Set 𝕊 := theorem multibrotExt_inf {d : ℕ} : ∞ ∈ multibrotExt d := subset_union_right rfl theorem multibrotExt_coe {d : ℕ} {c : ℂ} : ↑c ∈ multibrotExt d ↔ c ∉ multibrot d := by - simp only [multibrotExt, mem_union, mem_singleton_iff, coe_eq_inf_iff, or_false_iff, mem_image, + simp only [multibrotExt, mem_union, mem_singleton_iff, coe_eq_inf_iff, or_false, mem_image, mem_compl_iff, coe_eq_coe, not_iff_not] constructor; intro ⟨x, m, e⟩; rw [e] at m; exact m; intro m; use c, m theorem coe_preimage_multibrotExt {d : ℕ} : @@ -130,12 +130,12 @@ theorem mAnalyticAt_f : MAnalytic II I (uncurry (f d)) := theorem writtenInExtChartAt_coe_f {d : ℕ} {z : ℂ} : writtenInExtChartAt I I (z : 𝕊) (f d c) = f' d c := by - simp only [writtenInExtChartAt, f, Function.comp, lift_coe', RiemannSphere.extChartAt_coe, + simp only [writtenInExtChartAt, f, Function.comp_def, lift_coe', RiemannSphere.extChartAt_coe, PartialEquiv.symm_symm, coePartialEquiv_apply, coePartialEquiv_symm_apply, toComplex_coe] theorem fl_f : fl (f d) ∞ = fun c z : ℂ ↦ z^d / (1 + c * z^d) := by funext c z - simp only [fl, RiemannSphere.extChartAt_inf, Function.comp, invEquiv_apply, + simp only [fl, RiemannSphere.extChartAt_inf, Function.comp_def, invEquiv_apply, PartialEquiv.trans_apply, Equiv.toPartialEquiv_apply, PartialEquiv.coe_trans_symm, coePartialEquiv_symm_apply, PartialEquiv.symm_symm, coePartialEquiv_apply, Equiv.toPartialEquiv_symm_apply, invEquiv_symm, RiemannSphere.inv_inf, toComplex_zero, @@ -212,7 +212,7 @@ theorem superNearF (d : ℕ) [Fact (2 ≤ d)] (c : ℂ) : simp only [Complex.abs.map_mul, Complex.abs.map_pow] trans abs c * (max 16 (abs c / 2))⁻¹ ^ d; bound rw [inv_pow, mul_inv_le_iff]; swap; bound - rw [mul_one_div]; rw [le_div_iff, mul_comm]; swap; norm_num + rw [mul_one_div]; rw [le_div_iff₀, mul_comm]; swap; norm_num refine le_trans ?_ (pow_le_pow_right (le_max_of_le_left (by norm_num)) (two_le_d d)) by_cases cb : abs c / 2 ≤ 16 rw [max_eq_left cb, pow_two]; linarith @@ -242,7 +242,7 @@ theorem superNearF (d : ℕ) [Fact (2 ≤ d)] (c : ℂ) : ft := by intro z m; specialize cz1 m; specialize zb m simp only [fl_f, mem_setOf, map_div₀, Complex.abs.map_pow, ← ht] at m ⊢ - refine lt_of_le_of_lt ?_ m; rw [div_le_iff (lt_of_lt_of_le (by norm_num) cz1)] + refine lt_of_le_of_lt ?_ m; rw [div_le_iff₀ (lt_of_lt_of_le (by norm_num) cz1)] refine le_trans (pow_le_pow_of_le_one (Complex.abs.nonneg _) (le_trans zb (by norm_num)) (two_le_d d)) ?_ rw [pow_two]; refine mul_le_mul_of_nonneg_left ?_ (Complex.abs.nonneg _) @@ -273,13 +273,13 @@ theorem critical_f {z : 𝕊} : Critical (f d c) z ↔ z = 0 ∨ z = ∞ := by simp only [Critical, mfderiv, (mAnalyticAt_f (c, z)).along_snd.mdifferentiableAt, if_pos, ModelWithCorners.Boundaryless.range_eq_univ, fderivWithin_univ, writtenInExtChartAt_coe_f, RiemannSphere.extChartAt_coe, coePartialEquiv_symm_apply, toComplex_coe, coe_eq_zero, - coe_eq_inf_iff, or_false_iff, ← deriv_fderiv, deriv_f', ContinuousLinearMap.ext_iff, + coe_eq_inf_iff, or_false, ← deriv_fderiv, deriv_f', ContinuousLinearMap.ext_iff, ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply, Algebra.id.smul_eq_mul, - one_mul, mul_eq_zero, Nat.cast_eq_zero, d_ne_zero, false_or_iff, + one_mul, mul_eq_zero, Nat.cast_eq_zero, d_ne_zero, false_or, pow_eq_zero_iff (d_minus_one_pos d).ne', zx] constructor · intro h; specialize h 1 - simp only [one_mul, mul_eq_zero, one_ne_zero, false_or_iff] at h + simp only [one_mul, mul_eq_zero, one_ne_zero, false_or] at h exact h · exact fun h x ↦ Or.inr h @@ -533,7 +533,7 @@ theorem bottcher_bound {c : ℂ} (lo : 16 < abs c) : abs (bottcher' d c) ≤ 3 * generalize hz : g^[n] c⁻¹ = z simp only [← hg, fl, extChartAt_inf, PartialEquiv.trans_apply, Equiv.toPartialEquiv_apply, invEquiv_apply, RiemannSphere.inv_inf, coePartialEquiv_symm_apply, toComplex_zero, sub_zero, - Function.comp, add_zero, PartialEquiv.coe_trans_symm, PartialEquiv.symm_symm, + Function.comp_def, add_zero, PartialEquiv.coe_trans_symm, PartialEquiv.symm_symm, coePartialEquiv_apply, Equiv.toPartialEquiv_symm_apply, invEquiv_symm] rw [coe_toComplex] simp only [Ne, inv_eq_inf, ← hz, ← h, inv_inv, ← Function.iterate_succ_apply' (f d c)] @@ -561,7 +561,7 @@ theorem bottcher_bound {c : ℂ} (lo : 16 < abs c) : abs (bottcher' d c) ≤ 3 * theorem bottcher_tendsto_zero : Tendsto (bottcher' d) atInf (𝓝 0) := by rw [Metric.tendsto_nhds]; intro r rp; rw [atInf_basis.eventually_iff] use max 16 (3 / r) - simp only [true_and_iff, mem_setOf, Complex.dist_eq, sub_zero, Complex.norm_eq_abs, max_lt_iff] + simp only [true_and, mem_setOf, Complex.dist_eq, sub_zero, Complex.norm_eq_abs, max_lt_iff] intro z ⟨lo, rz⟩; apply lt_of_le_of_lt (bottcher_bound lo) rw [div_lt_iff rp] at rz; rw [map_inv₀, mul_inv_lt_iff (lt_trans (by norm_num) lo)]; exact rz @@ -577,7 +577,7 @@ theorem bottcherMAnalytic (d : ℕ) [Fact (2 ≤ d)] : intro c m; induction c using OnePoint.rec · refine mAnalyticAt_fill_inf ?_ bottcher_tendsto_zero rw [atInf_basis.eventually_iff]; use 2 - simp only [true_and_iff, mem_setOf, Complex.norm_eq_abs] + simp only [true_and, mem_setOf, Complex.norm_eq_abs] 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) @@ -686,7 +686,7 @@ theorem bottcher_surj (d : ℕ) [Fact (2 ≤ d)] : bottcher d '' multibrotExt d · refine _root_.trans ?_ interior_subset refine IsPreconnected.relative_clopen (convex_ball _ _).isPreconnected ?_ ?_ ?_ · use 0, mem_ball_self one_pos, ∞ - simp only [multibrotExt_inf, bottcher, fill_inf, true_and_iff] + simp only [multibrotExt_inf, bottcher, fill_inf, true_and] · -- Relative openness rw [IsOpen.interior_eq]; exact inter_subset_right rw [isOpen_iff_eventually]; intro z ⟨c, m, e⟩ @@ -729,7 +729,7 @@ theorem bottcher_large_approx (d : ℕ) [Fact (2 ≤ d)] (c : ℂ) : simp only [hasDerivAt_iff_tendsto, sub_zero, bottcherNear_zero, smul_eq_mul, mul_one, Metric.tendsto_nhds_nhds, Real.dist_eq, Complex.norm_eq_abs, Complex.dist_eq, abs_mul, abs_of_nonneg (Complex.abs.nonneg _), abs_inv] at m - simp only [Metric.tendsto_nhds, atInf_basis.eventually_iff, true_and_iff, mem_setOf, + simp only [Metric.tendsto_nhds, atInf_basis.eventually_iff, true_and, mem_setOf, Complex.dist_eq, Complex.norm_eq_abs] intro e ep; rcases m e ep with ⟨r, rp, h⟩; use 1 / r; intro z zr have az0 : abs z ≠ 0 := (lt_trans (one_div_pos.mpr rp) zr).ne' diff --git a/Ray/Dynamics/Multibrot/Bottcher.lean b/Ray/Dynamics/Multibrot/Bottcher.lean index 3d564c0..74e9bce 100644 --- a/Ray/Dynamics/Multibrot/Bottcher.lean +++ b/Ray/Dynamics/Multibrot/Bottcher.lean @@ -143,7 +143,7 @@ theorem bottcher_approx_z (d : ℕ) [Fact (2 ≤ d)] {c z : ℂ} (c16 : 16 < abs rcases term_prod_exists (superNearF d c) _ (inv_mem_t c16 cz) with ⟨p, h⟩ rw [h.tprod_eq]; simp only [HasProd] at h apply le_of_tendsto' (Filter.Tendsto.comp Complex.continuous_abs.continuousAt (h.sub_const 1)) - clear h; intro A; simp only [Function.comp] + clear h; intro A; simp only [Function.comp_def] rw [(by norm_num : (16 : ℝ) = 4 * 4), mul_assoc] refine dist_prod_one_le_abs_sum ?_ (by linarith) refine le_trans (Finset.sum_le_sum fun n _ ↦ term_approx d (by linarith) cz n) ?_ @@ -183,7 +183,7 @@ theorem bottcher_hasDerivAt_one : HasDerivAt (fun z : ℂ ↦ bottcher d (↑z) /-- bottcher is nonsingular at `∞` -/ theorem bottcher_mfderiv_inf_ne_zero : mfderiv I I (bottcher d) ∞ ≠ 0 := by simp only [mfderiv, (bottcherMAnalytic d _ multibrotExt_inf).mdifferentiableAt, if_pos, - writtenInExtChartAt, bottcher_inf, extChartAt_inf, extChartAt_eq_refl, Function.comp, + writtenInExtChartAt, bottcher_inf, extChartAt_inf, extChartAt_eq_refl, Function.comp_def, PartialEquiv.refl_coe, id, PartialEquiv.trans_apply, Equiv.toPartialEquiv_apply, invEquiv_apply, RiemannSphere.inv_inf, coePartialEquiv_symm_apply, toComplex_zero, PartialEquiv.coe_trans_symm, PartialEquiv.symm_symm, coePartialEquiv_apply, Equiv.toPartialEquiv_symm_apply, invEquiv_symm, diff --git a/Ray/Dynamics/Multibrot/Connected.lean b/Ray/Dynamics/Multibrot/Connected.lean index 886554d..ccbaed8 100644 --- a/Ray/Dynamics/Multibrot/Connected.lean +++ b/Ray/Dynamics/Multibrot/Connected.lean @@ -78,7 +78,7 @@ theorem isConnected_multibrot (d : ℕ) [Fact (2 ≤ d)] : IsConnected (multibro have e : _root_.multibrot d = (fun z : 𝕊 ↦ z.toComplex) '' (multibrotExt d)ᶜ := by apply Set.ext; intro z; simp only [mem_image, mem_compl_iff]; constructor intro m; use z - simp only [multibrotExt_coe, not_not, m, toComplex_coe, true_and_iff, + simp only [multibrotExt_coe, not_not, m, toComplex_coe, true_and, eq_self_iff_true] intro ⟨w, m, wz⟩; induction w using OnePoint.rec · contrapose m; clear m; simp only [not_not, multibrotExt_inf] @@ -101,8 +101,8 @@ theorem isConnected_compl_multibrot (d : ℕ) [Fact (2 ≤ d)] : IsConnected (_r 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, true_and_iff, toComplex_coe, not_false_iff, true_and_iff, - mem_diff, eq_self_iff_true, and_true_iff, mem_singleton_iff, coe_ne_inf] + simp only [multibrotExt_coe, m, true_and, toComplex_coe, not_false_iff, true_and, + mem_diff, eq_self_iff_true, 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, not_not] · simp only [multibrotExt_coe, toComplex_coe, mem_diff] at m wz; rwa [← wz] diff --git a/Ray/Dynamics/Multibrot/Isomorphism.lean b/Ray/Dynamics/Multibrot/Isomorphism.lean index f4ed16f..9d467ce 100644 --- a/Ray/Dynamics/Multibrot/Isomorphism.lean +++ b/Ray/Dynamics/Multibrot/Isomorphism.lean @@ -104,7 +104,7 @@ theorem bottcher_inj : InjOn (bottcher d) (multibrotExt d) := by rw [nhds_prod_eq, ← Filter.prod_map_map_eq, ← (bottcherNontrivial xm).nhds_eq_map_nhds, ← (bottcherNontrivial ym).nhds_eq_map_nhds, m1.1, ← nhds_prod_eq] apply (continuous_id.prod_mk continuous_id).continuousAt.frequently - simp only [eq_self_iff_true, true_and_iff, ← yp, ← abs_bottcher]; apply frequently_smaller + simp only [eq_self_iff_true, true_and, ← yp, ← abs_bottcher]; apply frequently_smaller rw [← Complex.abs.ne_zero_iff, abs_bottcher, yp]; exact p0 simp only [Filter.frequently_map] at f rcases(f.and_eventually (Ne.eventually_ne xy)).exists with ⟨⟨v, w⟩, ⟨bvw, pv⟩, vw⟩ diff --git a/Ray/Dynamics/Multibrot/Iterates.lean b/Ray/Dynamics/Multibrot/Iterates.lean index e21bba8..ce8c1b1 100644 --- a/Ray/Dynamics/Multibrot/Iterates.lean +++ b/Ray/Dynamics/Multibrot/Iterates.lean @@ -111,7 +111,7 @@ lemma f_error_nonneg {d : ℕ} [Fact (2 ≤ d)] {z : ℂ} (z3 : 3 ≤ abs z) : 0 have l1 : 1 ≤ log (abs z) := le_trans (by norm_num) (le_log_abs_z z3) apply Real.log_nonpos · simp only [one_div, neg_div, sub_nonneg, neg_le] - rw [le_div_iff (by positivity), neg_one_mul, neg_le] + rw [le_div_iff₀ (by positivity), neg_one_mul, neg_le] trans 2 · refine le_trans (neg_log_one_sub_le_linear (c := 2) (by positivity) (by norm_num) ?_) ?_ · exact le_trans (inv_le_inv_of_le (by positivity) z3) (by norm_num) @@ -459,7 +459,7 @@ theorem f_approx {c z : ℂ} (z3 : 3 ≤ abs z) (cz : abs c ≤ abs z) : generalize hu : log (abs (1 + c / z ^ d)) / (d * log (abs z)) = u ring_nf have inner : |u| ≤ -log (1 - 1/abs z) / (d * log (abs z)) := by - simp only [←hu, abs_div, abs_of_pos l1, div_le_iff l1] + simp only [←hu, abs_div, abs_of_pos l1, div_le_iff₀ l1] apply le_trans l2; apply le_of_eq; field_simp have weak : -log (1 - 1/abs z) / (d * log (abs z)) < 1 := by rw [div_lt_one l1] diff --git a/Ray/Dynamics/Multibrot/Log1p.lean b/Ray/Dynamics/Multibrot/Log1p.lean index 4986a64..62726a1 100644 --- a/Ray/Dynamics/Multibrot/Log1p.lean +++ b/Ray/Dynamics/Multibrot/Log1p.lean @@ -110,7 +110,7 @@ lemma neg_log_one_sub_le_linear {x c : ℝ} (x0 : 0 ≤ x) (c1 : 1 < c) apply mul_le_mul_of_nonneg_right _ x0 nth_rw 1 [←inv_inv x] rw [←mul_inv, mul_sub, mul_one, inv_mul_cancel₀ xz] - rw [add_comm, ←le_sub_iff_add_le, div_le_iff (by norm_num)] + rw [add_comm, ←le_sub_iff_add_le, div_le_iff₀ (by norm_num)] apply inv_le_of_inv_le c1p rw [le_sub_iff_add_le, le_inv (add_pos (inv_pos.mpr c1p) (by norm_num)) x0'] exact xc diff --git a/Ray/Dynamics/Multibrot/Potential.lean b/Ray/Dynamics/Multibrot/Potential.lean index db90d68..bf638e3 100644 --- a/Ray/Dynamics/Multibrot/Potential.lean +++ b/Ray/Dynamics/Multibrot/Potential.lean @@ -220,7 +220,7 @@ lemma potential_error_le' (d : ℕ) [Fact (2 ≤ d)] (i j b : ℝ) {c z : ℂ} simp only [add_comm (1:ℝ), ←sub_le_iff_le_add] refine le_trans ij (Real.exp_le_exp.mpr ?_) simp only [neg_div, neg_le_neg_iff, div_mul_eq_div_div] - rw [div_le_iff l0, mul_comm j, ←div_le_iff j0] + rw [div_le_iff₀ l0, mul_comm j, ←div_le_iff₀ j0] trans 0.8095 / b / j · gcongr · rw [Real.le_log_iff_exp_le z0] @@ -255,7 +255,7 @@ lemma iter_error_le_log_log_abs (d : ℕ) [Fact (2 ≤ d)] {c z : ℂ} (z4 : 4 exact le_trans (exp_div_lt).le hl refine le_trans ?_ hll apply le_trans (iter_error_le_of_z4 d z4 cz) - rw [div_le_iff' (by positivity), ←div_le_iff (by norm_num)] + rw [div_le_iff₀' (by positivity), ←div_le_iff₀ (by norm_num)] refine le_trans (by norm_num) (mul_le_mul z4 hl (by positivity) (by positivity)) /-- `s.potential ≈ 1/abs z` -/ diff --git a/Ray/Dynamics/Multiple.lean b/Ray/Dynamics/Multiple.lean index 13d8d45..5e7834d 100644 --- a/Ray/Dynamics/Multiple.lean +++ b/Ray/Dynamics/Multiple.lean @@ -66,7 +66,7 @@ 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_iff] 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]; exact ia.mdifferentiableAt rcases exist_root_of_unity s.d2 with ⟨a, a1, ad⟩ @@ -84,7 +84,7 @@ theorem SuperAt.not_local_inj {f : ℂ → ℂ} {d : ℕ} (s : SuperAt f d) : have t2 : ContinuousAt f 0 := s.fa0.continuousAt have m0 : ∀ᶠ z in 𝓝 0, i (a * bottcherNear f d z) ∈ t := by refine (ia.continuousAt.comp_of_eq t0 ?_).eventually_mem (s.o.mem_nhds ?_) - repeat' simp only [bottcherNear_zero, MulZeroClass.mul_zero, i0, s.t0, Function.comp] + repeat' simp only [bottcherNear_zero, MulZeroClass.mul_zero, i0, s.t0, Function.comp_def] have m1 : ∀ᶠ z in 𝓝 0, z ∈ t := s.o.eventually_mem s.t0 simp only [ContinuousAt, bottcherNear_zero, MulZeroClass.mul_zero, i0, s.f0] at t0 t1 t2 have tp := t0.prod_mk ba.continuousAt @@ -109,13 +109,13 @@ theorem not_local_inj_of_deriv_zero' {f : ℂ → ℂ} (fa : AnalyticAt ℂ f 0) (f0 : f 0 = 0) : ∃ g : ℂ → ℂ, AnalyticAt ℂ g 0 ∧ g 0 = 0 ∧ ∀ᶠ z in 𝓝[{0}ᶜ] 0, g z ≠ z ∧ f (g z) = f z := by by_cases o0 : orderAt f 0 = 0 - · simp only [orderAt_eq_zero_iff fa, f0, Ne, eq_self_iff_true, not_true, or_false_iff] at o0 + · simp only [orderAt_eq_zero_iff fa, f0, Ne, eq_self_iff_true, not_true, or_false] at o0 use fun z ↦ -z, (analyticAt_id _ _).neg, neg_zero; rw [eventually_nhdsWithin_iff] have e0 : ∀ᶠ z in 𝓝 0, f (-z) = 0 := by nth_rw 1 [← neg_zero] at o0; exact continuousAt_neg.eventually o0 refine o0.mp (e0.mp (.of_forall fun z f0' f0 z0 ↦ ?_)) simp only [mem_compl_singleton_iff] at z0; rw [Pi.zero_apply] at f0 - rwa [f0, f0', eq_self_iff_true, and_true_iff, neg_ne_self ℂ] + rwa [f0, f0', eq_self_iff_true, and_true, neg_ne_self ℂ] have o1 : orderAt f 0 ≠ 1 := by have d := df.deriv; contrapose d; simp only [not_not] at d exact deriv_ne_zero_of_orderAt_eq_one d @@ -183,7 +183,7 @@ theorem not_local_inj_of_mfderiv_zero {f : S → T} {c : S} (fa : MAnalyticAt I apply mem_extChartAt_source; apply mem_extChartAt_source exact MDifferentiableAt.comp _ fd (MAnalyticAt.extChartAt_symm (mem_extChartAt_target _ _)).mdifferentiableAt - simp only [mAnalyticAt_iff_of_boundaryless, Function.comp, hg] at fa + 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' diff --git a/Ray/Dynamics/Postcritical.lean b/Ray/Dynamics/Postcritical.lean index 551c91a..110c4c5 100644 --- a/Ray/Dynamics/Postcritical.lean +++ b/Ray/Dynamics/Postcritical.lean @@ -44,7 +44,7 @@ def Super.p (s : Super f d a) (c : ℂ) : ℝ := /-- `s.ps c` is nonempty (since it contains 1) -/ theorem Super.nonempty_ps (s : Super f d a) : (s.ps c).Nonempty := - ⟨1, by simp only [Super.ps, mem_setOf, eq_self_iff_true, true_or_iff]⟩ + ⟨1, by simp only [Super.ps, mem_setOf, eq_self_iff_true, true_or]⟩ /-- `s.ps c` is compact -/ theorem Super.compact_ps (s : Super f d a) [OnePreimage s] [T2Space S] : IsCompact (s.ps c) := by diff --git a/Ray/Dynamics/Potential.lean b/Ray/Dynamics/Potential.lean index 6932167..37b60cd 100644 --- a/Ray/Dynamics/Potential.lean +++ b/Ray/Dynamics/Potential.lean @@ -103,7 +103,7 @@ theorem Super.potential_a (s : Super f d a) : s.potential c a = 0 := by /-- If `z` doesn't reach `s.near`, `potential = 1` -/ theorem Super.potential_eq_one (s : Super f d a) (a : ∀ n, (c, (f c)^[n] z) ∉ s.near) : s.potential c z = 1 := by - simp only [Super.potential, not_exists.mpr a, not_false_iff, dif_neg, and_false_iff] + simp only [Super.potential, not_exists.mpr a, not_false_iff, dif_neg, and_false] /-- If `z` reaches `s.near`, `potential < 1` -/ theorem Super.potential_lt_one (s : Super f d a) (a : ∃ n, (c, (f c)^[n] z) ∈ s.near) : @@ -251,7 +251,7 @@ theorem Super.no_jump (s : Super f d a) [OnePreimage s] [T2Space S] (c : ℂ) (n rcases i with ⟨⟨q, qp, m⟩, b⟩ simp only [Prod.ext_iff] at qp; simp only [qp.1] at b simp only [Set.mem_image, Set.mem_compl_iff, Set.mem_inter_iff, Set.mem_prod_eq, Set.mem_univ, - and_true_iff, Prod.ext_iff, t] + and_true, Prod.ext_iff, t] use q, ⟨b, m⟩, qp.1.symm, qp.2.symm have m := th.mem_of_closed tc rcases(Set.mem_image _ _ _).mp m with ⟨p, m, pa⟩ @@ -260,7 +260,7 @@ theorem Super.no_jump (s : Super f d a) [OnePreimage s] [T2Space S] (c : ℂ) (n contrapose m; simp only [not_not, Set.mem_compl_iff] at m ⊢ rw [← @Prod.mk.eta _ _ p, pa.1, m] simp only [Set.mem_inter_iff, Set.prod_mk_mem_set_prod_eq, Metric.mem_closedBall, dist_self, - zero_le_one, Set.mem_univ, Set.mem_compl_iff, true_and_iff, Set.not_not_mem, not_not, + zero_le_one, Set.mem_univ, Set.mem_compl_iff, true_and, Set.not_not_mem, not_not, na] /-- A barrier is a compact, annular region around `a` (but not containing it) such that @@ -320,7 +320,7 @@ theorem Barrier.potential_large {s : Super f d a} [OnePreimage s] {n t : Set ( by_cases t0 : t = ∅ · use 1, zero_lt_one simp only [t0, gt_iff_lt, Set.mem_empty_iff_false, IsEmpty.forall_iff, forall_const, - imp_true_iff, and_true_iff] + imp_true_iff, and_true] simp only [← ne_eq, ← Set.nonempty_iff_ne_empty] at t0 have pc : ContinuousOn (uncurry s.potential) t := by refine ContinuousOn.mono ?_ b.near @@ -376,7 +376,7 @@ theorem Continuous.potential (s : Super f d a) [OnePreimage s] [T2Space S] : · use 0; simp only [za, Function.iterate_zero_apply, s.mem_near c] have sn : {(c, a)}ᶜ ∈ 𝓝 (c, z) := compl_singleton_mem_nhds - (by simp only [za, Ne, Prod.mk.inj_iff, and_false_iff, not_false_iff]) + (by simp only [za, Ne, Prod.mk.inj_iff, and_false, not_false_iff]) rcases (Filter.hasBasis_iff.mp (compact_basis_nhds (c, z)) ({(c, a)}ᶜ)).mp sn with ⟨u, ⟨un, uc⟩, ua⟩ simp only [Set.subset_compl_singleton_iff] at ua @@ -415,7 +415,7 @@ theorem Continuous.potential (s : Super f d a) [OnePreimage s] [T2Space S] : have ef : ∃ᶠ p in 𝓝 (c, z), p ∈ b.fast n := by refine (re.and_eventually ev).mp (.of_forall ?_) intro ⟨e, z⟩ ⟨zy, m⟩ - simp only [Set.mem_inter_iff, Set.mem_prod, Set.mem_univ, and_true_iff] at m + simp only [Set.mem_inter_iff, Set.mem_prod, Set.mem_univ, and_true] at m exact vh e m.2 z m.1 zy rcases b.mem_fast.mp (ef.mem_of_closed (b.closed_fast _)) with ⟨n, _, r⟩ exact ⟨n, b.near r⟩ @@ -502,17 +502,17 @@ def Super.np (s : Super f d a) (c : ℂ) (p : ℝ) : ℕ := theorem Super.nice_np (s : Super f d a) (c : ℂ) {p : ℝ} (p1 : p < 1) [op : OnePreimage s] : s.IsNiceN c p (s.np c p) := by have q : p < 1 ∧ OnePreimage s := ⟨p1, op⟩ - simp only [Super.np, q, true_and_iff, dif_pos] + simp only [Super.np, q, true_and, dif_pos] exact Nat.find_spec (s.has_nice_n c p1) theorem Super.np_zero (s : Super f d a) (c : ℂ) [op : OnePreimage s] : s.np c 0 = 0 := by - simp only [Super.np, zero_lt_one, op, true_and_iff, dif_pos, Nat.find_eq_zero, Super.isNice_zero] + simp only [Super.np, zero_lt_one, op, true_and, dif_pos, Nat.find_eq_zero, Super.isNice_zero] theorem Super.np_mono (s : Super f d a) (c : ℂ) {p0 p1 : ℝ} (le : p0 ≤ p1) (p11 : p1 < 1) [op : OnePreimage s] : s.np c p0 ≤ s.np c p1 := by have p01 : p0 < 1 := lt_of_le_of_lt le p11 have e : s.np c p0 = Nat.find (s.has_nice_n c p01) := by - simp only [Super.np, p01, op, true_and_iff, dif_pos] + simp only [Super.np, p01, op, true_and, dif_pos] rw [e]; apply Nat.find_min'; exact fun z zp ↦ s.nice_np c p11 _ (_root_.trans zp le) /-- An `n` such that `(f c)^[n]` sends everything with potential < `s.potential c z` to `s.near` -/ diff --git a/Ray/Dynamics/Ray.lean b/Ray/Dynamics/Ray.lean index 18b7e92..c5c7bc6 100644 --- a/Ray/Dynamics/Ray.lean +++ b/Ray/Dynamics/Ray.lean @@ -78,7 +78,7 @@ theorem Super.ext_connected (s : Super f d a) [OnePreimage s] : IsConnected s.ex 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_iff, mem_singleton_iff, eq_self_iff_true, or_true_iff] + true_and, mem_singleton_iff, eq_self_iff_true, 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 ⟨c, x⟩ m; simp only [mem_prod_eq, mem_singleton_iff] at m; rw [m.2]; exact s.mem_ext c @@ -178,7 +178,7 @@ theorem Super.ray_noncritical (s : Super f d a) [OnePreimage s] (post : (c, x) rw [x0] at d replace d := Eq.trans d (ContinuousLinearMap.zero_apply _) rw [deriv_pow, mul_eq_zero, Nat.cast_eq_zero, pow_eq_zero_iff', pow_eq_zero_iff'] at d - simp only [s.d0, false_and_iff, false_or_iff] at d; exact d.1 + simp only [s.d0, false_and, false_or] at d; exact d.1 simp only [mfderiv_comp x (s.bottcherNearIter_mAnalytic (s.ray_near post)).along_snd.mdifferentiableAt (s.ray_mAnalytic post).along_snd.mdifferentiableAt, diff --git a/Ray/Hartogs/FubiniBall.lean b/Ray/Hartogs/FubiniBall.lean index 6e3ffca..70a2674 100644 --- a/Ray/Hartogs/FubiniBall.lean +++ b/Ray/Hartogs/FubiniBall.lean @@ -85,8 +85,6 @@ theorem Metric.sphere_eq_empty {S : Type} [RCLike S] {c : S} {r : ℝ} : sphere rw [← not_nonempty_iff_eq_empty] at n simpa only [not_lt, NormedSpace.sphere_nonempty, not_le] using n -attribute [bound] Int.ceil_lt_add_one - /-- `range (circleMap c r _) = sphere c r` even when restricted to `Ioc 0 (2π)` -/ theorem circleMap_Ioc {c z : ℂ} {r : ℝ} (zs : z ∈ sphere c r) : ∃ t, t ∈ Ioc 0 (2 * π) ∧ z = circleMap c r t := by @@ -323,9 +321,8 @@ theorem NiceVolume.closedBall (c : ℂ) {r : ℝ} (rp : r > 0) : NiceVolume (clo finite := by simp only [Complex.volume_closedBall] apply ENNReal.mul_lt_top - · simp only [ne_eq, ENNReal.pow_eq_top_iff, ENNReal.ofReal_ne_top, OfNat.ofNat_ne_zero, - not_false_eq_true, and_true] - · simp only [ne_eq, ENNReal.coe_ne_top, not_false_eq_true] + · exact Batteries.compareOfLessAndEq_eq_lt.mp rfl + · exact ENNReal.coe_lt_top pos := by simp only [Complex.volume_closedBall, gt_iff_lt, CanonicallyOrderedCommSemiring.mul_pos, ENNReal.coe_pos, NNReal.pi_pos, and_true] diff --git a/Ray/Hartogs/Hartogs.lean b/Ray/Hartogs/Hartogs.lean index cd09576..50b4fb2 100644 --- a/Ray/Hartogs/Hartogs.lean +++ b/Ray/Hartogs/Hartogs.lean @@ -234,7 +234,7 @@ theorem on_subdisk [CompleteSpace E] (h : Har f (closedBall (c0, c1) r)) (rp : r intro b; rw [← hS]; simp only [← forall_const_and_distrib] rw [Set.setOf_forall]; apply isClosed_iInter; intro z1 by_cases z1r : z1 ∉ closedBall c1 r - · simp only [z1r, false_imp_iff, and_true_iff, Set.setOf_mem_eq, Metric.isClosed_ball] + · simp only [z1r, false_imp_iff, and_true, Set.setOf_mem_eq, Metric.isClosed_ball] · rw [Set.not_not_mem] at z1r simp only [z1r, true_imp_iff] refine ContinuousOn.isClosed_le Metric.isClosed_ball ?_ continuousOn_const @@ -360,7 +360,7 @@ theorem to_uneven [CompleteSpace E] (h : Har f (closedBall (c0, c1) r)) (rp : r have a' : AnalyticOn ℂ f (ball c0' (min r0 (r / 2)) ×ˢ ball c1 (r / 2)) := by apply a.mono; apply Set.prod_mono apply Metric.ball_subset_ball' - simp only [dist_self, add_zero, min_le_iff, le_refl, true_or_iff] + simp only [dist_self, add_zero, min_le_iff, le_refl, true_or] apply Metric.ball_subset_ball; linarith use c0', min r0 (r / 2), r / 2, _root_.trans Metric.ball_subset_closedBall sub, c0m exact @@ -597,7 +597,7 @@ theorem unevenSeries_analytic [CompleteSpace E] (u : Uneven f c0 c1 r0 r1) (n : simp only [Prod.ext_iff, Prod.fst_zero, Prod.snd_zero, sub_self, and_self_iff] rw [g0] at pa have ta := pa.comp (ga z1 (Set.mem_univ _)) - simp_rw [Function.comp] at ta; clear pa ga g0 + simp_rw [Function.comp_def] at ta; clear pa ga g0 have pu : ∀ᶠ w1 in nhds z1, unevenSeries u w1 n = (p.changeOrigin (g w1)).along0 n := by rw [eventually_nhds_iff] set s' := r1 - dist z1 c1 @@ -665,7 +665,7 @@ theorem unevenLog_uniform_bound [CompleteSpace E] (u : Uneven f c0 c1 r0 r1) {s gcongr · bound · trans max 1 c ^ 1 - · simp only [pow_one, le_max_iff, le_refl, or_true_iff] + · simp only [pow_one, le_max_iff, le_refl, or_true] · bound · bound @@ -692,7 +692,7 @@ theorem unevenLog_nonuniform_bound [CompleteSpace E] (u : Uneven f c0 c1 r0 r1) calc ‖r1 ^ n • unevenTerm u z1 n‖ _ = r1 ^ n * t := by simp only [← ht, norm_smul, abs_of_pos u.r1p, norm_pow, Real.norm_eq_abs, mul_eq_mul_left_iff, - eq_self_iff_true, true_or_iff, abs_pow] + eq_self_iff_true, true_or, abs_pow] _ ≤ r1 ^ n * (c * s⁻¹ ^ n) := by bound _ = r1 ^ n * (c * (e.exp ^ n / r1 ^ n)) := by rw [inv_div, div_pow] _ = r1 ^ n / r1 ^ n * c * e.exp ^ n := by ring @@ -716,8 +716,6 @@ theorem uneven_nonuniform_subharmonic [CompleteSpace E] [SecondCountableTopology rw [← analyticOn_iff_differentiableOn Metric.isOpen_ball] apply unevenTerm.analytic u -attribute [bound] Real.log_pos - /-- The nonuniform bound holds uniformly -/ theorem unevenSeries_strong_bound [CompleteSpace E] [SecondCountableTopology E] (u : Uneven f c0 c1 r0 r1) {s : ℝ} (sp : 0 < s) (sr : s < r1) : diff --git a/Ray/Hartogs/MaxLog.lean b/Ray/Hartogs/MaxLog.lean index b225699..b961f49 100644 --- a/Ray/Hartogs/MaxLog.lean +++ b/Ray/Hartogs/MaxLog.lean @@ -14,7 +14,7 @@ over the extended reals. `log (f z)` is subharmonic if `f z` is analytic, but ` open Complex (abs) open scoped Real -open Set (univ Ici) +open Set noncomputable section variable {E : Type} [NormedAddCommGroup E] [NormedSpace ℂ E] @@ -94,8 +94,8 @@ theorem LipschitzOnWith.log (b : ℝ) : LipschitzOnWith (-b).exp.toNNReal Real.l /-- `maxLog` is Lipschitz -/ theorem LipschitzWith.maxLog (b : ℝ) : LipschitzWith (-b).exp.toNNReal (maxLog b) := by rw [← lipschitzOnWith_univ] - have h := (LipschitzOnWith.log b).comp ((LipschitzWith.id.const_max b.exp).lipschitzOnWith univ) - (by simp only [id_eq, Set.mapsTo_univ_iff, Set.mem_Ici, le_max_iff, le_refl, true_or, - forall_const]) + have h := (LipschitzOnWith.log b).comp ((LipschitzWith.id.const_max b.exp).lipschitzOnWith + (s := univ)) (by simp only [id_eq, Set.mapsTo_univ_iff, Set.mem_Ici, le_max_iff, le_refl, + true_or, forall_const]) have e : Real.log ∘ max (Real.exp b) = _root_.maxLog b := by funext x; simp [_root_.maxLog] simpa only [e, mul_one, id_eq, ge_iff_le, lipschitzOnWith_univ] using h diff --git a/Ray/Hartogs/Subharmonic.lean b/Ray/Hartogs/Subharmonic.lean index cf12490..7eac898 100644 --- a/Ray/Hartogs/Subharmonic.lean +++ b/Ray/Hartogs/Subharmonic.lean @@ -274,7 +274,7 @@ theorem Minimum.submean {f : ℂ → ℝ} {s : Set ℂ} {c : ℂ} (fc : Continuo have m := setIntegral_ge_of_const_le n.measurable n.ne_top fg ((fc.mono ss).integrableOn_sphere tp) simp only [MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter, smul_eq_mul, ge_iff_le] - simpa only [mul_comm, ← div_eq_mul_inv, le_div_iff n.real_pos] + simpa only [mul_comm, ← div_eq_mul_inv, le_div_iff₀ n.real_pos] /-- `max b (log ‖f z‖)` is subharmonic for analytic `f` (`ℂ` case) -/ theorem AnalyticOn.maxLogAbsSubharmonicOn {f : ℂ → ℂ} {s : Set ℂ} (fa : AnalyticOn ℂ f s) (b : ℝ) : @@ -877,7 +877,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_iff, forall_const] + simp only [Set.mem_neg, Set.mem_setOf_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 -/ @@ -899,7 +899,7 @@ theorem le_liminf.simple {L : Type} [CompleteLinearOrder L] [DenselyOrdered L] { · 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 specialize h d; contrapose h - simp only [dc, not_forall, not_le, exists_prop, and_true_iff, Filter.eventually_atTop, + 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 diff --git a/Ray/Misc/AtInf.lean b/Ray/Misc/AtInf.lean index e5aca1a..2bc206a 100644 --- a/Ray/Misc/AtInf.lean +++ b/Ray/Misc/AtInf.lean @@ -66,14 +66,14 @@ theorem tendsto_atInf_iff_tendsto_nhds_zero {𝕜 X : Type} [NontriviallyNormedF constructor · intro h t tl; rcases h t tl with ⟨r, _, m⟩ by_cases rp : 0 < r - · use r⁻¹; simp only [rp, inv_pos, true_and_iff]; intro x xs; refine m ?_ + · 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 (norm_pos_iff.mpr xs.2) rp, xs.1, mem_setOf_eq, norm_inv] - · use 1; simp only [zero_lt_one, true_and_iff]; intro x xs; refine m ?_ + · 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 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_iff] + · 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 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, diff --git a/Ray/Misc/Bounds.lean b/Ray/Misc/Bounds.lean index 1d362a9..96e795b 100644 --- a/Ray/Misc/Bounds.lean +++ b/Ray/Misc/Bounds.lean @@ -232,7 +232,7 @@ theorem le_of_forall_small_le_add {a b t : ℝ} (tp : 0 < t) (h : ∀ e, 0 < e theorem one_over_one_sub_le {x : ℝ} : 0 ≤ x → x ≤ 1/2 → 1/(1 - x) ≤ 1 + 2*x := by intro xp xh have x1 : 1 - x > 0 := by linarith - rw [div_le_iff x1] + rw [div_le_iff₀ x1] calc (1 + 2*x) * (1 - x) = 1 + x * (1 - 2*x) := by ring _ ≥ 1 + x * (1 - 2 * (1/2)) := by bound _ = 1 := by ring diff --git a/Ray/Misc/Connected.lean b/Ray/Misc/Connected.lean index e1deb08..c7bc6bd 100644 --- a/Ray/Misc/Connected.lean +++ b/Ray/Misc/Connected.lean @@ -141,7 +141,7 @@ theorem IsPreconnected.limits_Ioc [CompactSpace X] [T4Space X] {r : ℝ → X} { 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 - simp only [Subtype.coe_mk, Ioc_subset_Ioc_iff m.1, m.2, le_refl, true_and_iff] + simp only [Subtype.coe_mk, Ioc_subset_Ioc_iff m.1, m.2, le_refl, true_and] 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 @@ -197,7 +197,7 @@ theorem IsPathConnected.image_of_continuousOn {X Y : Type} [TopologicalSpace X] IsPathConnected (f '' s) := by have uc : IsPathConnected (univ : Set s) := by convert sc.preimage_coe (subset_refl _); apply Set.ext; intro x - simp only [mem_univ, true_iff_iff, mem_preimage, Subtype.mem] + simp only [mem_univ, true_iff, mem_preimage, Subtype.mem] have e : f '' s = s.restrict f '' univ := by apply Set.ext; intro y; constructor intro ⟨x, m, e⟩; use⟨x, m⟩, mem_univ _, e diff --git a/Ray/Misc/Measure.lean b/Ray/Misc/Measure.lean index 025aca6..e50274e 100644 --- a/Ray/Misc/Measure.lean +++ b/Ray/Misc/Measure.lean @@ -35,7 +35,7 @@ variable {M : Type} [MeasureSpace 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_iff] + intro x h; simp only [Set.mem_diff, h, not_false_iff, and_true] simp_rw [Set.mem_def] at e refine Filter.Eventually.mono ?_ e rw [ae_iff]; simpa [Set.setOf_set] @@ -259,7 +259,7 @@ theorem mean_squeeze {f : X → ℝ} {s : Set X} {b : ℝ} (sn : NiceVolume s) ( have dm : MeasurableSet (s \ t) := MeasurableSet.diff sn.measurable tm have fb := @setIntegral_mono_on _ _ volume f (fun _ ↦ b) (s \ t) (fi.mono Set.diff_subset (le_refl _)) (integrableOn_const.mpr (Or.inr df)) dm ?_ - simp [measure_diff ts tm (lt_top_iff_ne_top.mp tf), + simp [measure_diff ts tm.nullMeasurableSet (lt_top_iff_ne_top.mp tf), ENNReal.toReal_sub_of_le (measure_mono ts) (lt_top_iff_ne_top.mp sn.finite)] at fb exact fb intro y yd; simp at yd; exact hi y yd.left diff --git a/Ray/Render/Color.lean b/Ray/Render/Color.lean index b1f81f4..158d38d 100644 --- a/Ray/Render/Color.lean +++ b/Ray/Render/Color.lean @@ -230,7 +230,7 @@ def Interval.quantize (x : Interval) : Option UInt8 := /-- `Color.quantize` is conservative -/ @[approx] lemma Color.mem_approx_quantize {c' : Color ℝ} {c : Color Interval} (cm : c' ∈ approx c) : c' ∈ approx c.quantize := by - rw [quantize] + unfold quantize generalize hr : c.r.quantize = r generalize hg : c.g.quantize = g generalize hb : c.b.quantize = b diff --git a/Ray/Render/Iterate.lean b/Ray/Render/Iterate.lean index 2958aad..dbea397 100644 --- a/Ray/Render/Iterate.lean +++ b/Ray/Render/Iterate.lean @@ -57,8 +57,8 @@ lemma iterate'_correct {c z : Box} {rs : Floating} {c' z' : ℂ} {rs' : ℝ} let w' := (f' 2 c')^[i.n - k] z' k ≤ i.n ∧ w' ∈ approx i.z ∧ (i.exit = .large → rs' < abs w' ^ 2) := by induction' n with n h generalizing k z z' - · simpa only [iterate', le_refl, ge_iff_le, tsub_eq_zero_of_le, Function.iterate_zero, id_eq, - IsEmpty.forall_iff, and_true, true_and] + · simpa only [iterate', le_refl, tsub_eq_zero_of_le, Function.iterate_zero, id_eq, reduceCtorEq, + false_implies, and_true, true_and] · simp only [iterate', Floating.val_lt_val] generalize hzr2 : z.re.sqr = zr2 generalize hzi2 : z.im.sqr = zi2 @@ -68,8 +68,8 @@ lemma iterate'_correct {c z : Box} {rs : Floating} {c' z' : ℂ} {rs' : ℝ} have wa : f' 2 c' z' ∈ approx w := by rw [we, f']; approx generalize hw' : f' 2 c' z' = w' at wa by_cases z2n : z2 = nan - · simpa only [z2n, ite_true, le_refl, ge_iff_le, tsub_eq_zero_of_le, Function.iterate_zero, - id_eq, IsEmpty.forall_iff, and_true, true_and] + · simpa only [z2n, ↓reduceIte, le_refl, tsub_eq_zero_of_le, Function.iterate_zero, id_eq, + reduceCtorEq, false_implies, and_true, true_and] by_cases rz : rs.val < z2.val · simp only [z2n, rz, ite_true, le_refl, ge_iff_le, tsub_eq_zero_of_le, Function.iterate_zero, id_eq, zm, forall_true_left, true_and, Complex.abs_def, @@ -106,7 +106,7 @@ lemma iterate_large {c z : Box} {rs : Floating} {n : ℕ} {c' z' : ℂ} rs.val < abs ((f' 2 c')^[(iterate c z rs n).n] z') ^ 2 := by rw [iterate] at l ⊢ by_cases rsn : rs = nan - · simp only [rsn, ↓reduceIte] at l + · simp only [rsn, ↓reduceIte, reduceCtorEq] at l · simp only [rsn, ite_false] at l ⊢ simpa only [not_lt, Nat.sub_zero] using (iterate'_correct cm zm (le_refl _) 0 n).2.2 l diff --git a/Ray/Render/Potential.lean b/Ray/Render/Potential.lean index d188794..2313c6a 100644 --- a/Ray/Render/Potential.lean +++ b/Ray/Render/Potential.lean @@ -155,7 +155,7 @@ lemma Box.approx_potential_large {c' z' : ℂ} {z : Box} (cz : abs c' ≤ abs z' (cm : c' ∈ approx c) (zm : z' ∈ approx z) (n : ℕ) (r : Floating) : (superF 2).potential c' z' ∈ approx (Box.potential c z n r).1 := by set s := superF 2 - rw [Box.potential] + unfold Box.potential generalize hcs : (normSq c).hi = cs generalize hi : iterate c z (cs.max 9) n = i by_cases csn : cs = nan diff --git a/lake-manifest.json b/lake-manifest.json index e3dabeb..1556dbc 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d747f070e42dd21e2649b75090f5b0d45c6ec8e0", + "rev": "46fed98b5cac2b1ea64e363b420c382ed1af0d85", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222", + "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9339d48cc3b7431b6353af47f303691e9d4da229", + "rev": "662f986ad3c5ad6ab1a1726b3c04f5ec425aa9f7", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -35,10 +35,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a96aee5245720f588876021b6a0aa73efee49c76", + "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.41", + "inputRev": "v0.0.42", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", @@ -55,17 +55,27 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6", + "rev": "fb7841a6f4fb389ec0e47dd4677844d49906af3c", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, + {"url": "https://github.com/siddhartha-gadgil/LeanSearchClient.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "c260ed920e2ebd23ef9fc8ca3fd24115e04c18b1", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b35703fe5a80f1fa74b82a2adc22f3631316a5b3", + "rev": "02e27ebc141ee83de5c6ae6b6fa3e98acde287f2", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +85,7 @@ "type": "git", "subDir": null, "scope": "girving", - "rev": "f323ef3b0a7ce173b7d95c0d56a8e122608d093b", + "rev": "b0a6ac2f8e083eacb06d3458604540b93d7f26bf", "name": "interval", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lakefile.lean b/lakefile.lean index adeea33..8f5dc39 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -32,7 +32,7 @@ lean_exe primes { target png.o pkg : FilePath := do let o := pkg.buildDir / "Ray/Render/png.o" - let src ← inputFile <| pkg.dir / "Ray/Render/png.cc" + let src ← inputTextFile <| pkg.dir / "Ray/Render/png.cc" let args := #["-I", (←getLeanIncludeDir).toString, "-I/opt/homebrew/include"] buildO o src args #["-fPIC"] "c++" getLeanTrace @@ -40,4 +40,3 @@ extern_lib libray pkg := do let name := nameToStaticLib "ray" let png ← fetch <| pkg.target ``png.o buildStaticLib (pkg.nativeLibDir / name) #[png] - diff --git a/lean-toolchain b/lean-toolchain index e7a4f40..98556ba 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.11.0-rc2 +leanprover/lean4:v4.12.0-rc1