Mathlib.Analysis.Ehlich­Zeller­Mesh

theorem czSup_attained (R : Polynomial ℝ) : ∃ t₀ ∈ Icc (0 : ℝ) pi, |czTrig R t₀| = czSup R := by classical have hK : IsCompact (Icc (0 : ℝ) pi) := isCompact_Icc have hne : (Icc (0 : ℝ) pi).Nonempty := ⟨0, by constructor <;> positivity⟩ have hcont : ContinuousOn (fun t => |czTrig R t|) (Icc (0 : ℝ) pi) := (czTrig_continuous R).abs.continuousOn rcases hK.exists_sSup_image_eq hne hcont with ⟨t₀, ht₀, hsup⟩ exact ⟨t₀, ht₀, hsup.symm⟩

theorem abs_czTrig_le_czSup (R : Polynomial ℝ) {t : ℝ} (ht : t ∈ Icc (0 : ℝ) pi) : |czTrig R t| ≤ czSup R := by classical unfold czSup refine le_csSup ?hbdd ⟨t, ht, rfl⟩ exact isCompact_Icc.bddAbove_image ((czTrig_continuous R).abs.continuousOn)

theorem czTrig_arccos_lipschitz_regularized (R : Polynomial ℝ) (β : ℕ) (hβ : R.natDegree ≤ β) {δ : ℝ} (hδ : 0 < δ) {s t : ℝ} (hs : s ∈ Icc 0 pi) (ht : t ∈ Icc 0 pi) : |arccos (czTrig R t / (czSup R + δ)) - arccos (czTrig R s / (czSup R + δ))| ≤ (β : ℝ) * |t - s| := by let M : ℝ := czSup R let d : ℝ := M + δ have hM_nonneg : 0 ≤ M := by simpa [M] using czSup_nonneg R have hdpos : 0 < d := by dsimp [d, M]; linarith let f : ℝ → ℝ := fun u => arccos (czTrig R u / d) have hdiff_at (x : ℝ) (hx : x ∈ Icc (0 : ℝ) pi) : DifferentiableAt ℝ f x := by have hq_abs : |czTrig R x| ≤ M := by simpa [M] using abs_czTrig_le_czSup R hx have hinner_abs : |czTrig R x / d| < 1 := by rw [abs_div, abs_of_pos hdpos] exact (div_lt_one hdpos).2 (by dsimp [d, M]; linarith) have hne_neg : czTrig R x / d ≠ -1 := by intro h have : |czTrig R x / d| = 1 := by simp [h] linarith have hne_pos : czTrig R x / d ≠ 1 := by intro h have : |czTrig R x / d| = 1 := by simp [h] linarith have hinner_diff : DifferentiableAt ℝ (fun u => czTrig R u / d) x := by unfold czTrig fun_prop exact ((Real.hasDerivAt_arccos hne_neg hne_pos).comp x (DifferentiableAt.hasDerivAt hinner_diff)).differentiableAt have hderiv_bound (x : ℝ) (hx : x ∈ Icc (0 : ℝ) pi) : ‖deriv f x‖ ≤ (β : ℝ) := by have hq_abs : |czTrig R x| ≤ M := by simpa [M] using abs_czTrig_le_czSup R hx have hinner_abs : |czTrig R x / d| < 1 := by rw [abs_div, abs_of_pos hdpos] exact (div_lt_one hdpos).2 (by dsimp [d, M]; linarith) have hinner_sq_lt : (czTrig R x / d) ^ 2 < 1 := by simpa using (sq_lt_one_iff_abs_lt_one (czTrig R x / d)).2 hinner_abs have hinner_pos : 0 < 1 - (czTrig R x / d) ^ 2 := by linarith have hinner_nonneg : 0 ≤ 1 - (czTrig R x / d) ^ 2 := hinner_pos.le have hne_neg : czTrig R x / d ≠ -1 := by intro h have : |czTrig R x / d| = 1 := by simp [h] linarith have hne_pos : czTrig R x / d ≠ 1 := by intro h have : |czTrig R x / d| = 1 := by simp [h] linarith have hinner_diff : DifferentiableAt ℝ (fun u => czTrig R u / d) x := by unfold czTrig fun_prop have hcz_diff : DifferentiableAt ℝ (czTrig R) x := by unfold czTrig fun_prop have hinner_hasDeriv : HasDerivAt (fun u => czTrig R u / d) (deriv (czTrig R) x / d) x := (DifferentiableAt.hasDerivAt hcz_diff).div_const d have hf_hasDeriv : HasDerivAt f (-(1 / sqrt (1 - (czTrig R x / d) ^ 2)) * (deriv (czTrig R) x / d)) x := by simpa [f, Function.comp_def] using (Real.hasDerivAt_arccos hne_neg hne_pos).comp x hinner_hasDeriv have hderiv_eq : deriv f x = -(1 / sqrt (1 - (czTrig R x / d) ^ 2)) * (deriv (czTrig R) x / d) := hf_hasDeriv.deriv have hsqrtd_pos : 0 < sqrt (1 - (czTrig R x / d) ^ 2) := Real.sqrt_pos_of_pos hinner_pos have hden_eq : d * sqrt (1 - (czTrig R x / d) ^ 2) = sqrt (d ^ 2 - (czTrig R x) ^ 2) := by apply (sq_eq_sq₀ (mul_nonneg hdpos.le (Real.sqrt_nonneg _)) (Real.sqrt_nonneg _)).mp rw [mul_pow, Real.sq_sqrt hinner_nonneg] have hdiff_nonneg : 0 ≤ d ^ 2 - (czTrig R x) ^ 2 := by have hlt : |czTrig R x| < d := by dsimp [d, M]; linarith have hsq_lt : (czTrig R x) ^ 2 < d ^ 2 := by have hlt_abs : |czTrig R x| < |d| := by simpa [abs_of_pos hdpos] using hlt exact (sq_lt_sq (a := czTrig R x) (b := d)).2 hlt_abs linarith rw [Real.sq_sqrt hdiff_nonneg] field_simp [ne_of_gt hdpos] have hderiv_abs : |deriv f x| = |deriv (czTrig R) x| / (d * sqrt (1 - (czTrig R x / d) ^ 2)) := by rw [hderiv_eq, abs_mul, abs_neg, abs_div, abs_one, abs_of_pos hsqrtd_pos, abs_div, abs_of_pos hdpos] field_simp [ne_of_gt hsqrtd_pos, ne_of_gt hdpos] have hrad_le : sqrt (M ^ 2 - (czTrig R x) ^ 2) ≤ d * sqrt (1 - (czTrig R x / d) ^ 2) := by rw [hden_eq] apply Real.sqrt_le_sqrt dsimp [d] nlinarith [hM_nonneg, hδ] have hnum_le : |deriv (czTrig R) x| ≤ (β : ℝ) * (d * sqrt (1 - (czTrig R x / d) ^ 2)) := (czTrig_szego_deriv R β hβ x).trans (mul_le_mul_of_nonneg_left hrad_le (by positivity)) have hden_pos : 0 < d * sqrt (1 - (czTrig R x / d) ^ 2) := mul_pos hdpos hsqrtd_pos rw [Real.norm_eq_abs, hderiv_abs] exact (div_le_iff₀ hden_pos).2 (by simpa [mul_comm, mul_left_comm, mul_assoc] using hnum_le) have hmv := Convex.norm_image_sub_le_of_norm_deriv_le (f := f) (s := Icc (0 : ℝ) pi) (C := (β : ℝ)) hdiff_at hderiv_bound (convex_Icc (0 : ℝ) pi) hs ht simpa [f, d, M, Real.norm_eq_abs, abs_sub_comm] using hmv

