Theory Affine_Functions

(***********************************************************************************
 * Copyright (c) University of Exeter, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *
 * SPDX-License-Identifier: BSD-3-Clause
 ***********************************************************************************)

chapter‹Affine Functions›

text‹
  In this theory, we provide formalisation of affine functions (sometimes also called linear 
  polynomial functions).
›

theory
  Affine_Functions
  imports
  Complex_Main
begin

section‹Definition of Affine Functions, Alternative Definitions, and Special Cases›

locale affine_fun =
  fixes f 
  assumes ‹∃ b. linear (λ x. f x - b)›

lemma affine_fun_alt: 
  ‹affine_fun f = (∃ c g. (f = (λ x. g x + c)) ∧ linear g)›
  unfolding affine_fun_def
  by(safe, force, simp add: Real_Vector_Spaces.linear_iff) 

lemma affine_fun_real_linfun: 
  ‹affine_fun (f::(real ⇒ real)) = (∃ a b . f = (λ x. a * x + b))›
  by(simp add: affine_fun_alt, metis real_linearD linear_times)

lemma linear_is_affine_fun: ‹linear f ⟹ affine_fun f›
  by (standard, simp add: Real_Vector_Spaces.linear_iff)

lemma affine_zero_is_linear: assumes ‹affine_fun f› and ‹f 0 = 0› shows ‹linear f›
  apply(insert assms) 
  unfolding affine_fun_def 
  using linear_0 by fastforce

lemma affine_add: 
  assumes ‹affine_fun f› and ‹affine_fun g›
  shows ‹affine_fun (λ x. f x + g x)›
  using assms  linear_compose_add
  by(auto simp add: affine_fun_alt, force) 

lemma scaleR:
  assumes ‹affine_fun f › shows ‹affine_fun (λ x. a *⇩R (f x))›
  using assms 
  apply(simp add: affine_fun_alt)
  by (metis linear_compose_scale_right scaleR_right_distrib) 
 
lemma real_affine_funD:
  fixes f :: "real ⇒ real"
  assumes "affine_fun f" obtains c b where "f = (λ x. c * x + b)"
  using assms  
  apply(simp add: affine_fun_alt)
  by (metis real_linearD) 


section‹Common Linear Polynomial Functions›

lemma affine_fun_const[simp]: ‹affine_fun (λ x. c)›
  apply(simp add: affine_fun_alt)
  using module_hom_zero by force 

lemma affine_fun_id[simp]: ‹affine_fun (λ x. x)›
  by (simp add: linear_is_affine_fun module_hom_ident)

lemma affine_fun_mult[simp]: ‹affine_fun (λ x. (c::'a::real_algebra) * x)›
  by(simp add: linear_is_affine_fun)

lemma affine_fun_scaled[simp]: ‹affine_fun (λ x. x /c )›
  for c :: "'a::real_normed_field"
  using bounded_linear_divide[of c] linear_is_affine_fun[of " (λ x. x /c )"] bounded_linear.linear 
  by blast 

lemma affine_fun_add[simp]: ‹affine_fun (λ x. x + c)›
  apply(simp add: affine_fun_alt)
  using module_hom_ident by force 

lemma affine_fun_diff[simp]: ‹affine_fun (λ x. x - c)›
  apply(simp add: affine_fun_alt)
  using module_hom_ident by force 

lemma affine_fun_triv[simp]: ‹affine_fun (λ x. a *⇩R x + c)›
  apply(simp add: affine_fun_alt)
  by fastforce 
 
lemma affine_fun_add_const[simp]: assumes ‹affine_fun f› shows ‹affine_fun (λ x. (f x) + c)›
  using assms apply(simp add:affine_fun_alt)
  by (metis add.commute add.left_commute)

lemma affine_fun_diff_const[simp]: assumes ‹affine_fun f› shows ‹affine_fun (λ x. (f x) - c)›
  using assms apply(simp add:affine_fun_alt) by force

lemma affine_fun_comp[simp]: assumes ‹affine_fun (f)›
and ‹affine_fun (g)› shows ‹affine_fun (f ∘ g)›
  using assms 
  unfolding affine_fun_alt
  apply(simp add:o_def)
  using linear_add linear_compose[simplified o_def] add.assoc
  by metis 

lemma affine_fun_linear[simp]: assumes ‹affine_fun f› shows ‹affine_fun (λ x. a *⇩R (f x) + c)›
  by(rule affine_fun_comp[of "λ x. a *⇩R x + c" f, simplified o_def], simp_all add: assms)  


section‹Linear Polynomial Functions and Orderings›

lemma affine_fun_leq_pos: 
assumes ‹affine_fun (f::real ⇒ real)› and ‹affine_fun g› 
and ‹x∈{0..u}›  and ‹(f 0 ≤ g 0 )›  and ‹(f u ≤ g u)› 
shows ‹f x ≤ g x›
  using assms 
  apply(auto simp add: linear_0 affine_fun_real_linfun)[1]
  by (smt (verit) left_diff_distrib mult_left_mono_neg mult_right_mono) 

lemma affine_fun_leq_neg:
assumes ‹affine_fun (f::real ⇒ real)› and ‹affine_fun g› 
and ‹x∈{l..0}›  and ‹(f l ≤ g l )›  and ‹(f 0 ≤ g 0)› 
shows ‹f x ≤ g x›
  using assms
  apply(auto simp add: linear_0 affine_fun_real_linfun)[1]
  using Groups.mult_ac(2) left_diff_distrib mult_right_mono
  by (smt (verit, ccfv_SIG))

lemma affine_fun_leq: 
assumes ‹affine_fun (f::real ⇒ real)› and ‹affine_fun g› 
and ‹x∈{l..u}›  and ‹(f l ≤ g l )›  and ‹(f u ≤ g u)› 
shows ‹f x ≤ g (x::real)›
  using assms affine_fun_leq_neg[of f g x l] affine_fun_leq_pos[of f g x u]
  apply(simp add: linear_0 affine_fun_real_linfun)
  by (smt (verit, ccfv_SIG) left_diff_distrib mult_left_mono_neg)


lemma affine_fun_le_pos: 
assumes ‹affine_fun (f::real ⇒ real)› and ‹affine_fun g› 
and ‹x∈{0..u}›  and ‹(f 0 < g 0 )›  and ‹(f u < g u)› 
shows ‹f x < g (x::real)›
  using assms  
  apply(auto simp add: linear_0 affine_fun_real_linfun)[1]
  using Groups.mult_ac(2) left_diff_distrib mult_right_mono 
  by (smt (verit, best))

lemma affine_fun_le_neg: 
assumes ‹affine_fun (f::real ⇒ real)› and ‹affine_fun g› 
and ‹x∈{l..0}›  and ‹(f l < g l )›  and ‹(f 0 < g 0)› 
shows ‹f x < g (x::real)›
  using assms  
  apply(auto simp add: linear_0 affine_fun_real_linfun)[1]
  using Groups.mult_ac(2) left_diff_distrib mult_right_mono 
  by (smt (verit, ccfv_SIG)) 

lemma affine_fun_le: 
assumes ‹affine_fun (f::real ⇒ real)› and ‹affine_fun g› 
and ‹x∈{l..u}›  and ‹(f l < g l )›  and ‹(f u < g u)› 
shows ‹f x < g (x::real)›
  using assms affine_fun_le_neg[of f g x l] affine_fun_le_pos[of f g x u]
  apply(simp add: linear_0 affine_fun_real_linfun)
  by (smt (verit, ccfv_SIG) left_diff_distrib mult_left_mono_neg)

end