Quelle  Periodic.thy

section‹Shifting the origin for integration of periodic functions›

theory Periodic
  imports "HOL-Analysis.Analysis" 
begin

lemma has_bochner_integral_null [intro]:
  fixes f :: "'a::euclidean_space ==> 'b::euclidean_space"
  assumes "N ∈ null_sets lebesgue"
  shows "has_bochner_integral (lebesgue_on N) f 0"
  unfolding has_bochner_integral_iff
proof
  show "integrable (lebesgue_on N) f"
  proof (subst integrable_restrict_space)
    show "N ∩ space lebesgue ∈ sets lebesgue"
      using assms by force
    show "integrable lebesgue (λx. indicat_real N x *_R f x)"
    proof (rule integrable_cong_AE_imp)
      show "integrable lebesgue (λx. 0)"
        by simp
      show *: "AE x in lebesgue. 0 = indicat_real N x *_R f x"
        using assms
        by (simp add: indicator_def completion.null_sets_iff_AE eventually_mono)
      show "(λx. indicat_real N x *_R f x) ∈ borel_measurable lebesgue"
        by (auto intro: borel_measurable_AE [OF _ *])
    qed
  qed
  show "integral^L (lebesgue_on N) f = 0"
  proof (rule integral_eq_zero_AE)
    show "AE x in lebesgue_on N. f x = 0"
      by (rule AE_I' [where N=N]) (auto simp: assms null_setsD2 null_sets_restrict_space)
  qed
qed

lemma has_bochner_integral_null_eq[simp]:
  fixes f :: "'a::euclidean_space ==> 'b::euclidean_space"
  assumes "N ∈ null_sets lebesgue"
  shows "has_bochner_integral (lebesgue_on N) f i ⟷ i = 0"
  using assms has_bochner_integral_eq by blast

lemma periodic_integer_multiple:
   "(∀x. f(x + a) = f x) ⟷ (∀x. ∀n ∈ ℤ. f(x + n * a) = f x)" (is "?lhs = ?rhs")
proof
  assume L [rule_format]: ?lhs
  have nat: "f(x + of_nat n * a) = f x" for x n
  proof (induction n)
    case (Suc n)
    with L [of "x + of_nat n * a"] show ?case
      by (simp add: algebra_simps)
  qed auto
  have "f(x + of_int z * a) = f x" for x z
  proof (cases "z ≥ 0")
    case True
    then show ?thesis
      by (metis nat of_nat_nat)
  next
    case False
    then show ?thesis
      using nat [of "x + of_int z * a" "nat (-z)"] by auto
  qed
  then show ?rhs
    by (auto simp: Ints_def)
qed (use Ints_1 in fastforce)

lemma has_integral_offset:
  fixes f :: "real ==> 'a::euclidean_space"
  assumes "has_bochner_integral (lebesgue_on {a..b}) f i"
  shows "has_bochner_integral (lebesgue_on {a-c..b-c}) (λx. f(x + c)) i"
proof -
  have eq: "indicat_real {a..b} (x + c) = indicat_real {a-c..b-c} x" for x
    by (auto simp: indicator_def)
  have "has_bochner_integral lebesgue (λx. indicator {a..b} x *_R f x) i"
    using assms  by (auto simp: has_bochner_integral_restrict_space)
  then have "has_bochner_integral lebesgue (λx. indicat_real {a-c..b-c} x *_R f(x + c)) i"
    using has_bochner_integral_lebesgue_real_affine_iff [of 1 "(λx. indicator {a..b} x *_R f x)" i c]
    by (simp add: add_ac eq)
  then show ?thesis
    using assms by (auto simp: has_bochner_integral_restrict_space)
qed


lemma has_integral_periodic_offset_lemma:
  fixes f :: "real ==> 'a::euclidean_space"
  assumes periodic: "∧x. f(x + (b-a)) = f x" and f: "has_bochner_integral (lebesgue_on {a..a+c}) f i"
  shows "has_bochner_integral (lebesgue_on {b..b+c}) f i"
proof -
  have "f(x + a-b) = f x" for x
    using periodic [of "x + (a-b)"] by (simp add: algebra_simps)
  then show ?thesis
    using has_integral_offset [OF f, of "a-b"]
    by (auto simp: algebra_simps)
qed


lemma has_integral_periodic_offset_pos:
  fixes f :: "real ==> real"
  assumes f: "has_bochner_integral (lebesgue_on {a..b}) f i" and periodic: "∧x. f(x + (b-a)) = f x"
      and c: "c ≥ 0" "a + c ≤ b"
  shows "has_bochner_integral (lebesgue_on {a..b}) (λx. f(x + c)) i"
proof -
  have "{a..a + c} ⊆ {a..b}"
    by (simp add: assms(4))
  then have 1: "has_bochner_integral (lebesgue_on {a..a+c}) f(integral^L (lebesgue_on {a..a+c}) f)"
    by (meson integrable_subinterval f has_bochner_integral_iff)
  then have 3: "has_bochner_integral (lebesgue_on {b..b+c}) f(integral^L (lebesgue_on {a..a+c}) f)"
    using has_integral_periodic_offset_lemma periodic by blast
  have "{a + c..b} ⊆ {a..b}"
    by (simp add: c)
  then have 2: "has_bochner_integral (lebesgue_on {a+c..b}) f(integral^L (lebesgue_on {a+c..b}) f)"
    by (meson integrable_subinterval f has_bochner_integral_integrable integrable.intros)
  have "integral^L (lebesgue_on {a + c..b}) f + integral^L (lebesgue_on {a..a + c}) f = i"
    by (metis integral_combine add.commute c f has_bochner_integral_iff le_add_same_cancel1)
  then have "has_bochner_integral (lebesgue_on {a+c..b+c}) f i"
    using has_bochner_integral_combine [OF _ _ 2 3] 1 2 by (simp add: c)
  then show ?thesis
    by (metis add_diff_cancel_right' has_integral_offset)
qed


lemma has_integral_periodic_offset_weak:
  fixes f :: "real ==> real"
  assumes f: "has_bochner_integral (lebesgue_on {a..b}) f i" and periodic: "∧x. f(x + (b-a)) = f x" and c: "∣c∣ ≤ b-a"
  shows "has_bochner_integral (lebesgue_on {a..b}) (λx. f(x + c)) i"
proof (cases "c ≥ 0")
  case True
  then show ?thesis
    using c f has_integral_periodic_offset_pos periodic by auto
next
  case False
  have per': "f(- (x + (- a - - b))) = f(- x)" for x
    using periodic [of "(a-b)-x"] by simp
  have f': "has_bochner_integral (lebesgue_on {- b..- a}) (λx. f(- x)) i"
    using f by blast
  show ?thesis
    using has_integral_periodic_offset_pos [of "-b" "-a" "λx. f(-x)" i "-c", OF f' per'] c  False
    by (simp flip: has_bochner_integral_reflect_real [of b a])
qed

lemma has_integral_periodic_offset:
  fixes f :: "real ==> real"
  assumes f: "has_bochner_integral (lebesgue_on {a..b}) f i" and periodic: "∧x. f(x + (b-a)) = f x"
  shows "has_bochner_integral (lebesgue_on {a..b}) (λx. f(x + c)) i"
proof -
  consider "b ≤ a" | "a < b" by linarith
  then show ?thesis
  proof cases
    case 1
    then have "{a..b} ∈ null_sets lebesgue"
      using less_eq_real_def by auto
    with f show ?thesis
      by auto
  next
    case 2
    define fba where "fba ≡ λx. f(x + (b-a) * frac(c / (b-a)))"
    have eq: "fba x = f(x + c)"
      if "x ∈ {a..b}" for x
    proof -
      have "f(x + n * (b-a)) = f x" if "n ∈ ℤ" for n x
        using periodic periodic_integer_multiple that by blast
      then have "f((x + c) + - floor (c / (b - a)) * (b - a)) = f(x + c)"
        using Ints_of_int by blast
      moreover have "((x + c) + -floor (c / (b - a)) * (b - a)) = (x + (b - a) * frac (c / (b - a)))"
        using 2 by (simp add: field_simps frac_def)
      ultimately show ?thesis
        unfolding fba_def by metis
    qed
    have *: "has_bochner_integral (lebesgue_on {a..b}) fba i"
      unfolding fba_def
    proof (rule has_integral_periodic_offset_weak [OF f])
      show "f(x + (b - a)) = f x" for x
        by fact
      have "∣frac (c / (b - a))∣ ≤ 1"
        using frac_unique_iff less_eq_real_def by auto
      then show "∣(b - a) * frac (c / (b - a))∣ ≤ b - a"
        using "2" by auto
    qed
    then show ?thesis
    proof (rule has_bochner_integralI_AE [OF _ _ AE_I2])
      have "fba ∈ borel_measurable (lebesgue_on {a..b})"
        using "*" borel_measurable_has_bochner_integral by blast
      then show "(λx. f(x + c)) ∈ borel_measurable (lebesgue_on {a..b})"
        by (subst measurable_lebesgue_cong [OF eq, symmetric])
    qed (auto simp: eq)
  qed
qed

lemma integrable_periodic_offset:
  fixes f :: "real ==> real"
  assumes f: "integrable (lebesgue_on {a..b}) f" and periodic: "∧x. f(x + (b-a)) = f x"
  shows "integrable (lebesgue_on {a..b}) (λx. f(x + c))"
  using f has_integral_periodic_offset periodic
  by (simp add: has_bochner_integral_iff)

lemma absolutely_integrable_periodic_offset:
  fixes f :: "real ==> real"
  assumes f: "f absolutely_integrable_on {a..b}" and periodic: "∧x. f(x + (b-a)) = f x"
  shows "(λx. f(x + c)) absolutely_integrable_on {a..b}" "(λx. f(c + x)) absolutely_integrable_on {a..b}"
  using assms integrable_periodic_offset [of a b "f"]
  by (auto simp: integrable_restrict_space set_integrable_def add.commute [of c])

lemma integral_periodic_offset:
  fixes f :: "real ==> real"
  assumes periodic: "∧x. f(x + (b-a)) = f x"
  shows "integral^L (lebesgue_on {a..b}) (λx. f(x + c)) = integral^L (lebesgue_on {a..b}) f"
proof (cases "integrable (lebesgue_on {a..b}) f")
  case True
  then show ?thesis
    using has_integral_periodic_offset periodic
    by (simp add: has_bochner_integral_iff)
next
  case False
  then have "¬ integrable (lebesgue_on {a..b}) (λx. f(x + c))"
    using periodic[of "_+c"]
    by (auto simp: algebra_simps intro: dest: integrable_periodic_offset [where c = "-c"])
  then have "integral^L (lebesgue_on {a..b}) f = 0" "integral^L (lebesgue_on {a..b}) (λx. f(x + c)) = 0"
    using False not_integrable_integral_eq by blast+
  then show ?thesis
    by simp
qed

end