theorem exists_meshParam_close (k : ℕ) (hk : 0 < k) {t₀ : ℝ} (ht₀ : t₀ ∈ Icc (0 : ℝ) Real.pi) : ∃ j ∈ range (k + 1), |t₀ - Real.pi * j / k| ≤ Real.pi / (2 * k) := by let x : ℝ := t₀ * k / Real.pi let n : ℤ := round x let j : ℕ := n.toNat have hkℝ : 0 < (k : ℝ) := by exact_mod_cast hk have hπpos : 0 < Real.pi := Real.pi_pos have hπne : Real.pi ≠ 0 := ne_of_gt hπpos have hkne : (k : ℝ) ≠ 0 := ne_of_gt hkℝ have hx_nonneg : 0 ≤ x := by dsimp [x] exact div_nonneg (mul_nonneg ht₀.1 hkℝ.le) hπpos.le have hx_le : x ≤ k := by dsimp [x] calc t₀ * (k : ℝ) / Real.pi ≤ Real.pi * (k : ℝ) / Real.pi := by gcongr exact ht₀.2 _ = k := by field_simp [hπne] have hn_nonneg : (0 : ℤ) ≤ n := by change (0 : ℤ) ≤ round x rw [round_eq] exact (Int.floor_nonneg).2 (by linarith) have hn_le : n ≤ (k : ℤ) := by change round x ≤ (k : ℤ) rw [round_eq, Int.floor_le_iff] change x + 1 / 2 < (k : ℝ) + 1 linarith have hj_le : j ≤ k := by dsimp [j] omega have hj_mem : j ∈ range (k + 1) := by rw [Finset.mem_range] exact Nat.lt_succ_of_le hj_le refine ⟨j, hj_mem, ?_⟩ have hj_cast : (j : ℝ) = (n : ℝ) := by dsimp [j] exact_mod_cast (Int.toNat_of_nonneg hn_nonneg) have hround : |x - (j : ℝ)| ≤ (1 : ℝ) / 2 := by simpa [hj_cast] using (abs_sub_round x) have hscale : t₀ - Real.pi * (j : ℝ) / k = (Real.pi / k) * (x - (j : ℝ)) := by dsimp [x] field_simp [hπne, hkne] calc |t₀ - Real.pi * (j : ℝ) / k| = |Real.pi / k| * |x - (j : ℝ)| := by rw [hscale, abs_mul] _ = (Real.pi / k) * |x - (j : ℝ)| := by rw [abs_of_nonneg (div_nonneg hπpos.le hkℝ.le)] _ ≤ (Real.pi / k) * ((1 : ℝ) / 2) := by exact mul_le_mul_of_nonneg_left hround (div_nonneg hπpos.le hkℝ.le) _ = Real.pi / (2 * k) := by field_simp [hkne]

