Theory Youngs

section ‹Young's Inequality for Increasing Functions›

text ‹From the following paper: 
Cunningham, F., and Nathaniel Grossman. ``On Young's Inequality.'' 
The American Mathematical Monthly 78, no. 7 (1971): 781--83. 
\url{https://doi.org/10.2307/2318018}›

theory Youngs imports
  "HOL-Analysis.Analysis" 
   
begin

subsection ‹Toward Young's inequality›

lemma strict_mono_image_endpoints:
  fixes f :: "'a::linear_continuum_topology ⇒ 'b::linorder_topology"
  assumes "strict_mono_on {a..b} f" and f: "continuous_on {a..b} f" and "a ≤ b"
  shows "f ` {a..b} = {f a..f b}"
proof
  show "f ` {a..b} ⊆ {f a..f b}"
    using assms(1) strict_mono_on_leD by fastforce
  show "{f a..f b} ⊆ f ` {a..b}"
    using assms IVT'[OF _ _ _ f] by (force simp: Bex_def)
qed

text ‹Generalisations of the type of @{term f} are not obvious›
lemma strict_mono_continuous_invD:
  fixes f :: "real ⇒ real"
  assumes sm: "strict_mono_on {a..} f" and contf: "continuous_on {a..} f" 
    and fim: "f ` {a..} = {f a..}" and g: "⋀x. x ≥ a ⟹ g (f x) = x"
  shows "continuous_on {f a..} g"
proof (clarsimp simp add: continuous_on_eq_continuous_within)
  fix y
  assume "f a ≤ y"
  then obtain u where u: "y+1 = f u" "u ≥ a"
    by (smt (verit, best) atLeast_iff fim imageE)
  have "continuous_on {f a..y+1} g" 
  proof -
    obtain "continuous_on {a..u} f"  "strict_mono_on {a..u} f"
      using contf sm continuous_on_subset by (force simp add: strict_mono_on_def)
    moreover have "continuous_on (f ` {a..u}) g"
      using assms continuous_on_subset
      by (intro continuous_on_inv) fastforce+
    ultimately show ?thesis
      using strict_mono_image_endpoints [of _ _ f]
      by (simp add: strict_mono_image_endpoints u)
  qed
  then have *: "continuous (at y within {f a..y+1}) g"
    by (simp add: ‹f a ≤ y› continuous_on_imp_continuous_within)
  show "continuous (at y within {f a..}) g"
  proof (clarsimp simp add: continuous_within_topological Ball_def)
    fix B
    assume "open B" and "g y ∈ B"
    with * obtain A where A: "open A" "y ∈ A" and "⋀x. f a ≤ x ∧ x ≤ y+1 ⟹ x ∈ A ⟶ g x ∈ B"
      by (force simp: continuous_within_topological)
    then have "∀x≥f a. x ∈ A ∩ ball y 1 ⟶ g x ∈ B"
      by (smt (verit, ccfv_threshold) IntE dist_norm mem_ball real_norm_def)
    then show "∃A. open A ∧ y ∈ A ∧ (∀x≥f a. x ∈ A ⟶ g x ∈ B)"
      by (metis Elementary_Metric_Spaces.open_ball Int_iff A centre_in_ball open_Int zero_less_one)
  qed
qed

subsection ‹Regular divisions›

text ‹Our lack of the Riemann integral forces us to construct explicitly
the step functions mentioned in the text.›

definition "segment ≡ λn k. {real k / real n..(1 + k) / real n}"

lemma segment_nonempty: "segment n k ≠ {}"
  by (auto simp: segment_def divide_simps)

lemma segment_Suc: "segment n ` {..<Suc k} = insert {k/n..(1 + real k) / n} (segment n ` {..<k})"
  by (simp add: segment_def lessThan_Suc)

lemma Union_segment_image: "⋃ (segment n ` {..<k}) = (if k=0 then {} else {0..real k/real n})"
proof (induction k)
  case (Suc k)
  then show ?case
    by (simp add: divide_simps segment_Suc Un_commute ivl_disj_un_two_touch split: if_split_asm)
qed (auto simp: segment_def)

definition "segments ≡ λn. segment n ` {..<n}"

lemma card_segments [simp]: "card (segments n) = n"
  by (simp add: segments_def segment_def card_image divide_right_mono inj_on_def)

lemma segments_0 [simp]: "segments 0 = {}"
  by (simp add: segments_def)

lemma Union_segments: "⋃ (segments n) = (if n=0 then {} else {0..1})"
  by (simp add: segments_def Union_segment_image)

definition "regular_division ≡ λa b n. (image ((+) a ∘ (*) (b-a))) ` (segments n)"

lemma translate_scale_01:
  assumes "a ≤ b" 
  shows "(λx. a + (b - a) * x) ` {0..1} = {a..b::real}"
  using closed_segment_real_eq [of a b] assms closed_segment_eq_real_ivl by auto

lemma finite_regular_division [simp]: "finite (regular_division a b n)"
  by (simp add: regular_division_def segments_def)

lemma card_regular_division [simp]: 
  assumes "a<b"
  shows "card (regular_division a b n) = n"
proof -
  have "inj_on ((`) ((+) a ∘ (*) (b - a))) (segments n)"
  proof
    fix x y
    assume "((+) a ∘ (*) (b - a)) ` x = ((+) a ∘ (*) (b - a)) ` y"
    then have "(+) (-a) ` ((+) a ∘ (*) (b - a)) ` x = (+) (-a) ` ((+) a ∘ (*) (b - a)) ` y"
      by simp
    then have "((*) (b - a)) ` x = ((*) (b - a)) ` y"
      by (simp add: image_comp)
    then have "(*) (inverse(b - a)) ` (*) (b - a) ` x = (*) (inverse(b - a)) ` (*) (b - a) ` y"
      by simp
    then show "x = y"
      using assms by (simp add: image_comp mult_ac)
  qed
  then show ?thesis
    by (metis card_image card_segments regular_division_def)
qed

lemma Union_regular_division:
  assumes "a ≤ b" 
  shows "⋃(regular_division a b n) = (if n=0 then {} else {a..b})"
  using assms
  by (auto simp: regular_division_def Union_segments translate_scale_01 simp flip: image_Union)

lemma regular_division_eqI:
  assumes K: "K = {a + (b-a)*(real k / n) .. a + (b-a)*((1 + real k) / n)}"
    and "a<b" "k < n"
  shows "K ∈ regular_division a b n" 
  unfolding regular_division_def segments_def image_comp
proof
  have "K = (λx. (b-a) * x + a) ` {real k / real n..(1 + real k) / real n}"
    using K ‹a<b› by (simp add: image_affinity_atLeastAtMost divide_simps)
  then show "K = ((`) ((+) a ∘ (*) (b - a)) ∘ segment n) k" 
    by (simp add: segment_def add.commute)
qed (use assms in auto)

lemma regular_divisionE:
  assumes "K ∈ regular_division a b n" "a<b"
  obtains k where "k<n" "K = {a + (b-a)*(real k / n) .. a + (b-a)*((1 + real k) / n)}"
proof -
  have eq: "(λx. a + (b - a) * x) = (λx. a + x) ∘ (λx. (b - a) * x)"
    by (simp add: o_def)
  obtain k where "k<n" "K = ((λx. a+x) ∘ (λx. (b-a) * x)) ` {k/n .. (1 + real k) / n}"
    using assms by (auto simp: regular_division_def segments_def segment_def)
  with that ‹a<b› show ?thesis
    unfolding image_comp [symmetric]  by auto
qed

lemma regular_division_division_of:
  assumes "a < b" "n>0"
  shows "(regular_division a b n) division_of {a..b}"
proof (rule division_ofI)
  show "finite (regular_division a b n)"
    by (simp add: regular_division_def segments_def)
  show §: "⋃ (regular_division a b n) = {a..b}"
    using Union_regular_division assms by simp
  fix K
  assume K: "K ∈ regular_division a b n"
  then obtain k where Keq: "K = {a + (b-a)*(k/n) .. a + (b-a)*((1 + real k) / n)}" 
    using ‹a<b› regular_divisionE by meson
  show "K ⊆ {a..b}"
    using K Union_regular_division ‹n>0› by (metis Union_upper §)
  show "K ≠ {}"
    using K by (auto simp: regular_division_def segment_nonempty segments_def)
  show "∃a b. K = cbox a b"
    by (metis K ‹a<b› box_real(2) regular_divisionE)
  fix K'
  assume K': "K' ∈ regular_division a b n" and "K ≠ K'"
  then obtain k' where Keq': "K' = {a + (b-a)*(k'/n) .. a + (b-a)*((1 + real k') / n)}" 
    using K ‹a<b› regular_divisionE by meson
  consider "1 + real k ≤ k'" | "1 + real k' ≤ k"
    using Keq Keq' ‹K ≠ K'› by force
  then show "interior K ∩ interior K' = {}"
  proof cases
    case 1
    then show ?thesis
      by (simp add: Keq Keq' min_def max_def divide_right_mono assms)
  next
    case 2
    then have "interior K' ∩ interior K = {}"
      by (simp add: Keq Keq' min_def max_def divide_right_mono assms)
    then show ?thesis
      by (simp add: inf_commute)
  qed
qed

subsection ‹Special cases of Young's inequality›

lemma weighted_nesting_sum:
  fixes g :: "nat ⇒ 'a::comm_ring_1"
  shows "(∑k<n. (1 + of_nat k) * (g (Suc k) - g k)) = of_nat n * g n - (∑i<n. g i)"
  by (induction n) (auto simp: algebra_simps)

theorem Youngs_exact:
  fixes f :: "real ⇒ real"
  assumes sm: "strict_mono_on {0..} f" and cont: "continuous_on {0..} f" and a: "a≥0" 
    and f: "f 0 = 0" "f a = b"
    and g: "⋀x. ⟦0 ≤ x; x ≤ a⟧ ⟹ g (f x) = x"
  shows "a*b = integral {0..a} f + integral {0..b} g" 
proof (cases "a=0")
  case False
  with ‹a ≥ 0› have "a > 0" by linarith
  then have "b ≥ 0"
    by (smt (verit, best) atLeast_iff f sm strict_mono_onD)
  have sm_0a: "strict_mono_on {0..a} f"
    by (metis atLeastAtMost_iff atLeast_iff sm strict_mono_on_def)
  have cont_0a: "continuous_on {0..a} f"
    using cont continuous_on_subset by fastforce
  with sm_0a have "continuous_on {0..b} g"
    by (metis a atLeastAtMost_iff compact_Icc continuous_on_inv f g strict_mono_image_endpoints)
  then have intgb_g: "g integrable_on {0..b}"
    using integrable_continuous_interval by blast
  have intgb_f: "f integrable_on {0..a}"
    using cont_0a integrable_continuous_real by blast

  have f_iff [simp]: "f x < f y ⟷ x < y" "f x ≤ f y ⟷ x ≤ y"
    if "x ≥ 0" "y ≥ 0" for x y
    using that by (smt (verit, best) atLeast_iff sm strict_mono_onD)+
  have fim: "f ` {0..a} = {0..b}"
    by (simp add: ‹a ≥ 0› cont_0a strict_mono_image_endpoints strict_mono_on_def f)
  have "uniformly_continuous_on {0..a} f"
    using compact_uniformly_continuous cont_0a by blast
  then obtain del where del_gt0: "⋀e. e>0 ⟹ del e > 0" 
        and del:  "⋀e x x'. ⟦¦x'-x¦ < del e; e>0; x ∈ {0..a}; x' ∈ {0..a}⟧ ⟹ ¦f x' - f x¦ < e"
    unfolding uniformly_continuous_on_def dist_real_def by metis

  have *: "¦a * b - integral {0..a} f - integral {0..b} g¦ < 2*ε" if "ε > 0" for ε
  proof -
    define δ where "δ = min a (del (ε/a)) / 2"
    have "δ > 0" "δ ≤ a"
      using ‹a > 0› ‹ε > 0› del_gt0 by (auto simp: δ_def)
    define n where "n ≡ nat⌊a / δ⌋"
    define a_seg where "a_seg ≡ λu::real. u * a/n"
    have "n > 0"
      using  ‹a > 0› ‹δ > 0› ‹δ ≤ a› by (simp add: n_def)
    have a_seg_ge_0 [simp]: "a_seg x ≥ 0 ⟷ x ≥ 0" 
     and a_seg_le_a [simp]: "a_seg x ≤ a ⟷ x ≤ n" for x
      using ‹n > 0› ‹a > 0› by (auto simp: a_seg_def zero_le_mult_iff divide_simps)
    have a_seg_le_iff [simp]: "a_seg x ≤ a_seg y ⟷ x ≤ y" 
      and a_seg_less_iff [simp]: "a_seg x < a_seg y ⟷ x < y" for x y
      using ‹n > 0› ‹a > 0› by (auto simp: a_seg_def zero_le_mult_iff divide_simps)
    have "strict_mono a_seg"
      by (simp add: strict_mono_def)
    have a_seg_eq_a_iff: "a_seg x = a ⟷ x=n" for x
      using ‹0 < n› ‹a > 0› by (simp add: a_seg_def nonzero_divide_eq_eq)
    have fa_eq_b: "f (a_seg n) = b"
      using a_seg_eq_a_iff f by fastforce

    have "a/d < real_of_int ⌊a * 2 / min a d⌋" if "d>0" for d
      by (smt (verit) ‹0 < δ› ‹δ ≤ a› add_divide_distrib divide_less_eq_1_pos floor_eq_iff that)
    then have an_less_del: "a/n < del (ε/a)"
      using ‹a > 0› ‹ε > 0› del_gt0  by (simp add: n_def δ_def field_simps)

    define lower where "lower ≡ λx. a_seg⌊(real n * x) / a⌋"
    define f1 where "f1 ≡ f ∘ lower"
    have f1_lower: "f1 x ≤ f x" if "0 ≤ x" "x ≤ a" for x
    proof -
      have "lower x ≤ x"
        using ‹n > 0› floor_divide_lower [OF ‹a > 0›] 
        by (auto simp: lower_def a_seg_def field_simps)
      moreover have "lower x ≥ 0"
        unfolding lower_def using ‹n > 0› ‹a ≥ 0› ‹0 ≤ x› by force
      ultimately show ?thesis
        using sm strict_mono_on_leD by (fastforce simp add: f1_def)
    qed
    define upper where "upper ≡ λx. a_seg⌈real n * x / a⌉"
    define f2 where "f2 ≡ f ∘ upper"
    have f2_upper: "f2 x ≥ f x" if "0 ≤ x" "x ≤ a" for x
    proof -
      have "x ≤ upper x"
        using ‹n > 0› ceiling_divide_upper [OF ‹a > 0›] by (simp add: upper_def a_seg_def field_simps)
      then show ?thesis
        using sm strict_mono_on_leD ‹0 ≤ x› by (force simp: f2_def)
    qed
    let ?𝒟 = "regular_division 0 a n"
    have div: "?𝒟 division_of {0..a}"
      using ‹a > 0› ‹n > 0› regular_division_division_of zero_less_nat_eq by presburger

    have int_f1_D: "(f1 has_integral f(Inf K) * (a/n)) K" 
      and int_f2_D: "(f2 has_integral f(Sup K) * (a/n)) K" and less: "¦f(Sup K) - f(Inf K)¦ < ε/a"
      if "K∈?𝒟" for K
    proof -
      from regular_divisionE [OF that] ‹a > 0›
      obtain k where "k<n" and k: "K = {a_seg(real k)..a_seg(Suc k)}"
        by (auto simp: a_seg_def mult.commute)
      define u where "u ≡ a_seg k"
      define v where "v ≡ a_seg (Suc k)"
      have "u < v" "0 ≤ u" "0 ≤ v" "u ≤ a" "v ≤ a" and Kuv: "K = {u..v}"
        using ‹n > 0› ‹k < n› ‹a > 0› by (auto simp: k u_def v_def divide_simps)
      have InfK: "Inf K = u" and SupK: "Sup K = v"
        using Kuv ‹u < v› apply force
        using ‹n > 0› ‹a > 0› by (auto simp: divide_right_mono k u_def v_def)
      have f1: "f1 x = f (Inf K)" if "x ∈ K - {v}" for x
      proof -
        have "x ∈ {u..<v}"
          using that Kuv atLeastLessThan_eq_atLeastAtMost_diff by blast
        then have "⌊real_of_int n * x / a⌋ = int k"
          using ‹n > 0› ‹a > 0› by (simp add: field_simps u_def v_def a_seg_def floor_eq_iff)
        then show ?thesis
          by (simp add: InfK f1_def lower_def a_seg_def mult.commute u_def) 
      qed
      have "((λx. f (Inf K)) has_integral (f (Inf K) * (a/n))) K"
        using has_integral_const_real [of "f (Inf K)" u v] 
              ‹n > 0› ‹a > 0› by (simp add: Kuv field_simps a_seg_def u_def v_def)
      then show "(f1 has_integral (f (Inf K) * (a/n))) K"
        using has_integral_spike_finite_eq [of "{v}" K "λx. f (Inf K)" f1] f1 by simp
      have f2: "f2 x = f (Sup K)" if "x ∈ K - {u}" for x
      proof -
        have "x ∈ {u<..v}"
          using that Kuv greaterThanAtMost_eq_atLeastAtMost_diff by blast 
        then have "⌈x * real_of_int n / a⌉  = 1 + int k"
          using ‹n > 0› ‹a > 0› by (simp add: field_simps u_def v_def a_seg_def ceiling_eq_iff)
        then show ?thesis 
          by (simp add: mult.commute f2_def upper_def a_seg_def SupK v_def)
      qed
      have "((λx. f (Sup K)) has_integral (f (Sup K) * (a/n))) K"
        using  ‹n > 0› ‹a > 0› has_integral_const_real [of "f (Sup K)" u v]
        by (simp add: Kuv field_simps u_def v_def a_seg_def)
      then show "(f2 has_integral (f (Sup K) * (a/n))) K"
        using has_integral_spike_finite_eq [of "{u}" K "λx. f (Sup K)" f2] f2 by simp
      have "¦v - u¦ < del (ε/a)"
        using ‹n > 0› ‹a > 0› by (simp add: v_def u_def a_seg_def field_simps an_less_del)
      then have "¦f v - f u¦ < ε/a"
        using ‹ε > 0› ‹a > 0› ‹0 ≤ u› ‹u ≤ a› ‹0 ≤ v› ‹v ≤ a›
        by (intro del) auto
      then show "¦f(Sup K) - f(Inf K)¦ < ε/a"
        using InfK SupK by blast
    qed

    have int_21_D: "((λx. f2 x - f1 x) has_integral (f(Sup K) - f(Inf K)) * (a/n)) K" if "K∈?𝒟" for K
      using that has_integral_diff [OF int_f2_D int_f1_D] by (simp add: algebra_simps)

    have D_ne: "?𝒟 ≠ {}"
      by (metis ‹0 < a› ‹n > 0› card_gt_0_iff card_regular_division)
    have f12: "((λx. f2 x - f1 x) has_integral (∑K∈?𝒟. (f(Sup K) - f(Inf K)) * (a/n))) {0..a}"
      by (intro div int_21_D has_integral_combine_division)
    moreover have "(∑K∈?𝒟. (f(Sup K) - f(Inf K)) * (a/n)) < ε"
    proof -
      have "(∑K∈?𝒟. (f(Sup K) - f(Inf K)) * (a/n)) ≤ (∑K∈?𝒟. ¦f(Sup K) - f(Inf K)¦ * (a/n))"
        using ‹n > 0› ‹a > 0›
        by (smt (verit) divide_pos_pos of_nat_0_less_iff sum_mono zero_le_mult_iff)
      also have "… < (∑K∈?𝒟. ε/n)"
        using ‹n > 0› ‹a > 0› less
        by (intro sum_strict_mono finite_regular_division D_ne) (simp add: field_simps)
      also have "… = ε"
        using ‹n > 0› ‹a > 0› by simp
      finally show ?thesis .
    qed
    ultimately have f2_near_f1: "integral {0..a} (λx. f2 x - f1 x) < ε"
      by (simp add: integral_unique)

    define yidx where "yidx ≡ λy. LEAST k. y < f (a_seg (Suc k))"
    have fa_yidx_le: "f (a_seg (yidx y)) ≤ y" and yidx_gt: "y < f (a_seg (Suc (yidx y)))" 
      if "y ∈ {0..b}" for y
    proof -
      obtain x where x: "f x = y" "x ∈ {0..a}"
        using Topological_Spaces.IVT' [OF _ _ _ cont_0a] assms
        by (metis ‹y ∈ {0..b}› atLeastAtMost_iff)
      define k where "k ≡ nat ⌊x/a * n⌋"
      have x_lims: "a_seg k ≤ x" "x < a_seg (Suc k)"
        using ‹n > 0› ‹0 < a› floor_divide_lower floor_divide_upper [of a "x*n"] x
        by (auto simp: k_def a_seg_def field_simps)
      with that x obtain f_lims: "f (a_seg k) ≤ y" "y < f (a_seg (Suc k))"
        using strict_mono_onD [OF sm] by force
      then have "a_seg (yidx y) ≤ a_seg k"
        by (simp add: Least_le ‹strict_mono a_seg› strict_mono_less_eq yidx_def)
      then have "f (a_seg (yidx y)) ≤ f (a_seg k)"
        using strict_mono_onD [OF sm] by simp
      then show "f (a_seg (yidx y)) ≤ y"
        using f_lims by linarith
      show "y < f (a_seg (Suc (yidx y)))"
        by (metis LeastI f_lims(2) yidx_def) 
    qed

    have yidx_equality: "yidx y = k" if "y ∈ {0..b}" "y ∈ {f (a_seg k)..<f (a_seg (Suc k))}" for y k
    proof (rule antisym)
      show "yidx y ≤ k"
        unfolding yidx_def by (metis atLeastLessThan_iff that(2) Least_le)
      have "(a_seg (real k)) < a_seg (1 + real (yidx y))"
        using yidx_gt [OF that(1)] that(2) strict_mono_onD [OF sm] order_le_less_trans by fastforce
      then have "real k < 1 + real (yidx y)"
        by (simp add: ‹strict_mono a_seg› strict_mono_less)
      then show "k ≤ yidx y"
        by simp 
    qed
    have "yidx b = n"
    proof -
      have "a < (1 + real n) * a / real n"
        using ‹0 < n› ‹0 < a› by (simp add: divide_simps)
      then have "b < f (a_seg (1 + real n))"
        using f ‹a ≥ 0› a_seg_def sm strict_mono_onD by fastforce
      then show ?thesis
        using ‹0 ≤ b› by (auto simp: f a_seg_def yidx_equality)
    qed
    moreover have yidx_less_n: "yidx y < n" if "y < b" for y
      by (metis ‹0 < n› fa_eq_b gr0_conv_Suc less_Suc_eq_le that Least_le yidx_def)
    ultimately have yidx_le_n: "yidx y ≤ n" if "y ≤ b" for y
      by (metis dual_order.order_iff_strict that)

    have zero_to_b_eq: "{0..b} = (⋃k<n. {f(a_seg k)..f(a_seg (Suc k))})" (is "?lhs = ?rhs")
    proof
      show "?lhs ⊆ ?rhs"
      proof
        fix y assume y: "y ∈ {0..b}"
        have fn: "f (a_seg n) = b"
          using a_seg_eq_a_iff ‹f a = b› by fastforce
        show "y ∈ ?rhs"
        proof (cases "y=b")
          case True
          with fn ‹n>0› show ?thesis
            by (rule_tac a="n-1" in UN_I) auto
        next
          case False
          with y show ?thesis 
            apply (simp add: subset_iff Bex_def)
            by (metis atLeastAtMost_iff of_nat_Suc order_le_less yidx_gt fa_yidx_le yidx_less_n)
        qed
      qed
      show "?rhs ⊆ ?lhs"
        apply clarsimp
        by (smt (verit, best) a_seg_ge_0 a_seg_le_a f f_iff(2) nat_less_real_le of_nat_0_le_iff)
    qed

    define g1 where "g1 ≡ λy. if y=b then a else a_seg (Suc (yidx y))"
    define g2 where "g2 ≡ λy. if y=0 then 0 else a_seg (yidx y)"
    have g1: "g1 y ∈ {0..a}" if "y ∈ {0..b}" for y
      using that ‹a > 0› yidx_less_n [of y] by (auto simp: g1_def a_seg_def divide_simps)
    have g2: "g2 y ∈ {0..a}" if "y ∈ {0..b}" for y
      using that ‹a > 0› yidx_le_n [of y] by (simp add: g2_def a_seg_def divide_simps)

    have g2_le_g: "g2 y ≤ g y" if "y ∈ {0..b}" for y
    proof -
      have "f (g2 y) ≤ y"
        using ‹f 0 = 0› g2_def that fa_yidx_le by presburger
      then have "f (g2 y) ≤ f (g y)"
        using that g by (smt (verit, best) atLeastAtMost_iff fim image_iff)
      then show ?thesis
        by (smt (verit, best) atLeastAtMost_iff fim g g2 imageE sm_0a strict_mono_onD that)
    qed
    have g_le_g1: "g y ≤ g1 y" if "y ∈ {0..b}" for y
    proof -
      have "y ≤ f (g1 y)"
        by (smt (verit, best) ‹f a = b› g1_def that yidx_gt)
      then have "f (g y) ≤ f (g1 y)"
        using that g by (smt (verit, best) atLeastAtMost_iff fim image_iff)
      then show ?thesis
        by (smt (verit, ccfv_threshold) atLeastAtMost_iff f_iff(1) g1 that)
    qed

    define DN where "DN ≡ λK. nat ⌊Inf K * real n / a⌋"
    have [simp]: "DN {a * real k / n..a * (1 + real k) / n} = k" for k
      using ‹n > 0› ‹a > 0› by (simp add: DN_def divide_simps)
    have DN: "bij_betw DN ?𝒟 {..<n}"
    proof (intro bij_betw_imageI)
      show "inj_on DN (regular_division 0 a n)"
      proof
        fix K K'
        assume "K ∈ regular_division 0 a n"
        with ‹a > 0› obtain k where k: "K = {a * (real k / n) .. a * (1 + real k) / n}"
          by (force elim: regular_divisionE)
        assume "K' ∈ regular_division 0 a n"
        with ‹a > 0› obtain k' where k': "K' = {a * (real k' / n) .. a * (1 + real k') / n}"
          by (force elim: regular_divisionE)
        assume "DN K = DN K'"
        then show "K = K'" by (simp add: k k')
      qed
      have "∃K∈regular_division 0 a n. k = nat ⌊Inf K * real n / a⌋" if "k < n" for k
        using ‹n > 0› ‹a > 0› that
        by (force simp: divide_simps intro: regular_division_eqI [OF refl])
      with ‹a>0› show "DN ` regular_division 0 a n = {..<n}"
        by (auto simp: DN_def bij_betw_def image_iff frac_le elim!: regular_divisionE)
    qed
 
    have int_f1: "(f1 has_integral (∑k<n. f(a_seg k)) * (a/n)) {0..a}"
    proof -
      have "a_seg (real (DN K)) = Inf K" if "K ∈ ?𝒟" for K
        using that ‹a>0› by (auto simp: DN_def field_simps a_seg_def elim: regular_divisionE)
      then have "(∑K∈?𝒟. f(Inf K) * (a/n)) = (∑k<n. (f(a_seg k)) * (a/n))"
        by (simp flip: sum.reindex_bij_betw [OF DN])
      moreover have "(f1 has_integral (∑K∈?𝒟. f(Inf K) * (a/n))) {0..a}"
        by (intro div int_f1_D has_integral_combine_division)
      ultimately show ?thesis
        by (metis sum_distrib_right)
    qed
    text ‹The claim @{term "(f2 has_integral (∑k<n. f(a_seg(Suc k))) * (a/n)) {0..a}"} can similarly be proved›

    have int_g1_D: "(g1 has_integral a_seg (Suc k) * (f (a_seg (Suc k)) - f (a_seg k))) 
                    {f(a_seg k)..f(a_seg (Suc k))}" 
     and int_g2_D: "(g2 has_integral a_seg k * (f (a_seg (Suc k)) - f (a_seg k))) 
                    {f(a_seg k)..f(a_seg (Suc k))}" 
      if "k < n" for k
    proof -
      define u where "u ≡ f (a_seg k)"
      define v where "v ≡ f (a_seg (Suc k))"
      obtain "u < v" "0 ≤ u" "0 ≤ v"
        unfolding u_def v_def assms
        by (smt (verit, best) a_seg_ge_0 a_seg_le_iff f(1) f_iff(1) of_nat_0_le_iff of_nat_Suc)
      have "u ≤ b" "v ≤ b"
        using ‹k < n› ‹a ≥ 0› by (simp_all add: u_def v_def flip: ‹f a = b›)
      have yidx_eq: "yidx x = k" if "x ∈ {u..<v}" for x
        using ‹0 ≤ u› ‹v ≤ b› that u_def v_def yidx_equality by auto

      have "g1 x = a_seg (Suc k)" if "x ∈ {u..<v}" for x
        using that ‹v ≤ b› by (simp add: g1_def yidx_eq)
      moreover have "((λx. a_seg (Suc k)) has_integral (a_seg (Suc k) * (v-u))) {u..v}"
        using has_integral_const_real ‹u < v›
        by (metis content_real_if less_eq_real_def mult.commute real_scaleR_def)
      ultimately show "(g1 has_integral (a_seg (Suc k) * (v-u))) {u..v}"
        using has_integral_spike_finite_eq [of "{v}" "{u..v}" "λx. a_seg (Suc k)" g1] by simp

      have g2: "g2 x = a_seg k" if "x ∈ {u<..<v}" for x
        using that ‹0 ≤ u› by (simp add: g2_def yidx_eq)
      moreover have "((λx. a_seg k) has_integral (a_seg k * (v-u))) {u..v}"
        using has_integral_const_real ‹u < v›
        by (metis content_real_if less_eq_real_def mult.commute real_scaleR_def)
      ultimately show "(g2 has_integral (a_seg k * (v-u))) {u..v}"
        using has_integral_spike_finite_eq [of "{u,v}" "{u..v}" "λx. a_seg k" g2] by simp
    qed

    have int_g1: "(g1 has_integral (∑k<n. a_seg (Suc k) * (f (a_seg (Suc k)) - f (a_seg k)))) {0..b}"
    and int_g2: "(g2 has_integral (∑k<n. a_seg k * (f (a_seg (Suc k)) - f (a_seg k)))) {0..b}"
      unfolding zero_to_b_eq using int_g1_D int_g2_D
      by (auto simp: min_def pairwise_def intro!: has_integral_UN negligible_atLeastAtMostI)

    have "(∑k<n. a_seg (Suc k) * (f (a_seg (Suc k)) - f (a_seg k)))
        = (∑k<n. (Suc k) * (f (a_seg (Suc k)) - f (a_seg k))) * (a/n)"
      unfolding a_seg_def sum_distrib_right sum_divide_distrib by (simp add: mult_ac)
    also have "… = (n * f (a_seg n) - (∑k<n. f (a_seg k))) * a / n"
      using weighted_nesting_sum [where g = "f o a_seg"] by simp
    also have "… = a * b - (∑k<n. f (a_seg k)) * a / n"
      using ‹n > 0› by (simp add: fa_eq_b field_simps)
    finally have int_g1': "(g1 has_integral a * b - (∑k<n. f (a_seg k)) * a / n) {0..b}"
      using int_g1 by simp
    text ‹The claim @{term "(g2 has_integral a * b - (∑k<n. f (a_seg (Suc k))) * a / n) {0..b}"} can similarly be proved.› 

    have a_seg_diff: "a_seg (Suc k) - a_seg k = a/n" for k
      by (simp add: a_seg_def field_split_simps)
    have f_a_seg_diff: "¦f (a_seg (Suc k)) - f (a_seg k)¦ < ε/a" if "k<n" for k
      using that ‹a > 0› a_seg_diff an_less_del ‹ε > 0›
      by (intro del) auto

    have "((λx. g1 x - g2 x) has_integral (∑k<n. (f (a_seg (Suc k)) - f (a_seg k)) * (a/n))) {0..b}"
      using has_integral_diff [OF int_g1 int_g2] a_seg_diff
      apply (simp flip: sum_subtractf left_diff_distrib)
      apply (simp add: field_simps)
      done
    moreover have "(∑k<n. (f (a_seg (Suc k)) - f (a_seg k)) * (a/n)) < ε"
    proof -
      have "(∑k<n. (f (a_seg (Suc k)) - f (a_seg k)) * (a/n)) 
         ≤ (∑k<n. ¦f (a_seg (Suc k)) - f (a_seg k)¦ * (a/n))"
        by simp
      also have "… < (∑k<n. (ε/a) * (a/n))"
      proof (rule sum_strict_mono)
        fix k assume "k ∈ {..<n}"
        with ‹n > 0› ‹a > 0› divide_strict_right_mono f_a_seg_diff pos_less_divide_eq
        show "¦f (a_seg (Suc k)) - f (a_seg k)¦ * (a/n) < ε/a * (a/n)" by fastforce
      qed (use ‹n > 0› in auto)
      also have "… = ε"
        using ‹n > 0› ‹a > 0› by simp
      finally show ?thesis .
    qed
    ultimately have g2_near_g1: "integral {0..b} (λx. g1 x - g2 x) < ε"
      by (simp add: integral_unique)

    have ab1: "integral {0..a} f1 + integral {0..b} g1 = a*b"
      using int_f1 int_g1' by (simp add: integral_unique)

    have "integral {0..a} (λx. f x - f1 x) ≤ integral {0..a} (λx. f2 x - f1 x)"
    proof (rule integral_le)
      show "(λx. f x - f1 x) integrable_on {0..a}" "(λx. f2 x - f1 x) integrable_on {0..a}"
        using Henstock_Kurzweil_Integration.integrable_diff int_f1 intgb_f f12 by blast+
    qed (auto simp: f2_upper)
    with f2_near_f1 have "integral {0..a} (λx. f x - f1 x) < ε"
      by simp
    moreover have "integral {0..a} f1 ≤ integral {0..a} f"
      by (intro integral_le has_integral_integral intgb_f has_integral_integrable [OF int_f1]) 
         (simp add: f1_lower)
    ultimately have f_error: "¦integral {0..a} f - integral {0..a} f1¦ < ε"
      using Henstock_Kurzweil_Integration.integral_diff int_f1 intgb_f by fastforce

    have "integral {0..b} (λx. g1 x - g x) ≤ integral {0..b} (λx. g1 x - g2 x)"
    proof (rule integral_le)
      show "(λx. g1 x - g x) integrable_on {0..b}" "(λx. g1 x - g2 x) integrable_on {0..b}"
        using Henstock_Kurzweil_Integration.integrable_diff int_g1 int_g2 intgb_g by blast+
    qed (auto simp: g2_le_g)
    with g2_near_g1 have "integral {0..b} (λx. g1 x - g x) < ε"
      by simp
    moreover have "integral {0..b} g ≤ integral {0..b} g1"
      by (intro integral_le has_integral_integral intgb_g has_integral_integrable [OF int_g1]) 
         (simp add: g_le_g1)
    ultimately have g_error: "¦integral {0..b} g1 - integral {0..b} g¦ < ε"
      using integral_diff int_g1 intgb_g by fastforce
    show ?thesis
      using f_error g_error ab1 by linarith
  qed
  show ?thesis
    using * [of "¦a * b - integral {0..a} f - integral {0..b} g¦ / 2"] by fastforce
qed (use assms in force)



corollary Youngs_strict:
  fixes f :: "real ⇒ real"
  assumes sm: "strict_mono_on {0..} f" and cont: "continuous_on {0..} f" and "a>0" "b≥0"
    and f: "f 0 = 0" "f a ≠ b" and fim: "f ` {0..} = {0..}"
    and g: "⋀x. 0 ≤ x ⟹ g (f x) = x"
  shows "a*b < integral {0..a} f + integral {0..b} g"
proof -
  have f_iff [simp]: "f x < f y ⟷ x < y" "f x ≤ f y ⟷ x ≤ y"
    if "x ≥ 0" "y ≥ 0" for x y
    using that by (smt (verit, best) atLeast_iff sm strict_mono_onD)+
  let ?b' = "f a"
  have "?b' ≥ 0"
    by (smt (verit, best) ‹0 < a› atLeast_iff f sm strict_mono_onD)
  then have sm_gx: "strict_mono_on {0..} g"
    unfolding strict_mono_on_def
    by (smt (verit, best) atLeast_iff f_iff(1) f_inv_into_f fim g inv_into_into)
  show ?thesis
  proof (cases "?b' < b")
    case True
    have gt_a: "a < g y" if "y ∈ {?b'<..b}" for y
    proof -
      have "a = g ?b'"
        using ‹a > 0› g by force
      also have "… < g y"
        using ‹0 ≤ ?b'› sm_gx strict_mono_onD that by fastforce
      finally show ?thesis .
    qed
    have "continuous_on {0..} g"
      by (metis cont f(1) fim g sm strict_mono_continuous_invD)
    then have contg: "continuous_on {?b'..b} g"
      by (meson Icc_subset_Ici_iff ‹0 ≤ f a› continuous_on_subset)
    have "mono_on {0..} g"
      by (simp add: sm_gx strict_mono_on_imp_mono_on)
    then have int_g0b: "g integrable_on {0..b}"
      by (simp add: integrable_on_mono_on mono_on_subset)
    then have int_gb'b: "g integrable_on {?b'..b}"
      by (simp add: ‹0 ≤ ?b'› integrable_on_subinterval)
    have "a * (b - ?b') = integral {?b'..b} (λy. a)"
      using True by force
    also have "… < integral {?b'..b} g"
      using contg True gt_a by (intro integral_less_real) auto
    finally have *: "a * (b - ?b') < integral {?b'..b} g" .
    have "a*b = a * ?b' + a * (b - ?b')"
      by (simp add: algebra_simps)
    also have "… = integral {0..a} f + integral {0..?b'} g + a * (b - ?b')"
      using Youngs_exact ‹a > 0› cont ‹f 0 = 0› g sm by force
    also have "… < integral {0..a} f + integral {0..?b'} g + integral {?b'..b} g"
      by (simp add: *)
    also have "… = integral {0..a} f + integral {0..b} g"
      by (smt (verit) Henstock_Kurzweil_Integration.integral_combine True ‹0 ≤ ?b'› int_g0b)
    finally show ?thesis .
  next
    case False
    with f have "b < ?b'" by force
    obtain a' where "f a' = b" "a' ≥ 0"
      using fim ‹b ≥ 0› by force 
    then have "a' < a"
      using ‹b < f a› ‹a > 0› by force
    have gt_b: "b < f x" if "x ∈ {a'<..a}" for x
      using ‹0 ≤ a'› ‹f a' = b› that by fastforce
    have int_f0a: "f integrable_on {0..a}"
      by (simp add: integrable_on_mono_on mono_on_def)
    then have int_fa'a: "f integrable_on {a'..a}"
      by (simp add: ‹0 ≤ a'› integrable_on_subinterval)
    have cont_f': "continuous_on {a'..a} f"
      by (meson Icc_subset_Ici_iff ‹0 ≤ a'› cont continuous_on_subset)
    have "b * (a - a') = integral {a'..a} (λx. b)"
      using ‹a' < a› by simp
    also have "… < integral {a'..a} f"
      using cont_f' ‹a' < a› gt_b by (intro integral_less_real) auto
    finally have *: "b * (a - a') < integral {a'..a} f" .
    have "a*b = a' * b + b * (a - a')"
      by (simp add: algebra_simps)
    also have "… = integral {0..a'} f + integral {0..b} g + b * (a - a')"
      by (simp add: Youngs_exact ‹0 ≤ a'› ‹f a' = b› cont f g sm)
    also have "… < integral {0..a'} f + integral {0..b} g + integral {a'..a} f"
      by (simp add: *)
    also have "… = integral {0..a} f + integral {0..b} g"
      by (smt (verit) Henstock_Kurzweil_Integration.integral_combine ‹0 ≤ a'› ‹a' < a› int_f0a)
    finally show ?thesis .
  qed
qed

corollary Youngs_inequality:
  fixes f :: "real ⇒ real"
  assumes sm: "strict_mono_on {0..} f" and cont: "continuous_on {0..} f" and "a≥0" "b≥0"
    and f: "f 0 = 0" and fim: "f ` {0..} = {0..}"
    and g: "⋀x. 0 ≤ x ⟹ g (f x) = x"
  shows "a*b ≤ integral {0..a} f + integral {0..b} g"
proof (cases "a=0")
  case True
  have "g x ≥ 0" if "x ≥ 0" for x
    by (metis atLeast_iff fim g imageE that)
  then have "0 ≤ integral {0..b} g"
    by (metis Henstock_Kurzweil_Integration.integral_nonneg atLeastAtMost_iff 
              not_integrable_integral order_refl)
  then show ?thesis 
    by (simp add: True)
next
  case False
  then show ?thesis
    by (smt (verit) assms Youngs_exact Youngs_strict)
qed

end