Theory Square_Integrable

section‹Square integrable functions over the reals›

theory Square_Integrable
  imports Lspace 
begin

subsection‹Basic definitions›

definition square_integrable:: "(real ⇒ real) ⇒ real set ⇒ bool" (infixr "square'_integrable" 46)
  where "f square_integrable S ≡ S ∈ sets lebesgue ∧ f ∈ borel_measurable (lebesgue_on S) ∧ integrable (lebesgue_on S) (λx. f x ^ 2)"

lemma square_integrable_imp_measurable:
   "f square_integrable S ⟹ f ∈ borel_measurable (lebesgue_on S)"
  by (simp add: square_integrable_def)

lemma square_integrable_imp_lebesgue:
   "f square_integrable S ⟹ S ∈ sets lebesgue"
  by (simp add: square_integrable_def)

lemma square_integrable_imp_lspace:
  assumes "f square_integrable S" shows "f ∈ lspace (lebesgue_on S) 2"
proof -
  have "(λx. (f x)⇧2) absolutely_integrable_on S"
    by (metis assms integrable_on_lebesgue_on nonnegative_absolutely_integrable_1 square_integrable_def zero_le_power2)
  moreover have "S ∈ sets lebesgue"
    using assms square_integrable_def by blast
  ultimately show ?thesis
    by (simp add: assms Lp_space_numeral integrable_restrict_space set_integrable_def square_integrable_imp_measurable)
qed