theorem czMeshLHS_le_czSup (R : Polynomial ℝ) : sSup ((fun x => |R.eval x|) '' Icc (-1 : ℝ) 1) ≤ czSup R := by refine Real.sSup_le ?_ (czSup_nonneg R) rintro y ⟨x, hx, rfl⟩ let t := arccos (-x) have ht : t ∈ Icc (0 : ℝ) pi := ⟨Real.arccos_nonneg (-x), Real.arccos_le_pi (-x)⟩ have hcos : -cos t = x := by have hx₁ : -1 ≤ -x := by linarith [hx.2] have hx₂ : -x ≤ 1 := by linarith [hx.1] simp [t, Real.cos_arccos hx₁ hx₂] simpa [czTrig, hcos] using abs_czTrig_le_czSup R ht

theorem eval_node_le_czMeshMax (R : Polynomial ℝ) (k : ℕ) {j : ℕ} (hj : j ∈ range (k + 1)) : |R.eval (czNode k j)| ≤ czMeshMax R k := by let s := range (k + 1) let f : ℕ → ℝ := fun j => |R.eval (czNode k j)| have hsne : s.Nonempty := ⟨0, by simp [s]⟩ let M : ℝ := max 0 (s.sup' hsne f) have hM_nonneg : 0 ≤ M := le_max_left _ _ have hval_le_M {i : ℕ} (hi : i ∈ s) : f i ≤ M := by exact (Finset.le_sup' f hi).trans (le_max_right _ _) have hinner_bound (i : ℕ) : (⨆ (_ : i ∈ s), f i) ≤ M := by exact Real.iSup_le (fun hi => hval_le_M hi) hM_nonneg have houter_bdd : BddAbove (range (fun i => ⨆ (_ : i ∈ s), f i)) := ⟨M, by rintro _ ⟨i, rfl⟩; exact hinner_bound i⟩ have hinner_bdd : BddAbove (range (fun _ : j ∈ s => f j)) := ⟨f j, by rintro _ ⟨hj, rfl⟩; rfl⟩ have hinner : f j ≤ ⨆ (_ : j ∈ s), f j := le_ciSup hinner_bdd hj have houter : f j ≤ ⨆ i, ⨆ (_ : i ∈ s), f i := le_ciSup_of_le houter_bdd j hinner simpa [czMeshMax, s, f] using houter

lemma czSup_neg (R : Polynomial ℝ) : czSup (-R) = czSup R := by apply congrArg sSup ext y constructor · rintro ⟨t, ht, rfl⟩ exact ⟨t, ht, by simp [czTrig_neg]⟩ · rintro ⟨t, ht, rfl⟩ exact ⟨t, ht, by simp [czTrig_neg]⟩

lemma meshParam_mem_Icc (k : ℕ) (hk : 0 < k) {j : ℕ} (hj : j ∈ range (k + 1)) : pi * j / k ∈ Icc (0 : ℝ) pi := by have hkℝ : 0 < (k : ℝ) := by exact_mod_cast hk have hkne : (k : ℝ) ≠ 0 := ne_of_gt hkℝ have hj_le : j ≤ k := Nat.le_of_lt_succ (Finset.mem_range.mp hj) constructor · positivity · calc pi * (j : ℝ) / k ≤ pi * (k : ℝ) / k := by gcongr _ = pi := by field_simp [hkne]