Theory Bump_Function

section ‹Bump Functions›
theory Bump_Function
  imports Smooth
    "HOL-Analysis.Weierstrass_Theorems"
begin

subsection ‹Construction›

context begin

qualified definition f :: "real  real" where
  "f t = (if t > 0 then exp(-inverse t) else 0)"

lemma f_nonpos[simp]: "x  0  f x = 0"
  by (auto simp: f_def)

lemma exp_inv_limit_0_right:
  "((λ(t::real). exp(-inverse t))  0) (at_right 0)"
  apply (rule filterlim_compose[where g = exp])
   apply (rule exp_at_bot)
  apply (rule filterlim_compose[where g = uminus])
   apply (rule filterlim_uminus_at_bot_at_top)
  by (rule filterlim_inverse_at_top_right)

lemma "F t in at_right 0. ((λx. inverse (x ^ Suc k)) has_real_derivative
  - (inverse (t ^ Suc k) * ((1 + real k) * t ^ k) * inverse (t ^ Suc k))) (at t)"
  unfolding eventually_at_filter
  by (auto simp del: power_Suc intro!: derivative_eq_intros eventuallyI)

lemma exp_inv_limit_0_right_gen':
  "((λ(t::real). inverse (t ^ k) / exp(inverse t))  0) (at_right 0)"
proof (induct k)
  case 0
  then show ?case
    using exp_inv_limit_0_right
    by (auto simp: exp_minus inverse_eq_divide)
next
  case (Suc k)
  have df: "F t in at_right 0. ((λx. inverse (x ^ Suc k)) has_real_derivative 
    - (inverse (t ^ k) * ((1 + real k)) * (inverse t ^ 2))) (at t)"
    unfolding eventually_at_filter
    apply (auto simp del: power_Suc intro!: derivative_eq_intros eventuallyI)
    by (auto simp: power2_eq_square)
  have dg: "F t in at_right 0. ((λx. exp (inverse x)) has_real_derivative
    - (exp (inverse t) * (inverse t ^ 2))) (at t)"
    unfolding eventually_at_filter
    by (auto simp del: power_Suc intro!: derivative_eq_intros eventuallyI simp: power2_eq_square)
  show ?case
    apply (rule lhopital_right_0_at_top [OF _ _ df dg])
      apply (rule filterlim_compose[where g = exp])
       apply (rule exp_at_top)
      apply (rule filterlim_inverse_at_top_right)
    subgoal by (auto simp: eventually_at_filter)
    subgoal
      apply (rule Lim_transform_eventually[where f = "λx. (1 + real k) * (inverse (x ^ k) / exp (inverse x))"])
      using Suc.hyps tendsto_mult_right_zero apply blast
      by (auto simp: eventually_at_filter)
    done
qed

lemma exp_inv_limit_0_right_gen:
  "((λ(t::real). exp(-inverse t) / t ^ k)  0) (at_right 0)"
  using exp_inv_limit_0_right_gen'[of k]
  by (metis (no_types, lifting) Groups.mult_ac(2) Lim_cong_within divide_inverse exp_minus)  

lemma f_limit_0_right: "(f  0) (at_right 0)"
proof -
  have "F t in at_right 0. (t::real) > 0"
    by (rule eventually_at_right_less)
  then have "F t in at_right 0. exp(-inverse t) = f t"
    by (eventually_elim) (auto simp: f_def)
  moreover have "((λ(t::real). exp(-inverse t))  0) (at_right 0)"
    by (rule exp_inv_limit_0_right)
  ultimately show ?thesis
    by (blast intro: Lim_transform_eventually)
qed

lemma f_limit_0: "(f  0) (at 0)"
  using _ f_limit_0_right
proof (rule filterlim_split_at_real)
  have "F t in at_left 0. 0 = f t"
    by (auto simp: f_def eventually_at_filter)
  then show "(f  0) (at_left 0)"
    by (blast intro: Lim_transform_eventually) 
qed

lemma f_tendsto: "(f  f x) (at x)"
proof -
  consider "x = 0" | "x < 0" | "x > 0" by arith
  then show ?thesis
  proof cases
    case 1
    then show ?thesis by (auto simp: f_limit_0 f_def)
  next
    case 2
    have "F t in at x. t < 0"
      apply (rule order_tendstoD)
      by (rule tendsto_intros) fact
    then have "F t in at x. 0 = f t"
      by (eventually_elim) (auto simp: f_def)
    then show ?thesis
      using x < 0 by (auto simp: f_def intro: Lim_transform_eventually)
  next
    case 3
    have "F t in at x. t > 0"
      apply (rule order_tendstoD)
      by (rule tendsto_intros) fact
    then have "F t in at x. exp(-inverse t) = f t"
      by (eventually_elim) (auto simp: f_def)
    moreover have "(λt. exp (- inverse t)) x f x"
      using x > 0 by (auto simp: f_def tendsto_intros )
    ultimately show ?thesis
      by (blast intro: Lim_transform_eventually)
  qed
