ZetaAppendix.lemma_aachra

@[blueprint  "lem:aachra"  (title := "Total variation of a function with monotone absolute value")  (statement := /--Let $g:[a,b]\to \mathbb{R}$ be continuous, with $|g(t)|$ non-increasing. Then$g$ is monotone, and $\|g\|_{\mathrm{TV}} = |g(a)|-|g(b)|$.-/)  (proof := /--Suppose $g$ changed sign: $g(a')>0>g(b')$ or $g(a') <0 < g(b')$ for some$a\leq a'< b'\leq b$. By IVT, there would be an $r\in [a',b']$ such that $g(r)=0$.Since $|g|$ is non-increasing, $g(b')=0$; contradiction. So, $g$ does not change sign:either $g\leq 0$ or $g\geq 0$. Thus, there is an $\varepsilon\in \{-1,1\}$ such that $g(t) = \varepsilon |g(t)|$ for all$t\in [a,b]$. Hence, $g$ is monotone. Then $\|g\|_{\mathrm{TV}} = |g(a)-g(b)|$.Since $|g(a)|\geq |g(b)|$ and $g(a)$, $g(b)$ are either both non-positive or non-negative,$|g(a)-g(b)| = |g(a)|-|g(b)|$.-/)  (latexEnv := "lemma")  (discussion := 547)]theorem lemma_aachra {a b : ℝ} (ha : a < b) (g : ℝ → ℝ)    (hg_cont : ContinuousOn g (Set.Icc a b))    (hg_mon : AntitoneOn (fun t ↦ |g t|) (Set.Icc a b)) :    BoundedVariationOn g (Set.Icc a b) ∧    (eVariationOn g (Set.Icc a b)).toReal = |g a| - |g b| := by  have h_no_sign_change : (∀ t ∈ Set.Icc a b, g t ≥ 0) ∨ (∀ t ∈ Set.Icc a b, g t ≤ 0) := by    by_contra h_contra    obtain ⟨a', b', ha', hb', hab', h_sign⟩ :        ∃ a' b' : ℝ, a ≤ a' ∧ a' < b' ∧ b' ≤ b ∧ (g a' > 0 ∧ g b' < 0) ∨        (∃ a' b' : ℝ, a ≤ a' ∧ a' < b' ∧ b' ≤ b ∧ (g a' < 0 ∧ g b' > 0)) := by      simp only [Set.mem_Icc, and_imp, not_or, not_forall, not_le, exists_and_left] at *      obtain ⟨⟨x, hx₁, hx₂, hx₃⟩, ⟨y, hy₁, hy₂, hy₃⟩⟩ := h_contra      cases lt_trichotomy x y with      | inl hxy => exact ⟨x, y, Or.inr ⟨x, hx₁, y, by grind, by grind, hx₃, hy₃⟩⟩      | inr h => cases h with        | inl heq => grind        | inr hxy => exact ⟨y, x, Or.inl ⟨by grind, hxy, by grind, hy₃, hx₃⟩⟩    · obtain ⟨c, hc⟩ : ∃ c ∈ Set.Ioo a' b', g c = 0 := by        refine intermediate_value_Ioo' (by grind) (hg_cont.mono <| Set.Icc_subset_Icc ha' hab')          ⟨?_, ?_⟩ <;> linarith [h_sign.1, h_sign.2]      have := hg_mon ⟨by linarith [hc.1.1], by linarith [hc.1.2]⟩        ⟨by linarith [hc.1.1], by linarith [hc.1.2]⟩ hc.1.2.le      aesop    · obtain ⟨a', b', ha', hb', hab', h₁, h₂⟩ := ‹_›      obtain ⟨c, hc⟩ : ∃ c ∈ Set.Ioo a' b', g c = 0 := by        apply intermediate_value_Ioo        · grind        · exact hg_cont.mono (Set.Icc_subset_Icc ha' hab')        · constructor <;> grind      have := hg_mon ⟨by linarith [hc.1.1], by linarith [hc.1.2]⟩        ⟨by linarith [hc.1.1], by linarith [hc.1.2]⟩ hc.1.2.le      simp_all  rcases h_no_sign_change with h | h  · have h_monotone : AntitoneOn g (Set.Icc a b) := fun x hx y hy hxy => by      simpa only [abs_of_nonneg (h x hx), abs_of_nonneg (h y hy)] using hg_mon hx hy hxy    have h_total_variation : eVariationOn g (Set.Icc a b) = ENNReal.ofReal (g a - g b) := by      refine le_antisymm ?_ ?_      · refine csSup_le ?_ ?_ <;> norm_num        · exact ⟨_, ⟨⟨0, ⟨fun _ ↦ a, fun _ _ _ ↦ by grind, fun _ ↦ ⟨by grind, by grind⟩⟩⟩, rfl⟩⟩        · rintro _ n x hx₁ hx₂ rfl          calc ∑ i ∈ range n, edist (g (x (i + 1))) (g (x i))              ≤ ∑ i ∈ range n, ENNReal.ofReal (g (x i) - g (x (i + 1))) := by                refine sum_le_sum (fun i _ ↦ ?_)                simp only [edist_dist, sub_nonneg, h_monotone (hx₂ i) (hx₂ (i + 1)) (hx₁ (Nat.le_succ _)),                  ENNReal.ofReal_le_ofReal_iff]                rw [dist_eq_norm, Real.norm_of_nonpos] <;>                linarith [h_monotone (hx₂ i) (hx₂ (i + 1)) (hx₁ (Nat.le_succ _))]            _ ≤ ENNReal.ofReal (g a - g b) := by                rw [← ENNReal.ofReal_sum_of_nonneg] <;> norm_num                · apply ENNReal.ofReal_le_ofReal                  have := sum_range_sub' (fun i ↦ g (x i)) n                  norm_num at *                  linarith [h_monotone ⟨le_refl a, ha.le⟩ (hx₂ 0) (by linarith [hx₂ 0]),                    h_monotone (hx₂ n) ⟨ha.le, le_refl b⟩ (by linarith [hx₂ n])]                · exact fun i hi ↦ h_monotone (hx₂ i) (hx₂ (i + 1)) (hx₁ (Nat.le_succ _))      · refine le_csSup ?_ ?_ <;> norm_num        refine ⟨1, fun i ↦ if i = 0 then a else b, ?_, ?_⟩ <;> norm_num [Monotone]        · grind        · simp only [edist_dist, dist_eq_norm, norm_eq_abs, abs_sub_comm, abs_of_nonneg            (sub_nonneg.mpr (h_monotone (Set.left_mem_Icc.mpr ha.le) (Set.right_mem_Icc.mpr ha.le) ha.le))]    rw [h_total_variation, ENNReal.toReal_ofReal]    · constructor      · exact ne_of_lt <| lt_of_le_of_lt h_total_variation.le ENNReal.ofReal_lt_top      · rw [abs_of_nonneg <| h a <| Set.left_mem_Icc.mpr ha.le,            abs_of_nonneg <| h b <| Set.right_mem_Icc.mpr ha.le]    · linarith [h_monotone (Set.left_mem_Icc.mpr ha.le) (Set.right_mem_Icc.mpr ha.le) ha.le]  · have h_monotone : MonotoneOn g (Set.Icc a b) := fun x hx y hy hxy ↦ by have := hg_mon hx hy hxy; grind    have h_bounded_variation : eVariationOn g (Set.Icc a b) = ENNReal.ofReal (g b - g a) := by      refine le_antisymm ?_ ?_      · refine csSup_le ?_ ?_ <;> norm_num        · exact ⟨_, ⟨⟨0, ⟨fun _ ↦ a, fun _ _ _ ↦ by grind, fun _ ↦ ⟨by grind, by grind⟩⟩⟩, rfl⟩⟩        · rintro _ n x hx₁ hx₂ rfl          calc ∑ i ∈ range n, edist (g (x (i + 1))) (g (x i))              ≤ ∑ i ∈ range n, ENNReal.ofReal (g (x (i + 1)) - g (x i)) := by                refine sum_le_sum (fun i _ ↦ ?_)                rw [edist_dist, dist_eq_norm, Real.norm_of_nonneg (sub_nonneg.mpr (h_monotone (hx₂ _)                  (hx₂ _) (hx₁ (Nat.le_succ _))))]            _ ≤ ENNReal.ofReal (g b - g a) := by                rw [← ENNReal.ofReal_sum_of_nonneg]                · rw [sum_range_sub (fun i ↦ g (x i))]                  apply ENNReal.ofReal_le_ofReal                  have hx0_mem : x 0 ∈ Set.Icc a b := ⟨by linarith [hx₂ 0], by linarith [hx₂ 0]⟩                  have hxn_mem : x n ∈ Set.Icc a b := ⟨by linarith [hx₂ n], by linarith [hx₂ n]⟩                  linarith [h_monotone ⟨le_refl a, ha.le⟩ hx0_mem (by linarith [hx₂ 0]),                    h_monotone hxn_mem ⟨ha.le, le_refl b⟩ (by linarith [hx₂ n])]                · exact fun i hi ↦ sub_nonneg_of_le <| h_monotone (hx₂ _) (hx₂ _) <| hx₁ <| Nat.le_succ _      · refine le_csSup ?_ ?_ <;> norm_num        refine ⟨1, fun i ↦ if i = 0 then a else b, ?_, ?_⟩ <;> norm_num [Monotone]        · grind        · simp [edist_dist, Real.dist_eq, abs_of_nonneg, h_monotone (show a ∈ Set.Icc a b by            constructor <;> grind) (show b ∈ Set.Icc a b by constructor <;> grind) ha.le]    simp_all only [Set.mem_Icc, and_imp]    constructor    · rw [BoundedVariationOn]      exact ne_of_lt (lt_of_le_of_lt h_bounded_variation.le ENNReal.ofReal_lt_top)    · rw [ENNReal.toReal_ofReal (sub_nonneg.mpr (h_monotone ⟨by grind, by grind⟩ ⟨by grind, by grind⟩ ha.le)),        abs_of_nonpos (h a le_rfl ha.le), abs_of_nonpos (h b ha.le le_rfl)]      ring