fix: three false statements (Egorov domain, 10.4.1/9.3.21 Nat div, Lusin caution)

Analysis/MeasureTheory/Section_1_3_5.lean

@@ -1549,7 +1549,7 @@ theorem PointwiseAeConvergesTo.uniformlyConverges_outside_small {d:ℕ} {f : ℕ
   (ε : ℝ) (hε : 0 < ε) :
   ∃ (E: Set (EuclideanSpace' d)), LebesgueMeasurable E ∧
     Lebesgue_measure E ≤ ε ∧
-    UniformlyConvergesToOn f g (Sᶜ ∪ E) := by sorry
+    UniformlyConvergesToOn f g (S ∩ Eᶜ) := by sorry
 
 /-- Theorem 1.3.28 (Lusin's theorem) -/
 theorem ComplexAbsolutelyIntegrable.approx_by_continuous_outside_small {d:ℕ} {f : EuclideanSpace' d → ℂ}
@@ -1562,7 +1562,8 @@ theorem ComplexAbsolutelyIntegrable.approx_by_continuous_outside_small {d:ℕ} {
 /-- Lusin's theorem does not make the original function continuous outside of E -/
 example : ∃ (d:ℕ) (f : EuclideanSpace' d → ℝ),
     RealMeasurable f ∧
-    ∀ (E: Set (EuclideanSpace' d)), LebesgueMeasurable E → Lebesgue_measure E ≤ 1 → ¬ ContinuousOn f Eᶜ := by sorry
+    ∀ (E: Set (EuclideanSpace' d)), LebesgueMeasurable E → Lebesgue_measure E ≤ 1 →
+      ¬ ∀ x ∈ Eᶜ, ContinuousAt f x := by sorry
 
 def LocallyComplexAbsolutelyIntegrable {d:ℕ} (f: EuclideanSpace' d → ℂ) : Prop :=
   ∀ (S: Set (EuclideanSpace' d)), LebesgueMeasurable S ∧ Bornology.IsBounded S → ComplexAbsolutelyIntegrableOn f S

Analysis/Section_10_4.lean

@@ -73,10 +73,10 @@ theorem inverse_function_theorem {X Y: Set ℝ} {f: ℝ → ℝ} {g:ℝ → ℝ}
     convert (hf _ hx _).inv₀ _ using 2 with n <;> grind
 
 /-- Exercise 10.4.1(a) -/
-example {n:ℕ} : ContinuousOn (fun x:ℝ ↦ x^(1/n:ℝ)) (.Ioi 0) := by sorry
+example {n:ℕ} : ContinuousOn (fun x:ℝ ↦ x^(1/(n:ℝ))) (.Ioi 0) := by sorry
 
 /-- Exercise 10.4.1(b) -/
-example {n:ℕ} {x:ℝ} (hx: x ∈ Set.Ioi 0) : HasDerivWithinAt (fun x:ℝ ↦ x^(1/n:ℝ))
+example {n:ℕ} {x:ℝ} (hx: x ∈ Set.Ioi 0) : HasDerivWithinAt (fun x:ℝ ↦ x^(1/(n:ℝ)))
   ((n:ℝ)⁻¹ * x^((n:ℝ)⁻¹-1)) (.Ioi 0) x := by sorry
 
 /-- Exercise 10.4.2(a) -/

Analysis/Section_9_3.lean

@@ -215,7 +215,7 @@ open Classical in
 /-- Example 9.3.21 -/
 noncomputable abbrev f_9_3_21 : ℝ → ℝ := fun x ↦ if x ∈ (fun q:ℚ ↦ (q:ℝ)) '' .univ then 1 else 0
 
-example : Filter.atTop.Tendsto (fun (n:ℕ) ↦ f_9_3_21 (1/n:ℝ)) (nhds 1) := by sorry
+example : Filter.atTop.Tendsto (fun (n:ℕ) ↦ f_9_3_21 (1/(n:ℝ))) (nhds 1) := by sorry
 
 example : Filter.atTop.Tendsto (fun (n:ℕ) ↦ f_9_3_21 ((Real.sqrt 2)/n:ℝ)) (nhds 0) := by sorry