qed

lemma f_continuous: "continuous_on S f"
  using f_tendsto continuous_on continuous_on_subset subset_UNIV by metis

lemma continuous_on_real_polynomial_function:
  "continuous_on S p" if "real_polynomial_function p"
  using that
  by induction (auto intro: continuous_intros linear_continuous_on)

lemma f_nth_derivative_is_poly:
  "higher_differentiable_on {0<..} f k 
   (p. real_polynomial_function p  (t>0. nth_derivative k f t 1 = p t / (t ^ (2 * k)) * exp(-inverse t)))"
proof (induction k)
  case 0
  then show ?case
    apply (auto simp: higher_differentiable_on.simps f_continuous)
    by (auto simp: f_def)
next
  case (Suc k)
  obtain p where fk: "higher_differentiable_on {0<..} f k"
    and p1: "real_polynomial_function p"
    and p2: "t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t)"
    using Suc by auto
  obtain p' where p'1: "real_polynomial_function p'"
    and p'2: "t. (p has_real_derivative (p' t)) (at t)"
    using has_real_derivative_polynomial_function[of p] p1 by auto

  define rp where "rp t = (t2 * p' t - 2 * real k * t * p t + p t)" for t
  have rp: "real_polynomial_function rp"
    unfolding rp_def
    by (auto intro!: real_polynomial_function.intros(2-) real_polynomial_function_diff
        p1 p'1 simp: power2_eq_square)
  moreover
  have fk': "(λx. nth_derivative k f x 1) differentiable at t" (is ?a)
    "frechet_derivative (λx. nth_derivative k f x 1) (at t) 1 =
        rp t * (exp (-inverse t) / t^(2*k+2))" (is ?b)
    if "0 < t" for t
  proof -
    from p'2 that have dp: "(p has_derivative ((*) (p' t))) (at t within {0<..})"
      by (auto simp: at_within_open[of _ "{0<..}"] has_field_derivative_def ac_simps)
    have "((λt. p t / t ^ (2 * k) * exp (- inverse t)) has_derivative
      (λv. v * rp t * (exp (-inverse t) / t^(2*k+2)))) (at t within {0<..})"
      using that
      apply (auto intro!: derivative_eq_intros dp ext)
      apply (simp add: divide_simps algebra_simps rp_def power2_eq_square)
      by (metis Suc_pred mult_is_0 neq0_conv power_Suc zero_neq_numeral)
    then have "((λx. nth_derivative k f x 1) has_derivative
      (λv. v * rp t * (exp (-inverse t) / t^(2*k+2)))) (at t within {0<..})"
      apply (rule has_derivative_transform_within[OF _ zero_less_one])
      using that p2 by auto
    then have "((λx. nth_derivative k f x 1) has_derivative
      (λv. v * rp t * (exp (-inverse t) / t^(2*k+2)))) (at t)"
      using that
      by (auto simp: at_within_open[of _ "{0<..}"])
    from frechet_derivative_at'[OF this] this
    show ?a ?b
      by (auto simp: differentiable_def)
  qed
  have hdS: "higher_differentiable_on {0<..} f (Suc k)"
    apply (subst higher_differentiable_on_real_Suc')
     apply (auto simp: fk fk' frechet_derivative_nth_derivative_commute[symmetric])
    apply (subst continuous_on_cong[OF refl])
     apply (rule fk')
    by (auto intro!: continuous_intros p'1 p1 rp
        intro: continuous_on_real_polynomial_function)
  moreover
  have "nth_derivative (Suc k) f t 1 = rp t / t ^ (2 * (Suc k)) * exp (- inverse t)"
    if "t > 0" for t
  proof -
    have "nth_derivative (Suc k) f t 1 = frechet_derivative (λx. nth_derivative k f x 1) (at t) 1"
      by (simp add: frechet_derivative_nth_derivative_commute)

    also have " = rp t / t^(2*k+2) * (exp (-inverse t))"
      using fk'[OF t > 0] by simp
    finally  show ?thesis by simp
  qed
  ultimately show ?case by blast
qed

lemma f_has_derivative_at_neg:
  " x < 0  (f has_derivative (λx. 0)) (at x)"
  by (rule has_derivative_transform_within_open[where f="λx. 0" and s="{..<0}"])
    (auto simp: f_def)

lemma f_differentiable_at_neg:
  "x < 0  f differentiable at x"
  using f_has_derivative_at_neg
  by (auto simp: differentiable_def)

lemma frechet_derivative_f_at_neg:
  "x  {..<0}  frechet_derivative f (at x) = (λx. 0)"
  by (rule frechet_derivative_at') (rule f_has_derivative_at_neg, simp)

lemma f_nth_derivative_lt_0:
  "higher_differentiable_on {..<0} f k  (t<0. nth_derivative k f t 1 = 0)"
proof (induction k)
  case 0
  have rewr: "a  {..<0}  ¬0 < a" for a::real by simp
  show ?case
    by (auto simp: higher_differentiable_on.simps f_def rewr
        simp del: lessThan_iff
        cong: continuous_on_cong)
next
  case (Suc k)
  have "t < 0  (λx. nth_derivative k f x 1) differentiable at t" for t
    by (rule differentiable_eqI[where g=0 and X="{..<0}"])
      (auto simp: zero_fun_def frechet_derivative_const Suc.IH)
  then have "frechet_derivative (λx. nth_derivative k f x 1) (at t) 1 = 0" if "t < 0" for t
    using that Suc.IH
    by (subst frechet_derivative_transform_within_open[where X="{..<0}" and g =0])
      (auto simp: frechet_derivative_zero_fun)
  with Suc show ?case
    by (auto simp: higher_differentiable_on.simps f_differentiable_at_neg
        frechet_derivative_f_at_neg zero_fun_def
        simp flip: frechet_derivative_nth_derivative_commute
        simp del: lessThan_iff
        intro!: higher_differentiable_on_const
        cong: higher_differentiable_on_cong)
qed

lemma netlimit_at_left: "netlimit (at_left x) = x" for x::real
  by (rule Lim_ident_at) simp

lemma netlimit_at_right: "netlimit (at_right x) = x" for x::real
  by (rule Lim_ident_at) simp


lemma has_derivative_split_at:
  "(g has_derivative g') (at x)"
  if
    "(g has_derivative g') (at_left x)"
    "(g has_derivative g') (at_right x)"
  for x::real
  using that
  unfolding has_derivative_def netlimit_at netlimit_at_right netlimit_at_left
  by (auto intro: filterlim_split_at)

lemma has_derivative_at_left_at_right':
  "(g has_derivative g') (at x)"
  if
    "(g has_derivative g') (at x within {..x})"
    "(g has_derivative g') (at x within {x..})"
  for x::real
  apply (rule has_derivative_split_at)
  subgoal by (rule has_derivative_subset) (fact, auto)
  subgoal by (rule has_derivative_subset) (fact, auto)
  done

lemma real_polynomial_function_tendsto:
  "(p  p x) (at x within X)" if "real_polynomial_function p"
  using that
  by (induction p) (auto intro!: tendsto_eq_intros intro: bounded_linear.tendsto)

lemma f_nth_derivative_cases:
  "higher_differentiable_on UNIV f k 
   (t0. nth_derivative k f t 1 = 0) 
   (p. real_polynomial_function p 
      (t>0. nth_derivative k f t 1 = p t / (t ^ (2 * k)) * exp(-inverse t)))"
proof (induction k)
  case 0
  then show ?case
    apply (auto simp: higher_differentiable_on.simps f_continuous)
    by (auto simp: f_def)
next
  case (Suc k)
  from Suc.IH obtain pk where IH:
    "higher_differentiable_on UNIV f k"
    "t. t  0  nth_derivative k f t 1 = 0"
    "real_polynomial_function pk"
    "t. t > 0  nth_derivative k f t 1 = pk t / t ^ (2 * k) * exp (- inverse t)"
    by auto
  from f_nth_derivative_lt_0[of "Suc k"]
    local.f_nth_derivative_is_poly[of "Suc k"]
  obtain p where neg: "higher_differentiable_on {..<0} f (Suc k)"
    and neg0: "(t<0. nth_derivative (Suc k) f t 1 = 0)"
    and pos: "higher_differentiable_on {0<..} f (Suc k)"
    and p: "real_polynomial_function p"
    "t. t > 0  nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)"
    by auto
  moreover
  have at_within_eq_at_right: "(at 0 within {0..}) = at_right (0::real)"
    apply (auto simp: filter_eq_iff eventually_at_filter )
     apply (simp add: eventually_mono)
    apply (simp add: eventually_mono)
    done
  have [simp]: "{0..} - {0} = {0::real<..}" by auto
  have [simp]: "(at (0::real) within {0..})  bot"
    by (auto simp: at_within_eq_bot_iff)
  have k_th_has_derivative_at_left:
    "((λx. nth_derivative k f x 1) has_derivative (λx. 0)) (at 0 within {..0})"
    apply (rule has_derivative_transform_within[OF _ zero_less_one])
      prefer 2
      apply force
     prefer 2
     apply (simp add: IH)
    by (rule derivative_intros)
  have k_th_has_derivative_at_right:
    "((λx. nth_derivative k f x 1) has_derivative (λx. 0)) (at 0 within {0..})"
    apply (rule has_derivative_transform_within[where
          f="λx'. if x' = 0 then 0 else pk x' / x' ^ (2 * k) * exp (- inverse x')", OF _ zero_less_one])
    subgoal
      unfolding has_derivative_def
      apply (auto simp: Lim_ident_at)
      apply (rule Lim_transform_eventually[where f="λx. (pk x * (exp (- inverse x) / x ^ (2 * k + 1)))"])
       apply (rule tendsto_eq_intros)
         apply (rule real_polynomial_function_tendsto[THEN tendsto_eq_rhs])
          apply fact
         apply (rule refl)
        apply (subst at_within_eq_at_right)
        apply (rule exp_inv_limit_0_right_gen)
      apply (auto simp add: eventually_at_filter divide_simps)
      done
    subgoal by force
    subgoal by (auto simp: IH(2) IH(4))
    done
  have k_th_has_derivative: "((λx. nth_derivative k f x 1) has_derivative (λx. 0)) (at 0)"
    apply (rule has_derivative_at_left_at_right')
     apply (rule k_th_has_derivative_at_left)
    apply (rule k_th_has_derivative_at_right)
    done
  have nth_Suc_zero: "nth_derivative (Suc k) f 0 1 = 0"
    apply (auto simp: frechet_derivative_nth_derivative_commute[symmetric])
    apply (subst frechet_derivative_at')
     apply (rule k_th_has_derivative)
    by simp
  moreover have "higher_differentiable_on UNIV f (Suc k)"
  proof -
    have "continuous_on UNIV (λx. nth_derivative (Suc k) f x 1)"
      unfolding continuous_on_eq_continuous_within
    proof
      fix x::real
      consider "x < 0" | "x > 0" | "x = 0" by arith
      then show "isCont (λx. nth_derivative (Suc k) f x 1) x"
      proof cases
        case 1
        then have at_eq: "at x = at x within {..<0}"
          using at_within_open[of x "{..<0}"] by auto
        show ?thesis
          unfolding at_eq
          apply (rule continuous_transform_within[OF _ zero_less_one])
          using neg0 1 by (auto simp: at_eq)
      next
        case 2
        then have at_eq: "at x = at x within {0<..}"
          using at_within_open[of x "{0<..}"] by auto
        show ?thesis
          unfolding at_eq
          apply (rule continuous_transform_within[OF _ zero_less_one])
          using p 2 by (auto intro!: continuous_intros
              intro: continuous_real_polymonial_function continuous_at_imp_continuous_within)
      next
        case 3
        have "((λx. nth_derivative (Suc k) f x 1)  0) (at_left 0)"
        proof -
          have "F x in at_left 0. 0 = nth_derivative (Suc k) f x 1"
            using neg0
            by (auto simp: eventually_at_filter)
          then show ?thesis
            by (blast intro: Lim_transform_eventually) 
        qed
        moreover have "((λx. nth_derivative (Suc k) f x 1)  0) (at_right 0)"
        proof -
          have "((λx. p x * (exp (- inverse x) / x ^ (2 * Suc k)))  0) (at_right 0)"
            apply (rule tendsto_eq_intros)
              apply (rule real_polynomial_function_tendsto)
              apply fact
             apply (rule exp_inv_limit_0_right_gen)
            by simp
          moreover
          have "F x in at_right 0. p x * (exp (- inverse x) / x ^ (2 * Suc k)) =
            nth_derivative (Suc k) f x 1"
            using p
            by (auto simp: eventually_at_filter)
          ultimately show ?thesis
            by (rule Lim_transform_eventually)
        qed
        ultimately show ?thesis
          by (auto simp: continuous_def nth_Suc_zero 3 filterlim_split_at
              simp del: nth_derivative.simps)
      qed
    qed
    moreover have "(λx. nth_derivative k f x 1) differentiable at x" for x
    proof -
      consider  "x = 0" | "x < 0" | "x > 0"by arith
      then show ?thesis
      proof cases
        case 1
        then show ?thesis
          using k_th_has_derivative by (auto simp: differentiable_def)
      next
        case 2
        with neg show ?thesis
          by (subst (asm) higher_differentiable_on_real_Suc') auto
      next
        case 3
        with pos show ?thesis
          by (subst (asm) higher_differentiable_on_real_Suc') auto
      qed
    qed
    moreover have "higher_differentiable_on UNIV f k" by fact
    ultimately
    show ?thesis
      by (subst higher_differentiable_on_real_Suc'[OF open_UNIV]) auto
  qed
  ultimately
  show ?case
    by (auto simp: less_eq_real_def)
qed

lemma f_smooth_on: "k-smooth_on S f"
  and f_higher_differentiable_on: "higher_differentiable_on S f n"
  using f_nth_derivative_cases
  by (auto simp: smooth_on_def higher_differentiable_on_subset[OF _ subset_UNIV])

lemma f_compose_smooth_on: "k-smooth_on S (λx. f (g x))"
  if "k-smooth_on S g" "open S"
  using smooth_on_compose[OF f_smooth_on that open_UNIV subset_UNIV]
  by (auto simp: o_def)

lemma f_nonneg: "f x  0"
  by (auto simp: f_def)

lemma f_pos_iff: "f x > 0  x > 0"
  by (auto simp: f_def)

lemma f_eq_zero_iff: "f x = 0  x  0"
  by (auto simp: f_def)


subsection ‹Cutoff function›

definition "h t = f (2 - t) / (f (2 - t) + f (t - 1))"

lemma denominator_pos: "f (2 - t) + f (t - 1) > 0"
  by (auto simp: f_def add_pos_pos)

lemma denominator_nonzero: "f (2 - t) + f (t - 1) = 0  False"
  using denominator_pos[of t] by auto

lemma h_range: "0  h t" "h t  1"
  by (auto simp: h_def f_nonneg denominator_pos)

lemma h_pos: "t < 2  0 < h t"
  and h_less_one: "1 < t  h t < 1"
  by (auto simp: h_def f_pos_iff denominator_pos)

lemma h_eq_0: "h t = 0" if "t  2"
  using that
  by (auto simp: h_def)

lemma h_eq_1: "h t = 1" if "t  1"
  using that
  by (auto simp: h_def f_eq_zero_iff)

lemma h_compose_smooth_on: "k-smooth_on S (λx. h (g x))"
  if "k-smooth_on S g" "open S"
  by (auto simp: h_def[abs_def] denominator_nonzero
      intro!: smooth_on_divide f_compose_smooth_on smooth_on_minus smooth_on_add
      that)


subsection ‹Bump function›

definition H::"_::real_inner  real" where "H x = h (norm x)"

lemma H_range: "0  H x" "H x  1"
  by (auto simp: H_def h_range)

lemma H_eq_one: "H x = 1" if "x  cball 0 1"
  using that
  by (auto simp: H_def h_eq_1)

lemma H_pos: "H x > 0" if "x  ball 0 2"
  using that
  by (auto simp: H_def h_pos)

lemma H_eq_zero: "H x = 0" if "x  ball 0 2"
  using that
  by (auto simp: H_def h_eq_0)

lemma H_neq_zeroD: "H x  0  x  ball 0 2"
  using H_eq_zero by blast

lemma H_smooth_on: "k-smooth_on UNIV H"
proof -
  have 1: "k-smooth_on (ball 0 1) H"
    by (rule smooth_on_cong[where g="λx. 1"]) (auto simp: H_eq_one)
  have 2: "k-smooth_on (UNIV - cball 0 (1/2)) H"
    by (auto simp: H_def[abs_def]
        intro!: h_compose_smooth_on smooth_on_norm)
  have O: "open (ball 0 1)" "open (UNIV - cball 0 (1 / 2))"
    by auto
  have *: "ball 0 1  (UNIV - cball 0 (1 / 2)) = UNIV" by (auto simp: mem_ball)
  from smooth_on_open_Un[OF 1 2 O, unfolded *]
  show ?thesis
    by (rule smooth_on_subset) auto
qed

lemma H_compose_smooth_on: "k-smooth_on S (λx. H (g x))" if "k-smooth_on S g" "open S"
  for g :: "_  _::euclidean_space"
  using smooth_on_compose[OF H_smooth_on that]
  by (auto simp: o_def)

end

end