lemma square_integrable_iff_lspace:
  assumes "S ∈ sets lebesgue"
  shows "f square_integrable S ⟷ f ∈ lspace (lebesgue_on S) 2" (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  then show ?rhs
    using square_integrable_imp_lspace by blast
next
  assume ?rhs then show ?lhs
  using assms by (auto simp: Lp_space_numeral square_integrable_def integrable_on_lebesgue_on)
qed

lemma square_integrable_0 [simp]:
   "S ∈ sets lebesgue ⟹ (λx. 0) square_integrable S"
  by (simp add: square_integrable_def power2_eq_square integrable_0)

lemma square_integrable_neg_eq [simp]:
   "(λx. -(f x)) square_integrable S ⟷ f square_integrable S"
  by (auto simp: square_integrable_def)

lemma square_integrable_lmult [simp]:
  assumes "f square_integrable S"
  shows "(λx. c * f x) square_integrable S"
proof (simp add: square_integrable_def, intro conjI)
  have f: "f ∈ borel_measurable (lebesgue_on S)" "integrable (lebesgue_on S) (λx. f x ^ 2)"
    using assms by (simp_all add: square_integrable_def)
  then show "(λx. c * f x) ∈ borel_measurable (lebesgue_on S)"
    using borel_measurable_scaleR [of "λx. c" "lebesgue_on S" f]  by simp
  have "integrable (lebesgue_on S) (λx. c⇧2 * (f x)⇧2)"
  by (cases "c=0") (auto simp: f integrable_0)
  then show "integrable (lebesgue_on S) (λx. (c * f x)⇧2)"
    by (simp add: power2_eq_square mult_ac)
  show "S ∈ sets lebesgue"
    using assms square_integrable_def by blast
qed

lemma square_integrable_rmult [simp]:
   "f square_integrable S ⟹ (λx. f x * c) square_integrable S"
  using square_integrable_lmult [of f S c] by (simp add: mult.commute)

lemma square_integrable_imp_absolutely_integrable_product:
  assumes f: "f square_integrable S" and g: "g square_integrable S"
  shows "(λx. f x * g x) absolutely_integrable_on S"
proof -
  have fS: "integrable (lebesgue_on S) (λr. (f r)⇧2)" "integrable (lebesgue_on S) (λr. (g r)⇧2)"
    using assms square_integrable_def by blast+
  have "integrable (lebesgue_on S) (λx. ¦f x * g x¦)"
  proof (intro integrable_abs Holder_inequality [of 2 2])
    show "f ∈ borel_measurable (lebesgue_on S)" "g ∈ borel_measurable (lebesgue_on S)"
      using f g square_integrable_def by blast+
    show "integrable (lebesgue_on S) (λx. ¦f x¦ powr 2)" "integrable (lebesgue_on S) (λx. ¦g x¦ powr 2)"
      using nonnegative_absolutely_integrable_1 [of "(λx. (f x)⇧2)"] nonnegative_absolutely_integrable_1 [of "(λx. (g x)⇧2)"]
      by (simp_all add: fS integrable_restrict_space set_integrable_def)
  qed auto
  then show ?thesis
    using assms
    by (simp add: absolutely_integrable_measurable_real borel_measurable_times square_integrable_def)
qed

lemma square_integrable_imp_integrable_product:
  assumes "f square_integrable S" "g square_integrable S"
  shows  "integrable (lebesgue_on S) (λx. f x * g x)"
  using absolutely_integrable_measurable assms integrable_abs_iff
  by (metis (full_types) absolutely_integrable_measurable_real square_integrable_def square_integrable_imp_absolutely_integrable_product)

lemma square_integrable_add [simp]:
  assumes f: "f square_integrable S" and g: "g square_integrable S"
  shows "(λx. f x + g x) square_integrable S"
  unfolding square_integrable_def
proof (intro conjI)
  show "S ∈ sets lebesgue"
    using assms square_integrable_def by blast
  show "(λx. f x + g x) ∈ borel_measurable (lebesgue_on S)"
    by (simp add: f g borel_measurable_add square_integrable_imp_measurable)
  show "integrable (lebesgue_on S) (λx. (f x + g x)⇧2)"
    unfolding power2_eq_square distrib_right distrib_left
  proof (intro Bochner_Integration.integrable_add)
    show "integrable (lebesgue_on S) (λx. f x * f x)" "integrable (lebesgue_on S) (λx. g x * g x)"
      using f g square_integrable_imp_integrable_product by blast+
    show "integrable (lebesgue_on S) (λx. f x * g x)" "integrable (lebesgue_on S) (λx. g x * f x)"
      using f g square_integrable_imp_integrable_product by blast+
  qed
qed

lemma square_integrable_diff [simp]:
   "⟦f square_integrable S; g square_integrable S⟧ ⟹ (λx. f x - g x) square_integrable S"
  using square_integrable_neg_eq square_integrable_add [of f S "λx. - (g x)"] by auto

lemma square_integrable_abs [simp]:
   "f square_integrable S ⟹ (λx. ¦f x¦) square_integrable S"
  by (simp add: square_integrable_def borel_measurable_abs)

lemma square_integrable_sum [simp]:
  assumes I: "finite I" "⋀i. i ∈ I ⟹ f i square_integrable S" and S: "S ∈ sets lebesgue"
  shows "(λx. ∑i∈I. f i x) square_integrable S"
  using I by induction (simp_all add: S)

lemma continuous_imp_square_integrable [simp]:
   "continuous_on {a..b} f ⟹ f square_integrable {a..b}"
  using continuous_imp_integrable [of a b "(λx. (f x)⇧2)"]
  by (simp add: square_integrable_def continuous_on_power continuous_imp_measurable_on_sets_lebesgue)

lemma square_integrable_imp_absolutely_integrable:
  assumes f: "f square_integrable S" and S: "S ∈ lmeasurable"
  shows "f absolutely_integrable_on S"
proof -
  have "f ∈ lspace (lebesgue_on S) 2"
    using f S square_integrable_iff_lspace by blast
  then have "f ∈ lspace (lebesgue_on S) 1"
    by (rule lspace_mono) (use S in auto)
  then show ?thesis
    using S by (simp flip: lspace_1)
qed

lemma square_integrable_imp_integrable:
  assumes f: "f square_integrable S" and S: "S ∈ lmeasurable"
  shows "integrable (lebesgue_on S) f"
  by (meson S absolutely_integrable_measurable_real f fmeasurableD integrable_abs_iff square_integrable_imp_absolutely_integrable)

subsection‹ The norm and inner product in L2›

definition l2product :: "'a::euclidean_space set ⇒ ('a ⇒ real) ⇒ ('a ⇒ real) ⇒ real"
  where "l2product S f g ≡ (∫x. f x * g x ∂(lebesgue_on S))"

definition l2norm :: "['a::euclidean_space set, 'a ⇒ real] ⇒ real"
  where "l2norm S f ≡ sqrt (l2product S f f)"

definition lnorm :: "['a measure, real, 'a ⇒ real] ⇒ real"
  where "lnorm M p f ≡ (∫x. ¦f x¦ powr p ∂M) powr (1/p)"

corollary Holder_inequality_lnorm:
  assumes "p > (0::real)" "q > 0" "1/p+1/q = 1"
      and "f ∈ borel_measurable M" "g ∈ borel_measurable M"
          "integrable M (λx. ¦f x¦ powr p)"
          "integrable M (λx. ¦g x¦ powr q)"
  shows "(∫x. ¦f x * g x¦ ∂M) ≤ lnorm M p f * lnorm M q g"
        "¦∫x. f x * g x ∂M ¦ ≤ lnorm M p f * lnorm M q g"
  by (simp_all add: Holder_inequality assms lnorm_def)

lemma l2norm_lnorm: "l2norm S f = lnorm (lebesgue_on S) 2 f"
proof -
  have "(LINT x|lebesgue_on S. (f x)⇧2) ≥ 0"
    by simp
  then show ?thesis
    by (auto simp: lnorm_def l2norm_def l2product_def power2_eq_square powr_half_sqrt)
qed

lemma lnorm_nonneg: "lnorm M p f ≥ 0"
  by (simp add: lnorm_def)

lemma lnorm_minus_commute: "lnorm M p (g - f) = lnorm M p (f - g)"
  by (simp add: lnorm_def abs_minus_commute)


text‹ Extending a continuous function in a periodic way›

proposition continuous_on_compose_frac:
  fixes f:: "real ⇒ real"
  assumes contf: "continuous_on {0..1} f" and f10: "f 1 = f 0"
  shows "continuous_on UNIV (f ∘ frac)"
proof -
  have *: "isCont (f ∘ frac) x"
    if caf: "⋀x. ⟦0 ≤ x; x ≤ 1⟧ ⟹ continuous (at x within {0..1}) f" for x
  proof (cases "x ∈ ℤ")
    case True
    then have [simp]: "frac x = 0"
      by simp
    show ?thesis
    proof (clarsimp simp add: continuous_at_eps_delta dist_real_def)
      have f0: "continuous (at 0 within {0..1}) f" and f1: "continuous (at 1 within {0..1}) f"
        by (auto intro: caf)
      show "∃d>0. ∀x'. ¦x'-x¦ < d ⟶ ¦f(frac x') - f 0¦ < e"
        if "0 < e" for e
      proof -
        obtain d0 where "d0 > 0" and d0: "⋀x'. ⟦x'∈{0..1}; ¦x'¦ < d0⟧ ⟹ ¦f x' - f 0¦ < e"
          using ‹e > 0› caf [of 0] dist_not_less_zero
          by (auto simp: continuous_within_eps_delta dist_real_def)
        obtain d1 where "d1 > 0" and d1: "⋀x'. ⟦x'∈{0..1}; ¦x' - 1¦ < d1⟧ ⟹ ¦f x' - f 0¦ < e"
          using ‹e > 0› caf [of 1] dist_not_less_zero f10
          by (auto simp: continuous_within_eps_delta dist_real_def)
        show ?thesis
        proof (intro exI conjI allI impI)
          show "0 < min 1 (min d0 d1)"
            by (auto simp: ‹d0 > 0› ‹d1 > 0›)
          show "¦f(frac x') - f 0¦ < e"
            if "¦x'-x¦ < min 1 (min d0 d1)" for x'
          proof (cases "x ≤ x'")
            case True
            with ‹x ∈ ℤ› that have "frac x' = x' - x"
              by (simp add: frac_unique_iff)
            then show ?thesis
              using True d0 that by auto
          next
            case False
            then have [simp]: "frac x' = 1 - (x - x')"
              using that ‹x ∈ ℤ› by (simp add: not_le frac_unique_iff)
            show ?thesis
              using False d1 that by auto
          qed
        qed
      qed
    qed
  next
    case False
    show ?thesis
    proof (rule continuous_at_compose)
      show "isCont frac x"
        by (simp add: False continuous_frac)
      have "frac x ∈ {0<..<1}"
        by (simp add: False frac_lt_1)
      then show "isCont f(frac x)"
        by (metis at_within_Icc_at greaterThanLessThan_iff le_cases not_le that)
    qed
  qed
  then show ?thesis
    using contf by (simp add: o_def continuous_on_eq_continuous_within)
qed


proposition Tietze_periodic_interval:
  fixes f:: "real ⇒ real"
  assumes contf: "continuous_on {a..b} f" and fab: "f a = f b"
  obtains g where "continuous_on UNIV g" "⋀x. x ∈ {a..b} ⟹ g x = f x"
                  "⋀x. g(x + (b-a)) = g x"
proof (cases "a < b")
  case True
  let ?g = "f ∘ (λy. a + (b-a) * y) ∘ frac ∘
                (λx. (x - a) / (b-a))"
  show ?thesis
  proof
    have "a + (b - a) * y ≤ b" if "a < b" "0 ≤ y" "y ≤ 1" for y
      using that affine_ineq by (force simp: field_simps)
    then have *: "continuous_on (range (λx. (x - a) / (b - a))) (f ∘ (λy. a + (b - a) * y) ∘ frac)"
      apply (intro continuous_on_subset [OF continuous_on_compose_frac] continuous_on_subset [OF contf]
          continuous_intros)
      using ‹a < b›
      by (auto simp: fab)
    show "continuous_on UNIV ?g"
      by (intro * continuous_on_compose continuous_intros) (use True in auto)
    show "?g x = f x" if "x ∈ {a..b}" for x :: real
    proof (cases "x=b")
      case True
      then show ?thesis
        by (auto simp: frac_def intro: fab)
    next
      case False
      with ‹a < b› that have "frac ((x - a) / (b - a)) = (x - a) / (b - a)"
        by (subst frac_eq) (auto simp: divide_simps)
      with ‹a < b› show ?thesis
        by auto
    qed
    have "a + (b-a) * frac ((x + b - 2 * a) / (b-a)) = a + (b-a) * frac ((x - a) / (b-a))" for x
      using True frac_1_eq [of "(x - a) / (b-a)"] by (auto simp: divide_simps)
    then show "?g (x + (b-a)) = (?g x::real)" for x
      by force
  qed
next
  case False
  show ?thesis
  proof
    show "f a = f x" if "x ∈ {a..b}" for x
      using that False order_trans by fastforce
  qed auto
qed


subsection‹Lspace stuff›

lemma eNorm_triangle_eps:
  assumes "eNorm N (x' - x) < a" "defect N = 1"
  obtains e where "e > 0" "⋀y. eNorm N (y - x') < e ⟹ eNorm N (y - x) < a"
proof -
  let ?d = "a - Norm N (x' - x)"
  have nt: "eNorm N (x' - x) < ⊤"
    using assms top.not_eq_extremum by fastforce
  with assms have d: "?d > 0"
    by (simp add: Norm_def diff_gr0_ennreal)
  have [simp]: "ennreal (1 - Norm N (x' - x)) = 1 - eNorm N (x' - x)"
    using that nt  unfolding Norm_def  by (metis enn2real_nonneg ennreal_1 ennreal_enn2real ennreal_minus)
  show ?thesis
  proof
    show "(0::ennreal) < ?d"
      using d ennreal_less_zero_iff by blast
    show "eNorm N (y - x) < a"
      if "eNorm N (y - x') < ?d" for y
      using that assms eNorm_triangular_ineq [of N "y - x'" "x' - x"] le_less_trans less_diff_eq_ennreal
      by (simp add: Norm_def nt)
  qed
qed

lemma topspace_topology⇩N [simp]:
  assumes "defect N = 1" shows "topspace (topology⇩N N) = UNIV"
proof -
  have "x ∈ topspace (topology⇩N N)" for x
  proof -
    have "∃e>0. ∀y. eNorm N (y - x') < e ⟶ eNorm N (y - x) < 1"
      if "eNorm N (x' - x) < 1" for x'
      using eNorm_triangle_eps
      by (metis assms that)
    then show ?thesis
      unfolding topspace_def
      by (rule_tac X="{y. eNorm N (y - x) < 1}" in UnionI) (auto intro: openin_topology⇩N_I)
  qed
  then show ?thesis
    by auto
qed

lemma tendsto_ine⇩N_iff_limitin:
  assumes "defect N = 1"
  shows "tendsto_ine⇩N N u x = limitin (topology⇩N N) u x sequentially"
proof -
  have "∀⇩F x in sequentially. u x ∈ U"
    if 0: "(λn. eNorm N (u n - x)) ⇢ 0" and U: "openin (topology⇩N N) U" "x ∈ U" for U
  proof -
    obtain e where "e > 0" and e: "⋀y. eNorm N (y-x) < e ⟹ y ∈ U"
      using openin_topology⇩N_D U by metis
    then show ?thesis
      using eventually_mono order_tendstoD(2)[OF 0] by force
  qed
  moreover have "(λn. eNorm N (u n - x)) ⇢ 0"
    if x: "x ∈ topspace (topology⇩N N)"
      and *: "⋀U. ⟦openin (topology⇩N N) U; x ∈ U⟧ ⟹ (∀⇩F x in sequentially. u x ∈ U)"
  proof (rule order_tendstoI)
    show "∀⇩F n in sequentially. eNorm N (u n - x) < a" if "a > 0" for a
      apply (rule * [OF openin_topology⇩N_I, of "{v. eNorm N (v - x) < a}", simplified])
      using assms eNorm_triangle_eps that apply blast+
      done
  qed simp
  ultimately show ?thesis
    by (auto simp: tendsto_ine⇩N_def limitin_def assms)
qed

corollary tendsto_ine⇩N_iff_limitin_ge1:
  fixes p :: ennreal
  assumes "p ≥ 1"
  shows "tendsto_ine⇩N (𝔏 p M) u x = limitin (topology⇩N (𝔏 p M)) u x sequentially"
proof (rule tendsto_ine⇩N_iff_limitin)
  show "defect (𝔏 p M) = 1"
    by (metis (full_types) L_infinity(2) L_zero(2) Lp(2) Lp_cases assms ennreal_ge_1)
qed

corollary tendsto_in⇩N_iff_limitin:
  assumes "defect N = 1" "x ∈ space⇩N N" "⋀n. u n ∈ space⇩N N"
  shows "tendsto_in⇩N N u x = limitin (topology⇩N N) u x sequentially"
  using assms tendsto_ine⇩N_iff_limitin tendsto_ine_in by blast

corollary tendsto_in⇩N_iff_limitin_ge1:
  fixes p :: ennreal
  assumes "p ≥ 1" "x ∈ lspace M p" "⋀n. u n ∈ lspace M p"
  shows "tendsto_in⇩N (𝔏 p M) u x = limitin (topology⇩N (𝔏 p M)) u x sequentially"
proof (rule tendsto_in⇩N_iff_limitin)
  show "defect (𝔏 p M) = 1"
    by (metis (full_types) L_infinity(2) L_zero(2) Lp(2) Lp_cases ‹p ≥ 1› ennreal_ge_1)
qed (auto simp: assms)


lemma l2product_sym: "l2product S f g = l2product S g f"
  by (simp add: l2product_def mult.commute)

lemma l2product_pos_le:
   "f square_integrable S ⟹ 0 ≤ l2product S f f"
  by (simp add: square_integrable_def l2product_def flip: power2_eq_square)

lemma l2norm_pow_2:
   "f square_integrable S ⟹ (l2norm S f) ^ 2 = l2product S f f"
  by (simp add: l2norm_def l2product_pos_le)

lemma l2norm_pos_le:
   "f square_integrable S ⟹ 0 ≤ l2norm S f"
  by (simp add: l2norm_def l2product_pos_le)

lemma l2norm_le: "(l2norm S f ≤ l2norm S g ⟷ l2product S f f ≤ l2product S g g)"
  by (simp add: l2norm_def)

lemma l2norm_eq:
   "(l2norm S f = l2norm S g ⟷ l2product S f f = l2product S g g)"
  by (simp add: l2norm_def)

lemma Schwartz_inequality_strong:
  assumes "f square_integrable S" "g square_integrable S"
  shows "l2product S (λx. ¦f x¦) (λx. ¦g x¦) ≤ l2norm S f * l2norm S g"
  using Holder_inequality_lnorm [of 2 2 f "lebesgue_on S" g] assms
  by (simp add: square_integrable_def l2product_def abs_mult flip: l2norm_lnorm)

lemma Schwartz_inequality_abs:
  assumes "f square_integrable S" "g square_integrable S"
  shows "¦l2product S f g¦ ≤ l2norm S f * l2norm S g"
proof -
  have "¦l2product S f g¦ ≤ l2product S (λx. ¦f x¦) (λx. ¦g x¦)"
    unfolding l2product_def
  proof (rule integral_abs_bound_integral)
    show "integrable (lebesgue_on S) (λx. f x * g x)" "integrable (lebesgue_on S) (λx. ¦f x¦ * ¦g x¦)"
      by (simp_all add: assms square_integrable_imp_integrable_product)
  qed (simp add: abs_mult)
  also have "… ≤ l2norm S f * l2norm S g"
    by (simp add: Schwartz_inequality_strong assms)
  finally show ?thesis .
qed

lemma Schwartz_inequality:
  assumes "f square_integrable S" "g square_integrable S"
  shows "l2product S f g ≤ l2norm S f * l2norm S g"
  using Schwartz_inequality_abs assms by fastforce


lemma lnorm_triangle:
  assumes f: "f ∈ lspace M p" and g: "g ∈ lspace M p" and "p ≥ 1"
  shows "lnorm M p (λx. f x + g x) ≤ lnorm M p f + lnorm M p g"
proof -
  have "p > 0"
    using assms by linarith
  then have "integrable M (λx. ¦f x¦ powr p)" "integrable M (λx. ¦g x¦ powr p)"
    by (simp_all add: Lp_D(2) assms)
  moreover have "f ∈ borel_measurable M" "g ∈ borel_measurable M"
    using Lp_measurable f g by blast+
  ultimately show ?thesis
    unfolding lnorm_def using Minkowski_inequality(2) ‹p ≥ 1› by blast
qed

lemma lnorm_triangle_fun:
  assumes f: "f ∈ lspace M p" and g: "g ∈ lspace M p" and "p ≥ 1"
  shows "lnorm M p (f + g) ≤ lnorm M p f + lnorm M p g"
  using lnorm_triangle [OF assms] by (simp add: plus_fun_def)

lemma l2norm_triangle:
  assumes "f square_integrable S" "g square_integrable S"
  shows "l2norm S (λx. f x + g x) ≤ l2norm S f + l2norm S g"
proof -
  have "f ∈ lspace (lebesgue_on S) 2" "g ∈ lspace (lebesgue_on S) 2"
    using assms by (simp_all add: square_integrable_imp_lspace)
  then show ?thesis
    using lnorm_triangle [of f 2 "lebesgue_on S"]
    by (simp add: l2norm_lnorm)
qed


lemma l2product_ladd:
   "⟦f square_integrable S; g square_integrable S; h square_integrable S⟧
    ⟹ l2product S (λx. f x + g x) h = l2product S f h + l2product S g h"
  by (simp add: l2product_def algebra_simps square_integrable_imp_integrable_product)

lemma l2product_radd:
   "⟦f square_integrable S; g square_integrable S; h square_integrable S⟧
    ⟹ l2product S f(λx. g x + h x) = l2product S f g + l2product S f h"
  by (simp add: l2product_def algebra_simps square_integrable_imp_integrable_product)

lemma l2product_ldiff:
   "⟦f square_integrable S; g square_integrable S; h square_integrable S⟧
    ⟹ l2product S (λx. f x - g x) h = l2product S f h - l2product S g h"
  by (simp add: l2product_def algebra_simps square_integrable_imp_integrable_product)

lemma l2product_rdiff:
   "⟦f square_integrable S; g square_integrable S; h square_integrable S⟧
    ⟹ l2product S f(λx. g x - h x) = l2product S f g - l2product S f h"
  by (simp add: l2product_def algebra_simps square_integrable_imp_integrable_product)

lemma l2product_lmult:
   "⟦f square_integrable S; g square_integrable S⟧
    ⟹ l2product S (λx. c * f x) g = c * l2product S f g"
  by (simp add: l2product_def algebra_simps)

lemma l2product_rmult:
   "⟦f square_integrable S; g square_integrable S⟧
    ⟹ l2product S f(λx. c * g x) = c * l2product S f g"
  by (simp add: l2product_def algebra_simps)

lemma l2product_lzero [simp]: "l2product S (λx. 0) f = 0"
  by (simp add: l2product_def)

lemma l2product_rzero [simp]: "l2product S f(λx. 0) = 0"
  by (simp add: l2product_def)

lemma l2product_lsum:
  assumes I: "finite I" "⋀i. i ∈ I ⟹ (f i) square_integrable S" and S: "g square_integrable S"
  shows "l2product S (λx. ∑i∈I. f i x) g = (∑i∈I. l2product S (f i) g)"
  using I
proof induction
  case (insert i I)
  with S show ?case
    by (simp add: l2product_ladd square_integrable_imp_lebesgue)
qed auto

lemma l2product_rsum:
  assumes I: "finite I" "⋀i. i ∈ I ⟹ (f i) square_integrable S" and S: "g square_integrable S"
  shows "l2product S g (λx. ∑i∈I. f i x) = (∑i∈I. l2product S g (f i))"
  using l2product_lsum [OF assms] by (simp add: l2product_sym)

lemma l2norm_lmult:
   "f square_integrable S ⟹ l2norm S (λx. c * f x) = ¦c¦ * l2norm S f"
  by (simp add: l2norm_def l2product_rmult l2product_sym real_sqrt_mult)

lemma l2norm_rmult:
   "f square_integrable S ⟹ l2norm S (λx. f x * c) = l2norm S f * ¦c¦"
  using l2norm_lmult by (simp add: mult.commute)

lemma l2norm_neg:
   "f square_integrable S ⟹ l2norm S (λx. - f x) = l2norm S f"
  using l2norm_lmult [of f S "-1"] by simp

lemma l2norm_diff:
  assumes "f square_integrable S" "g square_integrable S"
  shows "l2norm S (λx. f x - g x) = l2norm S (λx. g x - f x)"
proof -
  have "(λx. f x - g x) square_integrable S"
    using assms square_integrable_diff by blast
  then show ?thesis
    using l2norm_neg [of "λx. f x - g x" S] by (simp add: algebra_simps)
qed


subsection‹Completeness (Riesz-Fischer)›

lemma eNorm_eq_lnorm: "⟦f ∈ lspace M p; p > 0⟧ ⟹ eNorm (𝔏 (ennreal p) M) f = ennreal (lnorm M p f)"
  by (simp add: Lp_D(4) lnorm_def)

lemma Norm_eq_lnorm: "⟦f ∈ lspace M p; p > 0⟧ ⟹ Norm (𝔏 (ennreal p) M) f = lnorm M p f"
  by (simp add: Lp_D(3) lnorm_def)


lemma eNorm_ge1_triangular_ineq:
  assumes "p ≥ (1::real)"
  shows "eNorm (𝔏 p M) (x + y) ≤ eNorm (𝔏 p M) x + eNorm (𝔏 p M) y"
  using eNorm_triangular_ineq [of "(𝔏 p M)"] assms
  by (simp add: Lp(2))

text‹A mere repackaging of the theorem @{thm Lp_complete}, but nearly as much work again.›
proposition l2_complete:
  assumes f: "⋀i::nat. f i square_integrable S"
    and cauchy: "⋀e. 0 < e ⟹ ∃N. ∀m≥N. ∀n≥N. l2norm S (λx. f m x - f n x) < e"
  obtains g where "g square_integrable S" "((λn. l2norm S (λx. f n x - g x)) ⇢ 0)"
proof -
  have finite: "eNorm (𝔏 2 (lebesgue_on S)) (f n - f m) < ⊤" for m n
    by (metis f infinity_ennreal_def spaceN_diff spaceN_iff square_integrable_imp_lspace)
  have *: "cauchy_ine⇩N (𝔏 2 (lebesgue_on S)) f"
  proof (clarsimp simp: cauchy_ine⇩N_def)
    show "∃M. ∀n≥M. ∀m≥M. eNorm (𝔏 2 (lebesgue_on S)) (f n - f m) < e"
      if "e > 0" for e
    proof (cases e)
      case (real r)
      then have "r > 0"
        using that by auto
      with cauchy obtain N::nat where N: "⋀m n. ⟦m ≥ N; n ≥ N⟧ ⟹ l2norm S (λx. f n x - f m x) < r"
        by blast
      show ?thesis
      proof (intro exI allI impI)
        show "eNorm (𝔏 2 (lebesgue_on S)) (f n - f m) < e"
          if "N ≤ m" "N ≤ n" for m n
        proof -
          have fnm: "(f n - f m) ∈ borel_measurable (lebesgue_on S)"
            using f unfolding square_integrable_def by (blast intro: borel_measurable_diff')
          have "l2norm S (λx. f n x - f m x) = lnorm (lebesgue_on S) 2 (λx. f n x - f m x)"
            by (metis l2norm_lnorm)
          also have "… = Norm (𝔏 2 (lebesgue_on S)) (f n - f m)"
            using Lp_Norm [OF _ fnm, of 2] by (simp add: lnorm_def)
          finally show ?thesis
            using N [OF that] real finite
            by (simp add: Norm_def)
        qed
      qed
    qed (simp add: finite)
  qed
  then obtain g where g: "tendsto_ine⇩N (𝔏 2 (lebesgue_on S)) f g"
    using Lp_complete complete⇩N_def by blast
  show ?thesis
  proof
    have fng_to_0: "(λn. eNorm (𝔏 2 (lebesgue_on S)) (λx. f n x - g x)) ⇢ 0"
      using g Lp_D(4) [of 2 _ "lebesgue_on S"]
      by (simp add: tendsto_ine⇩N_def minus_fun_def)
    then obtain M where "⋀n . n ≥ M ⟹ eNorm (𝔏 2 (lebesgue_on S)) (λx. f n x - g x) < ⊤"
      apply (simp add: lim_explicit)
      by (metis (full_types) open_lessThan diff_self eNorm_zero lessThan_iff local.finite)
    then have "eNorm (𝔏 2 (lebesgue_on S)) (λx. g x - f M x) < ⊤"
      using eNorm_uminus [of _ "λx. g x - f _ x"] by (simp add: uminus_fun_def)
    moreover have "eNorm (𝔏 2 (lebesgue_on S)) (λx. f M x) < ⊤"
      using f square_integrable_imp_lspace by (simp add: spaceN_iff)
    ultimately have "eNorm (𝔏 2 (lebesgue_on S)) g < ⊤"
      using eNorm_ge1_triangular_ineq [of 2 "lebesgue_on S" "g - f M" "f M", simplified] not_le top.not_eq_extremum
      by (fastforce simp add: minus_fun_def)
    then have g_space: "g ∈ space⇩N (𝔏 2 (lebesgue_on S))"
      by (simp add: spaceN_iff)
    show "g square_integrable S"
      unfolding square_integrable_def
    proof (intro conjI)
      show "g ∈ borel_measurable (lebesgue_on S)"
        using Lp_measurable g_space by blast
      show "S ∈ sets lebesgue"
        using f square_integrable_def by blast
      then show "integrable (lebesgue_on S) (λx. (g x)⇧2)"
        using g_space square_integrable_def square_integrable_iff_lspace by blast
    qed
    then have "f n - g ∈ lspace (lebesgue_on S) 2" for n
      using f spaceN_diff square_integrable_imp_lspace by blast
    with fng_to_0 have "(λn. ennreal (lnorm (lebesgue_on S) 2 (λx. f n x - g x))) ⇢ 0"
      by (simp add: minus_fun_def flip: eNorm_eq_lnorm)
    then have "(λn. lnorm (lebesgue_on S) 2 (λx. f n x - g x)) ⇢ 0"
      by (simp add: ennreal_tendsto_0_iff lnorm_def)
    then show "(λn. l2norm S (λx. f n x - g x)) ⇢ 0"
      using g by (simp add:  l2norm_lnorm lnorm_def)
  qed
qed

subsection‹Approximation of functions in Lp by bounded and continuous ones›

lemma lspace_bounded_measurable:
  fixes p::real
  assumes f: "f ∈ borel_measurable (lebesgue_on S)" and g: "g ∈ lspace (lebesgue_on S) p" and "p > 0"
    and le: " AE x in lebesgue_on S. norm (¦f x¦ powr p) ≤ norm (¦g x¦ powr p)"
  shows "f ∈ lspace (lebesgue_on S) p"
  using assms by (auto simp: lspace_ennreal_iff intro: Bochner_Integration.integrable_bound)

lemma lspace_approximate_bounded:
  assumes f: "f ∈ lspace (lebesgue_on S) p" and S: "S ∈ lmeasurable" and "p > 0" "e > 0"
  obtains g where "g ∈ lspace (lebesgue_on S) p" "bounded (g ` S)"
    "lnorm (lebesgue_on S) p (f - g) < e"
proof -
  have f_bm: "f ∈ borel_measurable (lebesgue_on S)"
    using Lp_measurable f by blast
  let ?f = "λn::nat. λx. max (- n) (min n (f x))"
  have "tendsto_in⇩N (𝔏 p (lebesgue_on S)) ?f f"
  proof (rule Lp_domination_limit)
    show "⋀n::nat. ?f n ∈ borel_measurable (lebesgue_on S)"
      by (intro f_bm borel_measurable_max borel_measurable_min borel_measurable_const)
    show "abs ∘ f ∈ lspace (lebesgue_on S) p"
      using Lp_Banach_lattice [OF f] by (simp add: o_def)
    have *: "∀⇩F n in sequentially. dist (?f n x) (f x) < e"
      if x: "x ∈ space (lebesgue_on S)" and "e > 0" for x e
    proof
      show "dist (?f n x) (f x) < e"
        if "nat ⌈¦f x¦⌉ ≤ n" for n :: nat
        using that ‹0 < e› by (simp add: dist_real_def max_def min_def abs_if split: if_split_asm)
    qed
    then show "AE x in lebesgue_on S. (λn::nat. max (- n) (min n (f x))) ⇢ f x"
      by (blast intro: tendstoI)
  qed (auto simp: f_bm)
  moreover
  have lspace: "?f n ∈ lspace (lebesgue_on S) p" for n::nat
    by (intro f lspace_const lspace_min lspace_max ‹p > 0› S)
  ultimately have "(λn. lnorm (lebesgue_on S) p (?f n - f)) ⇢ 0"
    by (simp add: tendsto_in⇩N_def Norm_eq_lnorm ‹p > 0› f)
  with ‹e > 0› obtain N where N: "¦lnorm (lebesgue_on S) p (?f N - f)¦ < e"
    by (auto simp: LIMSEQ_iff)
  show ?thesis
  proof
    have "∀x∈S. ¦max (- real N) (min (real N) (f x))¦ ≤ N"
      by auto
    then show "bounded (?f N ` S::real set)"
      by (force simp: bounded_iff)
    show "lnorm (lebesgue_on S) p (f - ?f N) < e"
      using N by (simp add: lnorm_minus_commute)
  qed (auto simp: lspace)
qed

lemma borel_measurable_imp_continuous_limit:
  fixes h :: "'a::euclidean_space ⇒ 'b::euclidean_space"
  assumes h: "h ∈ borel_measurable (lebesgue_on S)" and S: "S ∈ sets lebesgue"
  obtains g where "⋀n. continuous_on UNIV (g n)" "AE x in lebesgue_on S. (λn::nat. g n x) ⇢ h x"
proof -
  have "h measurable_on S"
    using S h measurable_on_iff_borel_measurable by blast
  then obtain N g where N: "N ∈ null_sets lebesgue" and g: "⋀n. continuous_on UNIV (g n)"
    and tends: "⋀x. x ∉ N ⟹ (λn. g n x) ⇢ (if x ∈ S then h x else 0)"
    by (auto simp: measurable_on_def negligible_iff_null_sets)
  moreover have "AE x in lebesgue_on S. (λn::nat. g n x) ⇢ h x"
  proof (rule AE_I')
    show "N ∩ S ∈ null_sets (lebesgue_on S)"
      by (simp add: S N null_set_Int2 null_sets_restrict_space)
    show "{x ∈ space (lebesgue_on S). ¬ (λn. g n x) ⇢ h x} ⊆ N ∩ S"
      using tends by force
  qed
  ultimately show thesis
    using that by blast
qed


proposition lspace_approximate_continuous:
  assumes f: "f ∈ lspace (lebesgue_on S) p" and S: "S ∈ lmeasurable" and "1 ≤ p" "e > 0"
  obtains g where "continuous_on UNIV g" "g ∈ lspace (lebesgue_on S) p" "lnorm (lebesgue_on S) p (f - g) < e"
proof -
  have "p > 0"
    using assms by simp
  obtain h where h: "h ∈ lspace (lebesgue_on S) p" and "bounded (h ` S)"
    and lesse2: "lnorm (lebesgue_on S) p (f - h) < e/2"
    by (rule lspace_approximate_bounded [of f p S "e/2"]) (use assms in auto)
  then obtain B where "B > 0" and B: "⋀x. x ∈ S ⟹ ¦h x¦ ≤ B"
    by (auto simp: bounded_pos)
  have bmh: "h ∈ borel_measurable (lebesgue_on S)"
    using h lspace_ennreal_iff [of p] ‹p ≥ 1› by auto
  obtain g where contg: "⋀n. continuous_on UNIV (g n)"
    and gle: "⋀n x. x ∈ S ⟹ ¦g n x¦ ≤ B"
    and tends: "AE x in lebesgue_on S. (λn::nat. g n x) ⇢ h x"
  proof -
    obtain γ where cont: "⋀n. continuous_on UNIV (γ n)"
      and tends: "AE x in lebesgue_on S. (λn::nat. γ n x) ⇢ h x"
      using borel_measurable_imp_continuous_limit S bmh by blast
    let ?g = "λn::nat. λx. max (- B) (min B (γ n x))"
    show thesis
    proof
      show "continuous_on UNIV (?g n)" for n
        by (intro continuous_intros cont)
      show "¦?g n x¦ ≤ B" if "x ∈ S"  for n x
        using that ‹B > 0› by (auto simp: max_def min_def)
      have "(λn. max (- B) (min B (γ n x))) ⇢ h x"
        if "(λn. γ n x) ⇢ h x" "x ∈ S" for x
        using that ‹B > 0› B [OF ‹x ∈ S›]
        unfolding LIMSEQ_def by (fastforce simp: min_def max_def dist_real_def)
      then show "AE x in lebesgue_on S. (λn. ?g n x) ⇢ h x"
        using tends by auto
    qed
  qed
  have lspace_B: "(λx. B) ∈ lspace (lebesgue_on S) p"
    by (simp add: S ‹0 < p› lspace_const)
  have lspace_g: "g n ∈ lspace (lebesgue_on S) p" for n
  proof (rule lspace_bounded_measurable)
    show "g n ∈ borel_measurable (lebesgue_on S)"
      by (simp add: borel_measurable_continuous_onI contg measurable_completion measurable_restrict_space1)
    show "AE x in lebesgue_on S. norm (¦g n x¦ powr p) ≤ norm (¦B¦ powr p)"
      using ‹B > 0› gle S ‹0 < p› powr_mono2 by auto
  qed (use ‹p > 0› lspace_B in auto)
  have "tendsto_in⇩N (𝔏 p (lebesgue_on S)) g h"
  proof (rule Lp_domination_limit [OF bmh _ lspace_B tends])
    show "⋀n::nat. g n ∈ borel_measurable (lebesgue_on S)"
      using Lp_measurable lspace_g by blast
    show "⋀n. AE x in lebesgue_on S. ¦g n x¦ ≤ B"
      using S gle by auto
  qed
  then have 0: "(λn. Norm (𝔏 p (lebesgue_on S)) (g n - h)) ⇢ 0"
    by (simp add: tendsto_in⇩N_def)
  have "⋀e. 0 < e ⟹ ∃N. ∀n≥N. lnorm (lebesgue_on S) p (g n - h) < e"
    using LIMSEQ_D [OF 0] ‹e > 0›
    by (force simp: Norm_eq_lnorm ‹0 < p› h lspace_g)
  then obtain N where N: "lnorm (lebesgue_on S) p (g N - h) < e/2"
    unfolding minus_fun_def by (meson ‹e>0› half_gt_zero order_refl)
  show ?thesis
  proof
    show "continuous_on UNIV (g N)"
      by (simp add: contg)
    show "g N ∈ lspace (lebesgue_on S) (ennreal p)"
      by (simp add: lspace_g)
    have "lnorm (lebesgue_on S) p (f - h + - (g N - h)) ≤ lnorm (lebesgue_on S) p (f - h) + lnorm (lebesgue_on S) p (- (g N - h))"
      by (rule lnorm_triangle_fun) (auto simp: lspace_g h assms)
    also have "…  < e/2 + e/2"
      using lesse2 N by (simp add: lnorm_minus_commute)
    finally show "lnorm (lebesgue_on S) p (f - g N) < e"
      by simp
  qed
qed

proposition square_integrable_approximate_continuous:
  assumes f: "f square_integrable S" and S: "S ∈ lmeasurable" and "e > 0"
  obtains g where "continuous_on UNIV g" "g square_integrable S" "l2norm S (λx. f x - g x) < e"
proof -
  have f2: "f ∈ lspace (lebesgue_on S) 2"
    by (simp add: f square_integrable_imp_lspace)
  then obtain g where contg: "continuous_on UNIV g"
             and g2: "g ∈ lspace (lebesgue_on S) 2"
             and less_e: "lnorm (lebesgue_on S) 2 (λx. f x - g x) < e"
    using lspace_approximate_continuous [of f 2 S e] S ‹0 < e› by (auto simp: minus_fun_def)
  show thesis
  proof
    show "g square_integrable S"
      using g2 by (simp add: S fmeasurableD square_integrable_iff_lspace)
    show "l2norm S (λx. f x - g x) < e"
      using less_e by (simp add: l2norm_lnorm)
  qed (simp add: contg)
qed

lemma absolutely_integrable_approximate_continuous:
  fixes f :: "real ⇒ real"
  assumes f: "f absolutely_integrable_on S" and S: "S ∈ lmeasurable" and "0 < e"
  obtains g where "continuous_on UNIV g" "g absolutely_integrable_on S" "integral⇧L (lebesgue_on S) (λx. ¦f x - g x¦) < e"
proof -
  obtain g where "continuous_on UNIV g" "g ∈ lspace (lebesgue_on S) 1"
              and lnorm: "lnorm (lebesgue_on S) 1 (f - g) < e"
  proof (rule lspace_approximate_continuous)
    show "f ∈ lspace (lebesgue_on S) (ennreal 1)"
      by (simp add: S f fmeasurableD lspace_1)
  qed (auto simp: assms)
  show thesis
  proof
    show "continuous_on UNIV g"
      by fact
    show "g absolutely_integrable_on S"
      using S ‹g ∈ lspace (lebesgue_on S) 1› lspace_1 by blast
    have *: "(λx. f x - g x) absolutely_integrable_on S"
      by (simp add: ‹g absolutely_integrable_on S› f)
    moreover have "integrable (lebesgue_on S) (λx. ¦f x - g x¦)"
      by (simp add: L1_D(2) S * fmeasurableD lspace_1)
    ultimately show "integral⇧L (lebesgue_on S)  (λx. ¦f x - g x¦) < e"
      using lnorm S unfolding lnorm_def absolutely_integrable_on_def
      by simp
  qed
qed

end