TITLE: Problem proving $\int_{-\infty}^{\infty}x^2e^{-x^2}H_n(x)H_m(x)dx$
QUESTION [3 upvotes]: I am trying to show that the value of the following integral is:
$$\int_{-\infty}^{\infty}x^2e^{-x^2}H_n(x)H_m(x)dx=2^{n-1}\pi^{\frac{1}{2}}(2n+1)n!\delta_{mn}+2^n\pi^{\frac{1}{2}}(n+2)!\delta_{(n+2)m}+2^{n-2}\pi^{\frac{1}{2}}n!\delta_{(n-2)m},$$
where $H_n$ is the $n$-th Hermite polynomial.
My attempt is the following:
Suppose that the value of the integral is already known and that:
\begin{equation*}
\int_{-\infty}^{\infty}x^2e^{-x^2}H_n(x)H_m(x)dx=\lambda
\end{equation*}
From the recurrence relation we have to:
\begin{equation*}
H_{n+1}(x)=2xH_{n}(x)-2nH_{n-1}(x)
\end{equation*}
Therefore, since it is valid for any $ n $ then it will also be valid for any $ m $, that is:
\begin{equation*}
H_{m+1}(x)=2xH_m(x)-2mH_{m-1}(x)
\end{equation*}
Solving for the terms $2xH_ {m} (x)$ and $2xH_ {n} (x)$ we have:
\begin{align}
2xH_ {n} (x) & = H_ {n + 1} (x) + 2nH_ {n-1} (x) \\
2xH_ {m} (x) & = H_ {m + 1} (x) + 2mH_ {m-1} (x)
\end{align}
And multiplying the \ textcolor {red} {\ textbf {equation 1}} by $ 2xH_m (x) $ and substituting the cleared value we have:
\begin{align*}
4x^2H_{n}(x)H_{m}(x)&=2xH_m(x)\left[H_{n+1}(x)+2nH_{n-1}(x)\right]\\
4x^2H_{n}(x)H_{m}(x)&=\left[H_{m+1}(x)+2mH_{m-1}(x)\right]\left[H_{n+1}(x)+2nH_{n-1}(x)\right]\\
4x^2H_{n}(x)H_{m}(x)&= H_{m+1}(x)H_{n+1}(x)+2nH_{m+1}(x)H_{n-1}(x)+2mH_{m-1}(x)H_{n+1}(x)+4mnH_{m-1}(x)H_{n-1}(x)\\
\end{align*}
And from what we have just found we can conclude that:
{\begin{align*}
4\lambda&=\int_{-\infty}^{\infty}e^{-x^2}\left[H_{m+1}(x)H_{n+1}(x)\right]dx+\int_{-\infty}^{\infty}e^{-x^2}2nH_{m+1}(x)H_{n-1}(x)dx+\int_{-\infty}^{\infty}2me^{-x^2}H_{m-1}(x)H_{n+1}(x)+\int_{-\infty}^{\infty}4mne^{-x^2}H_{m-1}(x)H_{n-1}(x)dx
\end{align*}
So going back to the integral that we already had:
\begin{align*}
\cfrac{1}{4}\times4\lambda&=\cfrac{1}{4}\times \sqrt{\pi}\left\{2^{n+1}(n+1)!\left[\delta_{(m+1)(n+1)}+2m\delta_{(m-1)(n+1)}\right]+2^{n-1}(n-1)!\left[\delta_{(m+1)(n-1)}2n+4mn\delta_{(m-1)(n-1)}\right]\right\}\\
\lambda&=\cfrac{\sqrt{\pi}}{4}\left\{2^{n+1}(n+1)!\left[\delta_{(m+1)(n+1)}+2m\delta_{(m-1)(n+1)}\right]+2^{n-1}(n-1)!\left[\delta_{(m+1)(n-1)}2n+4mn\delta_{(m-1)(n-1)}\right]\right\}\\
\end{align*}
And as it was supposed from the beginning:
\begin{equation*}
\int_{-\infty}^{\infty}x^2e^{-x^2}H_n(x)H_m(x)dx=\lambda
\end{equation*}
Then finally it will come to:
$\int_{-\infty}^{\infty}x^2e^{-x^2}H_n(x)H_m(x)dx=\cfrac{\sqrt{\pi}}{4}\left\{2^{n+1}(n+1)!\left[\delta_{(m+1)(n+1)}+2m\delta_{(m-1)(n+1)}\right]+2^{n-1}(n-1)!\left[\delta_{(m+1)(n-1)}2n+4mn\delta_{(m-1)(n-1)}\right]\right\}$
But I can't find the way to give the answer $2^{n-1}\pi^{\frac{1}{2}}(2n+1)n!\delta_{mn}+2^n\pi^{\frac{1}{2}}(n+2)!\delta_{(n+2)m}+2^{n-2}\pi^{\frac{1}{2}}n!\delta_{(n-2)m}$

REPLY [0 votes]: Starting from here
$$
\cfrac{\sqrt{\pi}}{4}\left\{2^{n+1}(n+1)!\left[\delta_{(m+1)(n+1)}+2m\delta_{(m-1)(n+1)}\right]+2^{n-1}(n-1)!\left[\delta_{(m+1)(n-1)}2n+4mn\delta_{(m-1)(n-1)}\right]\right\}
$$
First, rewrite the $\delta$s so that they all have only $m$. We do this by noting that, for example, if $m-1 = n+1$, then $m = n+2$, so $\delta_{(m-1)(n+1)} = \delta_{m(n+2)}$. We can then also use $m\delta_{m(n+2)} = (n+2)\delta_{m(n+2)}$ to further simplify. This gives
$$
\cfrac{\sqrt{\pi}}{4}\left\{2^{n+1}(n+1)!\left[\delta_{mn}+2(n+2)\delta_{m(n+2)}\right]+2^{n-1}(n-1)!\left[\delta_{m(n-2)}2n+4n^2\delta_{mn}\right]\right\}
$$
Now expand the products:
$$
\sqrt{\pi}\left[2^{n-1}(n+1)!\delta_{mn}+2^{n}(n+2)(n+1)!\delta_{m(n+2)}+2^{n-2}n(n-1)!\delta_{m(n-2)}+2^{n-1}n^2(n-1)!\delta_{mn}\right]
$$
Finally, collect terms and simplify the factorials to get
$$
\sqrt{\pi}\left[2^{n-1}(2n+1)n!\delta_{mn}+2^{n}(n+2)!\delta_{m(n+2)}+2^{n-2}n!\delta_{m(n-2)}\right]
$$


TITLE: Accumulation points with respect to Zariski Topology on $\mathbb{R}$.
QUESTION [1 upvotes]: Consider the topology on $\mathbb{R}$  : the closed sets are given by the finite sets and $\mathbb{R}$ (basically the Zariski Topology on $\mathbb{R}$).
Let $(x_n)_{n \in \mathbb{N} }$ be a sequence in $\mathbb{R}$.

How do we show : if $l$ is a limit of the sequence $(x_n)_{n \in \mathbb{N} }$  if and only if for all $x \neq l$, the number of indices $n$ such that $x_n = x$ is finite.

Determine the accumulation points of the sequence $(x_n)_{n \in \mathbb{N} }$ w.r.t. Zariski topology

REPLY [0 votes]: You can translate the definition of “being a limit” using closed sets:
$ $          for every closed set $C$ not containing $l$, there exists $m$ such that, for $n>m$, $x_n\notin C$
The closed sets non containing $l$ are necessarily finite.
Suppose $l$ is a limit of the sequence. Then, taking $C=\{x\}$, with $x\ne l$, we see that the set $\{n\in\mathbb{N}:x_n=x\}$ is upper bounded, hence finite.
Suppose $l$ satisfies the condition about finiteness. Take a closed set $C$ not containing $l$. Then $C=\{r_1,r_2,\dots,r_k\}$ is finite and you should be able to finish up.
What about accumulation points of the sequence? Using Kelley's terminology, a sequence is convergent to $l$ if (and only if) it is eventually in every (open) neighborhood of $l$ (it belongs there from a certain point on). The point $l$ is an accumulation point if (and only if) it is frequently in every (open) neighborhood of $l$ (for every $m$, there is $n$ such that $n>m$ and $x_n$ is in the given neighborhood).
If $l$ is an accumulation point of the sequence and $x\ne l$, for every $m$ there is $n>m$ such that $x_n\ne x$. In particular, $\{n\in\mathbb{N}:x_n\ne x\}$ is infinite.
Can you finish with the converse?


TITLE: polynomial rings in two variables
QUESTION [1 upvotes]: Why  are not the rings $F[x,y]/(y^2-x)$ and $F[x,y]/(y^2-x^2)$ isomorphic? (Where $F$ is an arbitrary field)
Roughly speaking, I realize that $F[x,y]/(y^2 -x)$ "behaves" as $F[y]$ while $F[x,y]/(y^2 -x^2)$ "behaves" as $F[y] \oplus xF[y]$, but how can I prove that with a formal argument?

REPLY [1 votes]: Hint: the unique homomorphism from $F[y]$ to $F[x, y]/(y^2-x)$ that sends $y$ to the equivalence class $[y]$ is an isomorphism. So, as you say, $F[x, y]/(y^2-x)$ "behaves" exactly like $F[y]$ and, in particular, it is an integral domain. But, in $F[x, y]/(y^2-x^2)$, the elements $[x + y]$ and $[x - y]$ are non-zero (because the ideal $(y^2 - x^2)$ doesn't contain any polynomials of total degree less than $2$) and $[x + y]\cdot[x - y] = [(x + y)\cdot(x - y)] = [x^2 - y^2]= 0$, so $F[x, y]/(y^2-x^2)$ has non-trivial zero divisors and is not an integral domain.


text:
section \<open>Automation\<close>
theory Automation
imports Hoare_Triple (*"../Lib/Refine_Util"*)
begin

text \<open>
  In this theory, we provide a set of tactics and a simplifier setup for easy
  reasoning with our separation logic.
\<close>

subsection \<open>Normalization of Assertions\<close>
text \<open>
  In this section, we provide a set of lemmas and a simplifier
  setup to bring assertions to a normal form. We provide a simproc that
  detects pure parts of assertions and duplicate pointers. Moreover,
  we provide ac-rules for assertions. See Section~\ref{sec:auto:overview}
  for a short overview of the available proof methods.
\<close>

lemmas assn_aci =
  inf_aci[where 'a=assn]
  sup_aci[where 'a=assn]
  mult.left_ac[where 'a=assn]

lemmas star_assoc = mult.assoc[where 'a=assn]
lemmas assn_assoc =
  mult.left_assoc inf_assoc[where 'a=assn] sup_assoc[where 'a=assn]

lemma merge_true_star_ctx: "true * (true * P) = true * P"
  by (simp add: mult.left_ac)

lemmas star_aci =
  mult.assoc[where 'a=assn] mult.commute[where 'a=assn] mult.left_commute[where 'a=assn]
  assn_one_left mult_1_right[where 'a=assn]
  merge_true_star merge_true_star_ctx

text \<open>Move existential quantifiers to the front of assertions\<close>
lemma ex_assn_move_out[simp]:
  "\<And>Q R. (\<exists>\<^sub>Ax. Q x) * R = (\<exists>\<^sub>Ax. (Q x * R))"
  "\<And>Q R. R * (\<exists>\<^sub>Ax. Q x) = (\<exists>\<^sub>Ax. (R * Q x))"

  "\<And>P Q. (\<exists>\<^sub>Ax. Q x) \<and>\<^sub>A P = (\<exists>\<^sub>Ax. (Q x \<and>\<^sub>A P)) "
  "\<And>P Q. Q \<and>\<^sub>A (\<exists>\<^sub>Ax. P x) = (\<exists>\<^sub>Ax. (Q \<and>\<^sub>A P x))"

  "\<And>P Q. (\<exists>\<^sub>Ax. Q x) \<or>\<^sub>A P = (\<exists>\<^sub>Ax. (Q x \<or>\<^sub>A P))"
  "\<And>P Q. Q \<or>\<^sub>A (\<exists>\<^sub>Ax. P x) = (\<exists>\<^sub>Ax. (Q \<or>\<^sub>A P x))"
  apply -
  apply (simp add: ex_distrib_star)
  apply (subst mult.commute)
  apply (subst (2) mult.commute)
  apply (simp add: ex_distrib_star)

  apply (simp add: ex_distrib_and)
  apply (subst inf_commute)
  apply (subst (2) inf_commute)
  apply (simp add: ex_distrib_and)

  apply (simp add: ex_distrib_or)
  apply (subst sup_commute)
  apply (subst (2) sup_commute)
  apply (simp add: ex_distrib_or)
  done

text \<open>Extract pure assertions from and-clauses\<close>
lemma and_extract_pure_left_iff[simp]: "\<up>b \<and>\<^sub>A Q = (emp\<and>\<^sub>AQ)*\<up>b"
  by (cases b) auto

lemma and_extract_pure_left_ctx_iff[simp]: "P*\<up>b \<and>\<^sub>A Q = (P\<and>\<^sub>AQ)*\<up>b"
  by (cases b) auto

lemma and_extract_pure_right_iff[simp]: "P \<and>\<^sub>A \<up>b = (emp\<and>\<^sub>AP)*\<up>b"
  by (cases b) (auto simp: assn_aci)

lemma and_extract_pure_right_ctx_iff[simp]: "P \<and>\<^sub>A Q*\<up>b = (P\<and>\<^sub>AQ)*\<up>b"
  by (cases b) auto

lemmas and_extract_pure_iff =
  and_extract_pure_left_iff and_extract_pure_left_ctx_iff
  and_extract_pure_right_iff and_extract_pure_right_ctx_iff

lemmas norm_assertion_simps =
  (* Neutral elements *)
  mult_1[where 'a=assn] mult_1_right[where 'a=assn]
  inf_top_left[where 'a=assn] inf_top_right[where 'a=assn]
  sup_bot_left[where 'a=assn] sup_bot_right[where 'a=assn]

  (* Zero elements *)
  star_false_left star_false_right
  inf_bot_left[where 'a=assn] inf_bot_right[where 'a=assn]
  sup_top_left[where 'a=assn] sup_top_right[where 'a=assn]

  (* Associativity *)
  mult.left_assoc[where 'a=assn]
  inf_assoc[where 'a=assn]
  sup_assoc[where 'a=assn]

  (* Existential Quantifiers *)
  ex_assn_move_out ex_assn_const

  (* Extract pure assertions from conjunctions *)
  and_extract_pure_iff

  (* Merging *)
  merge_pure_star merge_pure_and merge_pure_or
  merge_true_star
  inf_idem[where 'a=assn] sup_idem[where 'a=assn]

  (* Duplicated References *)
  sngr_same_false snga_same_false

subsubsection \<open>Simplifier Setup Fine-Tuning\<close>
text \<open>Imperative HOL likes to simplify pointer inequations to this strange
  operator. We do some additional simplifier setup here\<close>
lemma not_same_noteqr[simp]: "\<not> a=!=a"
  by (metis Ref.unequal)
declare Ref.noteq_irrefl[dest!]

lemma not_same_noteqa[simp]: "\<not> a=!!=a"
  by (metis Array.unequal)
declare Array.noteq_irrefl[dest!]

text \<open>However, it is safest to disable this rewriting, as there is
  a working standard simplifier setup for \<open>(\<noteq>)\<close>
\<close>
declare Ref.unequal[simp del]
declare Array.unequal[simp del]

subsection \<open>Normalization of Entailments\<close>

text \<open>Used by existential quantifier extraction tactic\<close>
lemma enorm_exI': (* Incomplete, as chosen x may depend on heap! *)
  "(\<And>x. Z x \<longrightarrow> (P \<Longrightarrow>\<^sub>A Q x)) \<Longrightarrow> (\<exists>x. Z x) \<longrightarrow> (P \<Longrightarrow>\<^sub>A (\<exists>\<^sub>Ax. Q x))"
  by (metis ent_ex_postI)

text \<open>Example of how to build an extraction lemma.\<close>
thm enorm_exI'[OF enorm_exI'[OF imp_refl]]

lemmas ent_triv = ent_true ent_false

text \<open>Dummy rule to detect Hoare triple goal\<close>
lemma is_hoare_triple: "<P> c <Q> \<Longrightarrow> <P> c <Q>" .
text \<open>Dummy rule to detect entailment goal\<close>
lemma is_entails: "P\<Longrightarrow>\<^sub>AQ \<Longrightarrow> P \<Longrightarrow>\<^sub>AQ" .

subsection \<open>Frame Matcher\<close>
text \<open>Given star-lists P,Q and a frame F, this method tries to match
  all elements of Q with corresponding elements of P. The result is a
  partial match, that contains matching pairs and the unmatched content.\<close>

text \<open>The frame-matcher internally uses syntactic lists separated by
  star, and delimited by the special symbol \<open>SLN\<close>, which is defined
  to be \<open>emp\<close>.\<close>
definition [simp]: "SLN \<equiv> emp"
lemma SLN_left: "SLN * P = P" by simp
lemma SLN_right: "P * SLN = P" by simp

lemmas SLN_normalize = SLN_right mult.left_assoc[where 'a=assn]
lemmas SLN_strip = SLN_right SLN_left mult.left_assoc[where 'a=assn]

text \<open>A query to the frame matcher. Contains the assertions
  P and Q that shall be matched, as well as a frame F, that is not
  touched.\<close>

definition [simp]: "FI_QUERY P Q F \<equiv> P \<Longrightarrow>\<^sub>A Q*F"

abbreviation "fi_m_fst M \<equiv> foldr (*) (map fst M) emp"
abbreviation "fi_m_snd M \<equiv> foldr (*) (map snd M) emp"
abbreviation "fi_m_match M \<equiv> (\<forall>(p,q)\<in>set M. p \<Longrightarrow>\<^sub>A q)"

text \<open>A result of the frame matcher. Contains a list of matching pairs,
  as well as the unmatched parts of P and Q, and the frame F.
\<close>
definition [simp]: "FI_RESULT M UP UQ F \<equiv>
  fi_m_match M \<longrightarrow> (fi_m_fst M * UP \<Longrightarrow>\<^sub>A fi_m_snd M * UQ * F)"

text \<open>Internal structure used by the frame matcher:
  m contains the matched pairs; p,q the assertions that still needs to be
  matched; up,uq the assertions that could not be matched; and f the frame.
  p and q are SLN-delimited syntactic lists.
\<close>

definition [simp]: "FI m p q up uq f \<equiv>
  fi_m_match m \<longrightarrow> (fi_m_fst m * p * up \<Longrightarrow>\<^sub>A fi_m_snd m * q * uq * f)"

text \<open>Initialize processing of query\<close>
lemma FI_init:
  assumes "FI [] (SLN*P) (SLN*Q) SLN SLN F"
  shows "FI_QUERY P Q F"
  using assms by simp

text \<open>Construct result from internal representation\<close>
lemma FI_finalize:
  assumes "FI_RESULT m (p*up) (q*uq) f"
  shows "FI m p q up uq f"
  using assms by (simp add: assn_aci)

text \<open>Auxiliary lemma to show that all matching pairs together form
  an entailment. This is required for most applications.\<close>
lemma fi_match_entails:
  assumes "fi_m_match m"
  shows "fi_m_fst m \<Longrightarrow>\<^sub>A fi_m_snd m"
  using assms apply (induct m)
  apply (simp_all split: prod.split_asm add: ent_star_mono)
  done

text \<open>Internally, the frame matcher tries to match the first assertion
  of q with the first assertion of p. If no match is found, the first
  assertion of p is discarded. If no match for any assertion in p can be
  found, the first assertion of q is discarded.\<close>

text \<open>Match\<close>
lemma FI_match:
  assumes "p \<Longrightarrow>\<^sub>A q"
  assumes "FI ((p,q)#m) (ps*up) (qs*uq) SLN SLN f"
  shows "FI m (ps*p) (qs*q) up uq f"
  using assms unfolding FI_def
  by (simp add: assn_aci)

text \<open>No match\<close>
lemma FI_p_nomatch:
  assumes "FI m ps (qs*q) (p*up) uq f"
  shows "FI m (ps*p) (qs*q) up uq f"
  using assms unfolding FI_def
  by (simp add: assn_aci)

text \<open>Head of q could not be matched\<close>
lemma FI_q_nomatch:
  assumes "FI m (SLN*up) qs SLN (q*uq) f"
  shows "FI m SLN (qs*q) up uq f"
  using assms unfolding FI_def
  by (simp add: assn_aci)

subsection \<open>Frame Inference\<close>
lemma frame_inference_init:
  assumes "FI_QUERY P Q F"
  shows "P \<Longrightarrow>\<^sub>A Q * F"
  using assms by simp

lemma frame_inference_finalize:
  shows "FI_RESULT M F emp F"
  apply simp
  apply rule
  apply (drule fi_match_entails)
  apply (rule ent_star_mono[OF _ ent_refl])
  apply assumption
  done

subsection \<open>Entailment Solver\<close>
lemma entails_solve_init:
  "FI_QUERY P Q true \<Longrightarrow> P \<Longrightarrow>\<^sub>A Q * true"
  "FI_QUERY P Q emp \<Longrightarrow> P \<Longrightarrow>\<^sub>A Q"
  by (simp_all add: assn_aci)

lemma entails_solve_finalize:
  "FI_RESULT M P emp true"
  "FI_RESULT M emp emp emp"
  by (auto simp add: fi_match_entails intro: ent_star_mono)

lemmas solve_ent_preprocess_simps =
  ent_pure_post_iff ent_pure_post_iff_sng ent_pure_pre_iff ent_pure_pre_iff_sng

subsection \<open>Verification Condition Generator\<close>

lemmas normalize_rules = norm_pre_ex_rule norm_pre_pure_rule

(* Originally we introduced backwards-reasoning here, via
  cons_pre_rule[OF _ return_wp_rule] (old name: complete_return_cons).
  This only works, if the postcondition is not schematic! However, for
  forward reasoning, one usually assumes a schematic postcondition!
  *)
text \<open>May be useful in simple, manual proofs, where the postcondition
  is no schematic variable.\<close>
lemmas return_cons_rule = cons_pre_rule[OF _ return_wp_rule]

text \<open>Useful frame-rule variant for manual proof:\<close>
lemma frame_rule_left:
  "<P> c <Q> \<Longrightarrow> <R * P> c <\<lambda>x. R * Q x>"
  using frame_rule by (simp add: assn_aci)

lemmas deconstruct_rules =
  bind_rule if_rule false_rule return_sp_rule let_rule
  case_prod_rule case_list_rule case_option_rule case_sum_rule

lemmas heap_rules =
  ref_rule
  lookup_rule
  update_rule
  new_rule
  make_rule
  of_list_rule
  length_rule
  nth_rule
  upd_rule
  freeze_rule

lemma fi_rule:
  assumes CMD: "<P> c <Q>"
  assumes FRAME: "Ps \<Longrightarrow>\<^sub>A P * F"
  shows "<Ps> c <\<lambda>x. Q x * F>"
  apply (rule cons_pre_rule[rotated])
  apply (rule frame_rule)
  apply (rule CMD)
  apply (rule FRAME)
  done

subsection \<open>ML-setup\<close>

named_theorems sep_dflt_simps "Seplogic: Default simplification rules for automated solvers"
named_theorems sep_eintros "Seplogic: Intro rules for entailment solver"
named_theorems sep_heap_rules "Seplogic: VCG heap rules"
named_theorems sep_decon_rules "Seplogic: VCG deconstruct rules"

ML \<open>
infix 1 THEN_IGNORE_NEWGOALS

structure Seplogic_Auto =
struct

  (***********************************)
  (*             Tools               *)
  (***********************************)

  (* Repeat tac on subgoal. Determinize each step.
     Stop if tac fails or subgoal is solved. *)
  fun REPEAT_DETERM' tac i st = let
    val n = Thm.nprems_of st
  in
    REPEAT_DETERM (COND (has_fewer_prems n) no_tac (tac i)) st
  end

  (***********************************)
  (*             Debugging           *)
  (***********************************)
  fun tr_term t = Pretty.string_of (Syntax.pretty_term @{context} t);

  (***********************************)
  (*        Custom Tacticals         *)
  (***********************************)

  (* Apply tac1, and then tac2 with an offset such that anything left
     over by tac1 is skipped.

     The typical usage of this tactic is, if a theorem is instantiated
     with another theorem that produces additional goals that should
     be ignored first. Here, it is used in the vcg to ensure that
     frame inference is done before additional premises (that may
     depend on the frame) are discharged.
  *)
  fun (tac1 THEN_IGNORE_NEWGOALS tac2) i st = let
    val np = Thm.nprems_of st
  in
    (tac1 i THEN (fn st' => let val np' = Thm.nprems_of st' in
      if np'<np then tac2 i st'
      else tac2 (i+(np'-np)+1) st'
    end)) st
  end;

  (***********************************)
  (*     Assertion Normalization     *)
  (***********************************)
  (* Find two terms in a list whose key is equal *)
  fun find_similar (key_of:term -> term) (ts:term list) = let
    fun frec _ [] = NONE
    | frec tab (t::ts) = let val k=key_of t in
      if Termtab.defined tab k then
        SOME (the (Termtab.lookup tab k),t)
      else frec (Termtab.update (k,t) tab) ts
    end
  in
    frec Termtab.empty ts
  end;

  (* Perform DFS over term with binary operator opN, threading through
    a state. Atomic terms are transformed by tr. Supports omission of
    terms from the result structure by transforming them to NONE. *)
  fun dfs_opr opN (tr:'state -> term -> ('state*term option))
    d (t as ((op_t as Const (fN,_))$t1$t2)) =
    if fN = opN then let
        val (d1,t1') = dfs_opr opN tr d t1;
        val (d2,t2') = dfs_opr opN tr d1 t2;
      in
        case (t1',t2') of
          (NONE,NONE) => (d2,NONE)
        | (SOME t1',NONE) => (d2,SOME t1')
        | (NONE,SOME t2') => (d2,SOME t2')
        | (SOME t1',SOME t2') => (d2,SOME (op_t$t1'$t2'))
      end
    else tr d t
  | dfs_opr _ tr d t = tr d t;

  (* Replace single occurrence of (atomic) ot in t by nt.
    Returns new term or NONE if nothing was removed. *)
  fun dfs_replace_atomic opN ot nt t = let
    fun tr d t = if not d andalso t=ot then (true,SOME nt) else (d,SOME t);
    val (success,SOME t') = dfs_opr opN tr false t;
  in
    if success then SOME t' else NONE
  end;

  fun assn_simproc_fun ctxt credex = let
    val ([redex],ctxt') = Variable.import_terms true [Thm.term_of credex] ctxt;
    (*val _ = tracing (tr_term redex);*)
    val export = singleton (Variable.export ctxt' ctxt)

    fun mk_star t1 t2 = @{term "(*)::assn \<Rightarrow> _ \<Rightarrow> _"}$t2$t1;

    fun mk_star' NONE NONE = NONE
    | mk_star' (SOME t1) NONE  = SOME t1
    | mk_star' NONE (SOME t2) = SOME t2
    | mk_star' (SOME t1) (SOME t2) = SOME (mk_star t1 t2);

    fun ptrs_key (_$k$_) = k;

    fun remove_term pt t = case
      dfs_replace_atomic @{const_name "Groups.times_class.times"} pt
        @{term emp} t
    of
      SOME t' => t';

    fun normalize t = let

      fun ep_tr (has_true,ps,ptrs) t = case t of
        Const (@{const_name "Assertions.pure_assn"},_)$_
        => ((has_true,t::ps,ptrs),NONE)
      | Const (@{const_name "Assertions.sngr_assn"},_)$_$_
        => ((has_true,ps,t::ptrs),SOME t)
      | Const (@{const_name "Assertions.snga_assn"},_)$_$_
        => ((has_true,ps,t::ptrs),SOME t)
      | Const (@{const_name "Orderings.top_class.top"},_)
        => ((true,ps,ptrs),NONE)
      | (inf_op as Const (@{const_name "Lattices.inf_class.inf"},_))$t1$t2
        => ((has_true,ps,ptrs),SOME (inf_op$normalize t1$normalize t2))
      | _ => ((has_true,ps,ptrs),SOME t);

      fun normalizer t = case dfs_opr @{const_name "Groups.times_class.times"}
        ep_tr (false,[],[]) t
      of
        ((has_true,ps,ptrs),rt) => ((has_true,rev ps,ptrs),rt);

      fun normalize_core t = let
        val ((has_true,pures,ptrs),rt) = normalizer t;
        val similar = find_similar ptrs_key ptrs;
        val true_t = if has_true then SOME @{term "Assertions.top_assn"}
          else NONE;
        val pures' = case pures of
            [] => NONE
          | p::ps => SOME (fold mk_star ps p);
      in
        case similar of NONE => the (mk_star' pures' (mk_star' true_t rt))
        | SOME (t1,t2) => let
            val t_stripped = remove_term t1 (remove_term t2 t);
          in mk_star t_stripped (mk_star t1 t2) end
      end;

      fun skip_ex ((exq as Const (@{const_name "ex_assn"},_))$(Abs (n,ty,t))) =
        exq$Abs (n,ty,skip_ex t)
      | skip_ex t = normalize_core t;

      val (bs,t') = strip_abs t;
      val ty = fastype_of1 (map #2 bs,t');
    in
      if ty = @{typ assn} then
        Logic.rlist_abs (bs,skip_ex t')
      else t
    end;

    (*val _ = tracing (tr_term redex);*)
    val (f,terms) = strip_comb redex;
    val nterms = map (fn t => let
        (*val _ = tracing (tr_term t); *)
        val t'=normalize t;
        (*val _ = tracing (tr_term t');*)
      in t' end) terms;
    val new_form = list_comb (f,nterms);

    val res_ss = (put_simpset HOL_basic_ss ctxt addsimps @{thms star_aci});
    val result = Option.map (export o mk_meta_eq) (Arith_Data.prove_conv_nohyps
      [simp_tac res_ss 1] ctxt' (redex,new_form)
    );

  in
    result
  end handle exc =>
    if Exn.is_interrupt exc then Exn.reraise exc
    else
      (tracing ("assn_simproc failed with exception\n:" ^ Runtime.exn_message exc);
        NONE) (* Fail silently *);

  val assn_simproc =
    Simplifier.make_simproc @{context} "assn_simproc"
     {lhss =
      [@{term "h \<Turnstile> P"},
       @{term "P \<Longrightarrow>\<^sub>A Q"},
       @{term "P \<Longrightarrow>\<^sub>t Q"},
       @{term "Hoare_Triple.hoare_triple P c Q"},
       @{term "(P::assn) = Q"}],
      proc = K assn_simproc_fun};

  (***********************************)
  (*     Default Simplifications     *)
  (***********************************)

  (* Default simplification. MUST contain assertion normalization!
    Tactic must not fail! *)
  fun dflt_tac ctxt = asm_full_simp_tac
    (put_simpset HOL_ss ctxt
      addsimprocs [assn_simproc]
      addsimps @{thms norm_assertion_simps}
      addsimps (Named_Theorems.get ctxt @{named_theorems sep_dflt_simps})
      |> fold Splitter.del_split @{thms if_split}
    );

  (***********************************)
  (*         Frame Matcher           *)
  (***********************************)

  (* Do frame matching
    imp_solve_tac - tactic used to discharge first assumption of match-rule
      cf. lemma FI_match.
  *)
  fun match_frame_tac imp_solve_tac ctxt = let
    (* Normalize star-lists *)
    val norm_tac = simp_tac (
      put_simpset HOL_basic_ss ctxt addsimps @{thms SLN_normalize});

    (* Strip star-lists *)
    val strip_tac =
      simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms SLN_strip}) THEN'
      simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms SLN_def});

    (* Do a match step *)
    val match_tac = resolve_tac ctxt @{thms FI_match} (* Separate p,q*)
      THEN' SOLVED' imp_solve_tac (* Solve implication *)
      THEN' norm_tac;

    (* Do a no-match step *)
    val nomatch_tac = resolve_tac ctxt @{thms FI_p_nomatch} ORELSE'
      (resolve_tac ctxt @{thms FI_q_nomatch} THEN' norm_tac);
  in
    resolve_tac ctxt @{thms FI_init} THEN' norm_tac
    THEN' REPEAT_DETERM' (FIRST' [
      CHANGED o dflt_tac ctxt,
      (match_tac ORELSE' nomatch_tac)])
    THEN' resolve_tac ctxt @{thms FI_finalize} THEN' strip_tac
  end;

  (***********************************)
  (*         Frame Inference         *)
  (***********************************)

  fun frame_inference_tac ctxt =
    resolve_tac ctxt @{thms frame_inference_init}
    THEN' match_frame_tac (resolve_tac ctxt @{thms ent_refl}) ctxt
    THEN' resolve_tac ctxt @{thms frame_inference_finalize};

  (***********************************)
  (*       Entailment Solver         *)
  (***********************************)

  (* Extract existential quantifiers from entailment goal *)
  fun extract_ex_tac ctxt i st = let
    fun count_ex (Const (@{const_name Assertions.entails},_)$_$c) =
      count_ex c RS @{thm HOL.mp}
    | count_ex (Const (@{const_name Assertions.ex_assn},_)$Abs (_,_,t))
      = count_ex t RS @{thm enorm_exI'}
    | count_ex _ = @{thm imp_refl};

    val concl = Logic.concl_of_goal (Thm.prop_of st) i |> HOLogic.dest_Trueprop;
    val thm = count_ex concl;
  in
    (TRY o REPEAT_ALL_NEW (match_tac ctxt @{thms ent_ex_preI}) THEN'
     resolve_tac ctxt [thm]) i st
  end;

  (* Solve Entailment *)
  fun solve_entails_tac ctxt = let
    val preprocess_entails_tac =
      dflt_tac ctxt
      THEN' extract_ex_tac ctxt
      THEN' simp_tac
        (put_simpset HOL_ss ctxt addsimps @{thms solve_ent_preprocess_simps});

    val match_entails_tac =
      resolve_tac ctxt @{thms entails_solve_init}
      THEN' match_frame_tac (resolve_tac ctxt @{thms ent_refl}) ctxt
      THEN' resolve_tac ctxt @{thms entails_solve_finalize};
  in
    preprocess_entails_tac
    THEN' (TRY o
      REPEAT_ALL_NEW (match_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems sep_eintros}))))
    THEN_ALL_NEW (dflt_tac ctxt THEN'
      TRY o (match_tac ctxt @{thms ent_triv}
        ORELSE' resolve_tac ctxt @{thms ent_refl}
        ORELSE' match_entails_tac))
  end;

  (***********************************)
  (* Verification Condition Generator*)
  (***********************************)

  fun heap_rule_tac ctxt h_thms =
    resolve_tac ctxt h_thms ORELSE' (
    resolve_tac ctxt @{thms fi_rule} THEN' (resolve_tac ctxt h_thms THEN_IGNORE_NEWGOALS
    frame_inference_tac ctxt));

  fun vcg_step_tac ctxt = let
    val h_thms = rev (Named_Theorems.get ctxt @{named_theorems sep_heap_rules});
    val d_thms = rev (Named_Theorems.get ctxt @{named_theorems sep_decon_rules});
    val heap_rule_tac = heap_rule_tac ctxt h_thms

    (* Apply consequence rule if postcondition is not a schematic var *)
    fun app_post_cons_tac i st =
      case Logic.concl_of_goal (Thm.prop_of st) i |> HOLogic.dest_Trueprop of
        Const (@{const_name Hoare_Triple.hoare_triple},_)$_$_$qt =>
          if is_Var (head_of qt) then no_tac st
          else resolve_tac ctxt @{thms cons_post_rule} i st
      | _ => no_tac st;

  in
    CSUBGOAL (snd #> (FIRST' [
      CHANGED o dflt_tac ctxt,
      REPEAT_ALL_NEW (resolve_tac ctxt @{thms normalize_rules}),
      CHANGED o (FIRST' [resolve_tac ctxt d_thms, heap_rule_tac]
        ORELSE' (app_post_cons_tac THEN'
          FIRST' [resolve_tac ctxt d_thms, heap_rule_tac]))
    ]))
  end;

  fun vcg_tac ctxt = REPEAT_DETERM' (vcg_step_tac ctxt)

  (***********************************)
  (*        Automatic Solver         *)
  (***********************************)

  fun sep_autosolve_tac do_pre do_post ctxt = let
    val pre_tacs = [
      CHANGED o clarsimp_tac ctxt,
      CHANGED o REPEAT_ALL_NEW (match_tac ctxt @{thms ballI allI impI conjI})
    ];
    val main_tacs = [
      match_tac ctxt @{thms is_hoare_triple} THEN' CHANGED o vcg_tac ctxt,
      match_tac ctxt @{thms is_entails} THEN' CHANGED o solve_entails_tac ctxt
    ];
    val post_tacs = [SELECT_GOAL (auto_tac ctxt)];
    val tacs = (if do_pre then pre_tacs else [])
      @ main_tacs
      @ (if do_post then post_tacs else []);
  in
    REPEAT_DETERM' (CHANGED o FIRST' tacs)
  end;

  (***********************************)
  (*          Method Setup           *)
  (***********************************)

  val dflt_simps_modifiers = [
    Args.$$$ "dflt_simps" -- Scan.option Args.add -- Args.colon
      >> K (Method.modifier (Named_Theorems.add @{named_theorems sep_dflt_simps}) \<^here>),
    Args.$$$ "dflt_simps" -- Scan.option Args.del -- Args.colon
      >> K (Method.modifier (Named_Theorems.del @{named_theorems sep_dflt_simps}) \<^here>)
  ];
  val heap_modifiers = [
    Args.$$$ "heap" -- Scan.option Args.add -- Args.colon
      >> K (Method.modifier (Named_Theorems.add @{named_theorems sep_heap_rules}) \<^here>),
    Args.$$$ "heap" -- Scan.option Args.del -- Args.colon
      >> K (Method.modifier (Named_Theorems.del @{named_theorems sep_heap_rules}) \<^here>)
  ];
  val decon_modifiers = [
    Args.$$$ "decon" -- Scan.option Args.add -- Args.colon
      >> K (Method.modifier (Named_Theorems.add @{named_theorems sep_decon_rules}) \<^here>),
    Args.$$$ "decon" -- Scan.option Args.del -- Args.colon
      >> K (Method.modifier (Named_Theorems.del @{named_theorems sep_decon_rules}) \<^here>)
  ];

  val eintros_modifiers = [
    Args.$$$ "eintros" -- Scan.option Args.add -- Args.colon
      >> K (Method.modifier (Named_Theorems.add @{named_theorems sep_eintros}) \<^here>),
    Args.$$$ "eintros" -- Scan.option Args.del -- Args.colon
      >> K (Method.modifier (Named_Theorems.del @{named_theorems sep_eintros}) \<^here>)
  ];

  val solve_entails_modifiers = dflt_simps_modifiers @ eintros_modifiers;

  val vcg_modifiers =
    heap_modifiers @ decon_modifiers @ dflt_simps_modifiers;

  val sep_auto_modifiers =
    clasimp_modifiers @ vcg_modifiers @ eintros_modifiers;

end;
\<close>

simproc_setup assn_simproc
  ("h\<Turnstile>P" | "P\<Longrightarrow>\<^sub>AQ" | "P\<Longrightarrow>\<^sub>tQ" | "<P> c <R>" | "(P::assn) = Q")
  = \<open>K Seplogic_Auto.assn_simproc_fun\<close>

method_setup assn_simp =\<open>Scan.succeed (fn ctxt => (SIMPLE_METHOD' (
  CHANGED o Seplogic_Auto.dflt_tac ctxt
)))\<close> "Seplogic: Simplification of assertions"

method_setup frame_inference = \<open>Scan.succeed (fn ctxt => (SIMPLE_METHOD' (
  CHANGED o Seplogic_Auto.frame_inference_tac ctxt
)))\<close> "Seplogic: Frame inference"

method_setup solve_entails = \<open>
  Method.sections Seplogic_Auto.solve_entails_modifiers >>
  (fn _ => fn ctxt => SIMPLE_METHOD' (
  CHANGED o Seplogic_Auto.solve_entails_tac ctxt
))\<close> "Seplogic: Entailment Solver"

method_setup heap_rule = \<open>
  Attrib.thms >>
  (fn thms => fn ctxt => SIMPLE_METHOD' (
    let
      val thms = case thms of [] => rev (Named_Theorems.get ctxt @{named_theorems sep_heap_rules})
        | _ => thms
    in
      CHANGED o Seplogic_Auto.heap_rule_tac ctxt thms
    end
))\<close> "Seplogic: Apply rule with frame inference"

method_setup vcg = \<open>
  Scan.lift (Args.mode "ss") --
  Method.sections Seplogic_Auto.vcg_modifiers >>
  (fn (ss,_) => fn ctxt => SIMPLE_METHOD' (
  CHANGED o (
    if ss then Seplogic_Auto.vcg_step_tac ctxt
    else Seplogic_Auto.vcg_tac ctxt
  )
))\<close> "Seplogic: Verification Condition Generator"

method_setup sep_auto =
  \<open>Scan.lift (Args.mode "nopre" -- Args.mode "nopost" -- Args.mode "plain")
      --| Method.sections Seplogic_Auto.sep_auto_modifiers >>
  (fn ((nopre,nopost),plain) => fn ctxt => SIMPLE_METHOD' (
    CHANGED o Seplogic_Auto.sep_autosolve_tac
      ((not nopre) andalso (not plain))
      ((not nopost) andalso (not plain)) ctxt
  ))\<close> "Seplogic: Automatic solver"

lemmas [sep_dflt_simps] = split

declare deconstruct_rules[sep_decon_rules]
declare heap_rules[sep_heap_rules]

lemmas [sep_eintros] = impI conjI exI

subsection \<open>Semi-Automatic Reasoning\<close>
text \<open>In this section, we provide some lemmas for semi-automatic reasoning\<close>

text \<open>Forward reasoning with frame. Use \<open>frame_inference\<close>-method
  to discharge second assumption.\<close>
lemma ent_frame_fwd:
  assumes R: "P \<Longrightarrow>\<^sub>A R"
  assumes F: "Ps \<Longrightarrow>\<^sub>A P*F"
  assumes I: "R*F \<Longrightarrow>\<^sub>A Q"
  shows "Ps \<Longrightarrow>\<^sub>A Q"
  using assms
  by (metis ent_refl ent_star_mono ent_trans)

lemma mod_frame_fwd:
  assumes M: "h\<Turnstile>Ps"
  assumes R: "P\<Longrightarrow>\<^sub>AR"
  assumes F: "Ps \<Longrightarrow>\<^sub>A P*F"
  shows "h\<Turnstile>R*F"
  using assms
  by (metis ent_star_mono entails_def)

text \<open>Apply precision rule with frame inference.\<close>
lemma prec_frame:
  assumes PREC: "precise P"
  assumes M1: "h\<Turnstile>(R1 \<and>\<^sub>A R2)"
  assumes F1: "R1 \<Longrightarrow>\<^sub>A P x p * F1"
  assumes F2: "R2 \<Longrightarrow>\<^sub>A P y p * F2"
  shows "x=y"
  using preciseD[OF PREC] M1 F1 F2
  by (metis entailsD mod_and_dist)

lemma prec_frame_expl:
  assumes PREC: "\<forall>x y. (h\<Turnstile>(P x * F1) \<and>\<^sub>A (P y * F2)) \<longrightarrow> x=y"
  assumes M1: "h\<Turnstile>(R1 \<and>\<^sub>A R2)"
  assumes F1: "R1 \<Longrightarrow>\<^sub>A P x * F1"
  assumes F2: "R2 \<Longrightarrow>\<^sub>A P y * F2"
  shows "x=y"
  using assms
  by (metis entailsD mod_and_dist)

text \<open>Variant that is useful within induction proofs, where induction
  goes over \<open>x\<close> or \<open>y\<close>\<close>
lemma prec_frame':
  assumes PREC: "(h\<Turnstile>(P x * F1) \<and>\<^sub>A (P y * F2)) \<longrightarrow> x=y"
  assumes M1: "h\<Turnstile>(R1 \<and>\<^sub>A R2)"
  assumes F1: "R1 \<Longrightarrow>\<^sub>A P x * F1"
  assumes F2: "R2 \<Longrightarrow>\<^sub>A P y * F2"
  shows "x=y"
  using assms
  by (metis entailsD mod_and_dist)

lemma ent_wand_frameI:
  assumes "(Q -* R) * F \<Longrightarrow>\<^sub>A S"
  assumes "P \<Longrightarrow>\<^sub>A F * X"
  assumes "Q*X \<Longrightarrow>\<^sub>A R"
  shows "P \<Longrightarrow>\<^sub>A S"
  using assms
  by (metis ent_frame_fwd ent_wandI mult.commute)

subsubsection \<open>Manual Frame Inference\<close>

lemma ent_true_drop:
  "P\<Longrightarrow>\<^sub>AQ*true \<Longrightarrow> P*R\<Longrightarrow>\<^sub>AQ*true"
  "P\<Longrightarrow>\<^sub>AQ \<Longrightarrow> P\<Longrightarrow>\<^sub>AQ*true"
  apply (metis assn_times_comm ent_star_mono ent_true merge_true_star_ctx)
  apply (metis assn_one_left ent_star_mono ent_true star_aci(2))
  done

lemma fr_refl: "A\<Longrightarrow>\<^sub>AB \<Longrightarrow> A*C \<Longrightarrow>\<^sub>AB*C"
  by (blast intro: ent_star_mono ent_refl)

lemma fr_rot: "(A*B \<Longrightarrow>\<^sub>A C) \<Longrightarrow> (B*A \<Longrightarrow>\<^sub>A C)"
  by (simp add: assn_aci)

lemma fr_rot_rhs: "(A \<Longrightarrow>\<^sub>A B*C) \<Longrightarrow> (A \<Longrightarrow>\<^sub>A C*B)"
  by (simp add: assn_aci)

lemma ent_star_mono_true:
  assumes "A \<Longrightarrow>\<^sub>A A' * true"
  assumes "B \<Longrightarrow>\<^sub>A B' * true"
  shows "A*B*true \<Longrightarrow>\<^sub>A A'*B'*true"
  using ent_star_mono[OF assms] apply simp
  using ent_true_drop(1) by blast

lemma ent_refl_true: "A \<Longrightarrow>\<^sub>A A * true"
  by (simp add: ent_true_drop(2))

lemma entt_fr_refl: "F\<Longrightarrow>\<^sub>tF' \<Longrightarrow> F*A \<Longrightarrow>\<^sub>t F'*A" by (rule entt_star_mono) auto
lemma entt_fr_drop: "F\<Longrightarrow>\<^sub>tF' \<Longrightarrow> F*A \<Longrightarrow>\<^sub>t F'"
  using ent_true_drop(1) enttD enttI by blast

method_setup fr_rot = \<open>
  let
    fun rot_tac ctxt =
      resolve_tac ctxt @{thms fr_rot} THEN'
      simp_tac (put_simpset HOL_basic_ss ctxt
        addsimps @{thms star_assoc[symmetric]})

  in
    Scan.lift Parse.nat >>
      (fn n => fn ctxt => SIMPLE_METHOD' (
        fn i => REPEAT_DETERM_N n (rot_tac ctxt i)))

  end
\<close>

method_setup fr_rot_rhs = \<open>
  let
    fun rot_tac ctxt =
      resolve_tac ctxt @{thms fr_rot_rhs} THEN'
      simp_tac (put_simpset HOL_basic_ss ctxt
        addsimps @{thms star_assoc[symmetric]})

  in
    Scan.lift Parse.nat >>
      (fn n => fn ctxt => SIMPLE_METHOD' (
        fn i => REPEAT_DETERM_N n (rot_tac ctxt i)))

  end
\<close>

(*<*)
subsection \<open>Test Cases\<close>

lemma "\<And>x. A x * true * Q x \<Longrightarrow>\<^sub>A true * A x * Q x"
  apply simp
  done

lemma "A * (true * B) \<Longrightarrow>\<^sub>A true * A * B"
  apply (simp)
  done

lemma "h\<Turnstile>true*P*true \<longleftrightarrow> h\<Turnstile>P*true"
  by simp

lemma "A * true * \<up>(b \<and> c) * true * B \<Longrightarrow>\<^sub>A \<up>b * \<up>c * true *A * B"
  by simp

lemma "\<exists>y c. \<exists>\<^sub>Ax. P x * (R x * Q y) * \<up> (b \<and> c) \<Longrightarrow>\<^sub>A (\<exists>\<^sub>Ax. \<up>b * (P x * (R x * Q y) * \<up>c))"
  apply simp
  done

lemma "A * B * (\<up>c * B * C * D * \<up>a * true * \<up>d) * (\<exists>\<^sub>Ax. E x * F * \<up>b) * true \<Longrightarrow>\<^sub>A (\<exists>\<^sub>Ax. \<up> (c \<and> a \<and> d \<and> b) *
          true * A * B * (true * B * C * D) * (E x * F))"
  apply simp
  done

lemma "<P> c <\<lambda>r. Q r * true * \<up>(b r) * true * \<up>a>
  \<longleftrightarrow> <P> c <\<lambda>r. Q r * true * \<up>(b r \<and> a)>"
  apply simp
  done

lemma "(h\<Turnstile>((A*B*\<up>b*true*\<up>c*true) \<and>\<^sub>A (\<up>(p=q)*P*Q)))
  \<longleftrightarrow> h \<Turnstile> A * B * true \<and>\<^sub>A P * Q \<and> b \<and> c \<and> p = q"
  apply simp
  done

lemma assumes "FI_RESULT [(B, B), (A, A)] C D F"
  shows "FI_QUERY (A*B*C) (D*B*A) F"
  apply (tactic \<open>Seplogic_Auto.match_frame_tac
    (resolve_tac @{context} @{thms ent_refl}) @{context} 1\<close>)
  by (rule assms)

lemma
  assumes "FI_RESULT [(B,B), (A,A)] C emp F"
  shows "FI_QUERY (A*B*C) (B*A) F"
  apply (tactic \<open>Seplogic_Auto.match_frame_tac
    (resolve_tac @{context} @{thms ent_refl}) @{context} 1\<close>)
  by (rule assms)

lemma
  assumes "FI_RESULT [(B, B), (A, A)] emp emp F"
  shows "FI_QUERY (A*B) (B*A) F"
  apply (tactic \<open>Seplogic_Auto.match_frame_tac
    (resolve_tac @{context} @{thms ent_refl}) @{context} 1\<close>)
  by (rule assms)

lemma
  assumes "FI_RESULT [(A, A)] emp emp F"
  shows "FI_QUERY (A) (A) F"
  apply (tactic \<open>Seplogic_Auto.match_frame_tac
    (resolve_tac @{context} @{thms ent_refl}) @{context} 1\<close>)
  by (rule assms)

lemma
  assumes "FI_RESULT [(A, A)] (B * C * D) emp F"
  shows "FI_QUERY (B*C*D*A) (A) F"
  apply (tactic \<open>Seplogic_Auto.match_frame_tac
    (resolve_tac @{context} @{thms ent_refl}) @{context} 1\<close>)
  by (rule assms)

schematic_goal
  "P1 * P2 * P3 * P4 \<Longrightarrow>\<^sub>A P3 * ?R1"
  "P1 * (P2 * (P3 * P4)) \<Longrightarrow>\<^sub>A P1 * ?R2"
  "P4 * (P2 * (P1 * P3)) \<Longrightarrow>\<^sub>A P1 * ?R2'"
  "P1 * P2 * P3 * P4 \<Longrightarrow>\<^sub>A P4 * ?R3"
  "P1 * P2 \<Longrightarrow>\<^sub>A P1 * ?R4"
  "P1 * P2 \<Longrightarrow>\<^sub>A P2 * ?R5"
  "P1 \<Longrightarrow>\<^sub>A P1 * ?R6"
  "P1 * P2 \<Longrightarrow>\<^sub>A emp * ?R7"
  by frame_inference+

lemma "\<lbrakk>A; B; C; b 17\<rbrakk> \<Longrightarrow>
  Q 1 5 3 \<Longrightarrow>\<^sub>A (\<exists>\<^sub>Ax y z. \<exists>\<^sub>Aa. Q x y z * \<up>(b a) * \<up>(y=5))"
  by solve_entails

thm nth_rule
lemma "<P * x\<mapsto>\<^sub>a[1,2,3]>
  do { v\<leftarrow>Array.nth x 1; return v }
  <\<lambda>r. P * x\<mapsto>\<^sub>a[1,2,3] * \<up>(r=2)>"
  apply sep_auto
  done

(*>*)

subsection \<open>Quick Overview of Proof Methods\<close>
  text_raw \<open>\label{sec:auto:overview}\<close>
text \<open>
  In this section, we give a quick overview of the available proof methods
  and options. The most versatile proof method that we provide is
  \<open>sep_auto\<close>. It tries to solve the first subgoal, invoking appropriate
  proof methods as required. If it cannot solve the subgoal completely, it
  stops at the intermediate state that it could not handle any more.

  \<open>sep_auto\<close> can be configured by
  section-arguments for the simplifier, the classical reasoner, and all
  section-arguments for the verification condition generator and
  entailment solver. Moreover, it takes an optional mode argument (mode), where
  valid modes are:
  \begin{description}
    \item[(nopre)] No preprocessing of goal. The preprocessor tries to clarify
      and simplify the goal before the main method is invoked.
    \item[(nopost)] No postprocessing of goal. The postprocessor tries to
      solve or simplify goals left over by verification condition generation or
      entailment solving.
    \item[(plain)] Neither pre- nor postprocessing. Just applies vcg and
      entailment solver.
  \end{description}

  \paragraph{Entailment Solver.} The entailment solver processes goals of the
  form \<open>P \<Longrightarrow>\<^sub>A Q\<close>. It is invoked by the method \<open>solve_entails\<close>.
  It first tries to pull out pure parts of
  \<open>P\<close> and \<open>Q\<close>. This may introduce quantifiers, conjunction,
  and implication into the goal, that are eliminated by resolving with rules
  declared as \<open>sep_eintros\<close> (method argument: eintros[add/del]:).
  Moreover, it simplifies with rules declared as \<open>sep_dflt_simps\<close>
  (section argument: \<open>dflt_simps[add/del]:\<close>).

  Now, \<open>P\<close> and \<open>Q\<close> should have the form \<open>X\<^sub>1*\<dots>*X\<^sub>n\<close>.
  Then, the frame-matcher is used to match all items of \<open>P\<close> with items
  of \<open>Q\<close>, and thus solve the implication. Matching is currently done
  syntactically, but can instantiate schematic variables.

  Note that, by default, existential introduction is declared as
  \<open>sep_eintros\<close>-rule. This introduces schematic variables, that can
  later be matched against. However, in some cases, the matching may instantiate
  the schematic variables in an undesired way. In this case, the argument
  \<open>eintros del: exI\<close> should be passed to the entailment solver, and
  the existential quantifier should be instantiated manually.

  \paragraph{Frame Inference}
  The method \<open>frame_inference\<close> tries to solve a goal of the
  form \<open>P\<Longrightarrow>Q*?F\<close>, by matching \<open>Q\<close> against the parts of
  \<open>P\<close>, and instantiating \<open>?F\<close> accordingly.
  Matching is done syntactically, possibly
  instantiating schematic variables. \<open>P\<close> and \<open>Q\<close> should be
  assertions separated by \<open>*\<close>. Note that frame inference does no
  simplification or other kinds of normalization.

  The method \<open>heap_rule\<close> applies the specified heap rules, using
  frame inference if necessary. If no rules are specified, the default
  heap rules are used.

  \paragraph{Verification Condition Generator}
  The verification condition generator processes goals of the form
  \<open><P>c<Q>\<close>. It is invoked by the method \<open>vcg\<close>.
  First, it tries to pull out pure parts and simplifies with
  the default simplification rules. Then, it tries to resolve the goal with
  deconstruct rules (attribute: \<open>sep_decon_rules\<close>,
  section argument: \<open>decon[add/del]:\<close>), and if this does not succeed,
  it tries
  to resolve the goal with heap rules (attribute: \<open>sep_heap_rules\<close>,
  section argument: \<open>heap[add/del]:\<close>), using the frame rule and
  frame inference.
  If resolving is not possible, it also tries to apply the consequence rule to
  make the postcondition a schematic variable.
\<close>

(*<*)
subsection \<open>Hiding of internal stuff\<close>
hide_const (open) FI SLN
(*>*)

end

subset_name: curated


TITLE: Minimal polynomial has coefficients in the valuation ring?
QUESTION [1 upvotes]: Question
Let $K$ be a complete nonarchimedean valued field with valuation ring $\mathcal{O}$ and let $L/K$ be a finite extension.
Let $\alpha$ be an element of $L$ and $f\in K[x]$ its minimal polynomial.
Is is true that $f\in\mathcal{O}[x]$?
Comments
First of all, I am asking this, because of a proof I saw, where the author said "...let $f$ be the minimal polynomial of $\alpha$ and let $\overline{f}=f\pmod{\kappa}$, where $\kappa$ is the residue field of $K$."
He is implicitly using the fact that he can send the coefficients of $f$ to the residue field, and we can only do that if the coefficientes are in $\mathcal{O}$.
I strongly suspect that this is not true in general. I know that if $f$ is monic and the independent term is in $\mathcal{O}$ then indeed $f\in\mathcal{O}[x]$, but only with the information that $f$ is the minimal of some element, I cannot deduce that.
I think that the author meant the following:
"Take the minimal polynomial $f$, clean denominators, and now you can send it to $\kappa[x]$, even though $f$ is not monic anymore".
Is this correct?
If so, after sending $f$ to $\kappa[x]$, it feels like we could perfectly make it monic again, right?
Sorry if this question is kind of annoying or obvious, but Neukirch's style is yet kind of hard for me, making a lot of implicit assumptions and I want to understand things correctly.
Thank you in advance for explanations.

REPLY [0 votes]: Another answer since I didn't understand your original question properly: the result I gave is pretty general.  Let me state it clearly:

Let $A$ be an integrally closed integral domain with quotient field $K$, $L$ a finite separable extension of $K$, and $B$ the integral closure of $A$ in $L$.  Let $\alpha \in L$ and let $f \in K[X]$ be its minimal polynomial over $K$ (assumed to be monic).  Then $\alpha \in B$ if and only if $f \in A[X]$.

I gave the result for the ring of integers of a number field, the proof is the same in general.  If $S$ is a multiplicatively closed subset of $A$, then $S^{-1}B$ is the integral closure of $S^{-1}A$ in $L$, and the same result holds with $B$ replaced by $S^{-1}B$ and $A$ replaced by $S^{-1}A$.  So e.g. if $\mathfrak p$ is a prime of $\mathcal O_K$, and $S = \mathcal O_K \setminus \mathfrak p$, then $S^{-1} \mathcal O_L$ is the integral closure of $\mathcal O_{K, \mathfrak p}$ in $L$.  But $S^{-1} \mathcal O_L$ isn't the valuation ring of valuation of $L$, unless there is only one prime $\mathfrak P$ of $\mathcal O_L$ lying over $\mathfrak p$, in which case $S^{-1} \mathcal O_L = \mathcal O_{L, \mathfrak P}$ (otherwise you just have $\subseteq$).
In general, if $A$ is a Dedekind domain (in particular $A$ is integrally closed so the result holds), and $S = A \setminus \mathfrak p$ for a prime $\mathfrak p$ of $A$, then $S^{-1}B$ is a principal ideal domain with finitely many prime ideals $S^{-1}\mathfrak P_1, ... , S^{-1} \mathfrak P_g$, where $\mathfrak P_1, ... , \mathfrak P_g$ are all the primes of $B$ lying over $\mathfrak p$.
In your case, the fact that $K$ is complete with respect to its valuation means that there is only one prime $w$ lying over $v$, so the integral closure of $\mathcal O$ in $L$ is exactly the valuation ring of $w$.


TITLE: Find the zeros of $f(z)=z^3-\sin^3z$
QUESTION [4 upvotes]: I want to find the zeros of $f(z)$, $$f(z)=z^3-\sin^3z$$
My attempt
$f(z)=0$
$z^3-(z-z^3/3!+z^5/5!-\dots)^3=0$
$z^3-z^3(1-z^2/3!+z^4/5!-\dots)^3=0$
$z^3[1-(1-z^2/3!+z^4/5!-\dots)^3]=0$
So $z=0$ is a zero of order $3$.
I don't feel good about this answer. Please give me some hints if I am incorrect.
Edit: What is the order of root $z=0$?

REPLY [2 votes]: Interesting problem. I'm considering a couple of approaches.
We have $f(z)=z^3-sin^3(z)$ and wish to find the roots, or equivalently solutions of $z^3=sin^3(z)$ which gives $$z^3/sin^3(z)=1$$
So roots occur where $z/sin(z)$= cubic roots of unity:$\{1, e^{2\pi i/3}, e^{4\pi i/3}\}$.
Or consider $z^3-sin^3{z}=0=(z-\sin{z})(z^2+z\sin{z}+\sin^2z)$
Applying the quadratic formula to the second term in parentheses gives $$z=\frac{-\sin{z}+\sqrt{\sin^2{z}-4\sin^2{z}}}{2}=(\sin z)(\frac{-1}{2}+\frac{i\sqrt{3}}{2})$$
Again we get that $\frac{z}{\sin{z}}$=1 or the other two roots of unity.
For each root of unity, use your Taylor Series representation of Sine to get the Taylor series of $\frac{\sin{z}}{z}$ to the quadratic term, set this equal to the successive roots of unity. This should get you close approximations to  several solutions.


TITLE: Estimate the sample deviation in one pass
QUESTION [3 upvotes]: We've learned this algorithm in class but I'm not sure I've fully understood the correctness of this approach.
It is known as Welford's algorithm for the sum of squares, as described in: Welford, B.P., "Note on a Method for Calculating Corrected Sums of Squares and Products", Technometrics, Vol. 4, No. 3 (Aug., 1962), pp. 419-420
The two-pass algorithm to estimate the sample deviation is simple. We first estimate the mean by one pass and then calculate the standard deviation. In short, it is $s_n^2 = \frac{1}{n-1} \sum_{i=1}^n (Y_i - \hat{Y})^2$.
The one-pass approach has three steps.
1) $v_1 = 0$
2) $v_k = v_{k-1} + \frac{1}{k(k-1)} (\sum_{i=1}^{k-1} Y_i - (k-1) Y_k)^2 (2 \leq k \leq n)$
3) $s_n^2 = \frac{v_n}{n-1}$.
Can someone help me understand how this approach works?

REPLY [4 votes]: $v_n$ is going to be $\sum_{i=1}^n (Y_i - \overline{Y}_n)^2$ where $\overline{Y}_n = \frac{1}{n} \sum_{i=1}^n Y_i$.  Note that by expanding out the square,
$v_n = \sum_{i=1}^n Y_i^2 - \frac{1}{n} \left(\sum_{i=1}^n Y_i\right)^2$.
In terms of $m_k = \sum_{i=1}^k Y_i$, we have
$$v_n = \sum_{i=1}^n Y_i^2 - \frac{1}{n} m_n^2 = \sum_{i=1}^{n-1} Y_i^2 + Y_n^2 - \frac{1}{n} (m_{n-1} + Y_n)^2$$
On the other hand,
$$v_{n-1} = \sum_{i=1}^{n-1} Y_i^2 - \frac{1}{n-1} m_{n-1}^2$$
Since $(m_{n-1} + Y_n)^2 = m_{n-1}^2 + 2 Y_n m_{n-1} + Y_n^2$, the difference between these is
$$ v_n - v_{n-1} = \left(1 - \frac{1}{n}\right) Y_n^2 + \left(\frac{1}{n-1} - \frac{1}{n}\right) m_{n-1}^2 - \frac{2}{n} Y_n m_{n-1} $$
$$ =  \frac{1}{n(n-1)} m_{n-1}^2 - \frac{2}{n} Y_n m_{n-1} +\frac{n-1}{n} Y_n^2 $$
$$ = \frac{1}{n(n-1)} \left(m_{n-1} - (n-1) Y_n\right)^2 $$


TITLE: Closure of the set in dictionary order topology.
QUESTION [0 upvotes]: Consider the ordered square $I_0^2$, the set $[0,1]\times [0,1]$  with the dictionary order topology. Let the general element of $I_0^2$ be denoted by $x\times y$, where $x, y\in [0,1]$. Then the closure of the subset $$S = \big\{x\times \frac{3}{4}: 0<a<x<b<1\big\}$$ in $I_0^2$ is

$S\cup \big((a, b]\times\{0\}\big) \cup \big([a, b)\times \{1\}\big)$
$S\cup \big((a, b]\times\{0\}\big) \cup \big((a, b]\times \{1\}\big)$
$S\cup \big((a, b)\times\{0\}\big) \cup \big((a, b)\times \{1\}\big)$
$S\cup \big((a, b]\times\{0\}\big)$

please explain it properly. I have no idea how to start with?

REPLY [2 votes]: Let $(p,0)$ be in $[0,1]^2$ in this order topology, where $0 < p$. A basic open neighbourhood of $(p,0)$ is an open interval with endpoints in $[0,1]^2$, say $\langle (l_1,l_2), (r_1,r_2)\rangle$. It follows by the definition of the lexicographic order that $l_1 < p$. A moment's thought reveals that we can in fact only need to consider basic open sets of the form $\langle (l_1,1), (p,r_2)\rangle$ for $(p,0)$ (with $0< l_1 < p, r_2 >0$), by shrinking such an open interval.
For a point $(q,1), q < 1$ we likewise only need to consider open basic sets of the form $\langle (q,l_1), (r_1,0)\rangle$ (with $l_1 > 0, q < r_1 < 1$).
It's then easy to see that a point $(p,0) \in \overline{S}$ iff $p \in (a,b]$ and $(q,1) \in \overline{S}$ iff $q \in [a,b)$.


text:
(*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
    License: BSD
*)

section \<open>Transfer Operator\<close>

theory Transfer_Operator
  imports Recurrence
begin

context qmpt begin

text \<open>The map $T$ acts on measures by push-forward. In particular, if $f d\mu$ is absolutely continuous
with respect to the reference measure $\mu$, then its push-forward $T_*(f d\mu)$ is absolutely
continuous with respect to $\mu$, and can therefore be written as $g d\mu$ for some function $g$.
The map $f \mapsto g$, representing the action of $T$ on the level of densities, is called the
transfer operator associated to $T$ and often denoted by $\hat T$.

We first define it on nonnegative functions, using Radon-Nikodym derivatives. Then, we extend it
to general real-valued functions by separating it into positive and negative parts.

The theory presents many similarities with the theory of conditional expectations. Indeed, it is
possible to make a theory encompassing the two. When the map is measure preserving,
there is also a direct relationship: $(\hat T f) \circ T$ is the conditional expectation of $f$
with respect to $T^{-1}B$ where $B$ is the sigma-algebra. Instead of building a general theory,
we copy the proofs for conditional expectations and adapt them where needed.\<close>

subsection \<open>The transfer operator on nonnegative functions\<close>

definition nn_transfer_operator :: "('a \<Rightarrow> ennreal) \<Rightarrow> ('a \<Rightarrow> ennreal)"
where
  "nn_transfer_operator f = (if f \<in> borel_measurable M then RN_deriv M (distr (density M f) M T)
                              else (\<lambda>_. 0))"

lemma borel_measurable_nn_transfer_operator [measurable]:
  "nn_transfer_operator f \<in> borel_measurable M"
unfolding nn_transfer_operator_def by auto

lemma borel_measurable_nn_transfer_operator_iterates [measurable]:
  assumes [measurable]: "f \<in> borel_measurable M"
  shows "(nn_transfer_operator^^n) f \<in> borel_measurable M"
by (cases n, auto)

text \<open>The next lemma is arguably the most fundamental property of the transfer operator: it is the
adjoint of the composition by $T$. If one defined it as an abstract adjoint, it would be defined
on the dual of $L^\infty$, which is a large unwieldy space. The point is that it can be defined
on genuine functions, using the push-forward point of view above. However, once we have this
property, we can forget completely about the definition, since this property characterizes
the transfer operator, as the second lemma below shows.
From this point on, we will only work with it, and forget completely about
the definition using Radon-Nikodym derivatives.
\<close>

lemma nn_transfer_operator_intg:
  assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  shows "(\<integral>\<^sup>+ x. f x * nn_transfer_operator g x \<partial>M) = (\<integral>\<^sup>+ x. f (T x) * g x \<partial>M)"
proof -
  have *: "density M (RN_deriv M (distr (density M g) M T)) = distr (density M g) M T"
    by (rule density_RN_deriv) (auto intro!: quasi_measure_preserving_absolutely_continuous simp add: Tqm)
  have "(\<integral>\<^sup>+ x. f x * nn_transfer_operator g x \<partial>M) = (\<integral>\<^sup>+ x. f x \<partial>(density M (RN_deriv M (distr (density M g) M T))))"
    unfolding nn_transfer_operator_def by (simp add: nn_integral_densityR)
  also have "... = (\<integral>\<^sup>+ x. f x \<partial>(distr (density M g) M T))"
    unfolding * by simp
  also have "... = (\<integral>\<^sup>+ x. f (T x) \<partial>(density M g))"
    by (rule nn_integral_distr, auto)
  also have "... = (\<integral>\<^sup>+ x. f (T x) * g x \<partial>M)"
    by (simp add: nn_integral_densityR)
  finally show ?thesis by auto
qed

lemma nn_transfer_operator_intTn_g:
  assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  shows "(\<integral>\<^sup>+ x. f x * (nn_transfer_operator^^n) g x \<partial>M) = (\<integral>\<^sup>+ x. f ((T^^n) x) * g x \<partial>M)"
proof -
  have "\<And>f g. f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<integral>\<^sup>+ x. f x * (nn_transfer_operator^^n) g x \<partial>M) = (\<integral>\<^sup>+ x. f ((T^^n) x) * g x \<partial>M)" for n
  proof (induction n)
    case (Suc n)
    have [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M" by fact+
    have "(\<integral>\<^sup>+ x. f x * (nn_transfer_operator ^^ Suc n) g x \<partial>M) = (\<integral>\<^sup>+ x. f x * (nn_transfer_operator ((nn_transfer_operator^^n) g)) x \<partial>M)"
      apply (rule nn_integral_cong) using funpow.simps(2) unfolding comp_def by auto
    also have "... = (\<integral>\<^sup>+ x. f (T x) * (nn_transfer_operator^^n) g x \<partial>M)"
      by (rule nn_transfer_operator_intg, auto)
    also have "... = (\<integral>\<^sup>+ x. (\<lambda>x. f (T x)) ((T^^n) x) * g x \<partial>M)"
      by (rule Suc.IH, auto)
    also have "... = (\<integral>\<^sup>+ x. f ((T^^(Suc n)) x) * g x \<partial>M)"
      apply (rule nn_integral_cong) using funpow.simps(2) unfolding comp_def by auto
    finally show ?case by auto
  qed (simp)
  then show ?thesis using assms by auto
qed

lemma nn_transfer_operator_intg_Tn:
  assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  shows "(\<integral>\<^sup>+ x. (nn_transfer_operator^^n) g x * f x \<partial>M) = (\<integral>\<^sup>+ x. g x * f ((T^^n) x) \<partial>M)"
using nn_transfer_operator_intTn_g[OF assms, of n] by (simp add: algebra_simps)

lemma nn_transfer_operator_charact:
  assumes "\<And>A. A \<in> sets M \<Longrightarrow> (\<integral>\<^sup>+ x. indicator A x * g x \<partial>M) = (\<integral>\<^sup>+ x. indicator A (T x) * f x \<partial>M)" and
          [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  shows "AE x in M. nn_transfer_operator f x = g x"
proof -
  have *:"set_nn_integral M A g = set_nn_integral M A (nn_transfer_operator f)" if [measurable]: "A \<in> sets M" for A
  proof -
    have "set_nn_integral M A g = (\<integral>\<^sup>+ x. indicator A x * g x \<partial>M)"
      using mult.commute by metis
    also have "... = (\<integral>\<^sup>+ x. indicator A (T x) * f x \<partial>M)"
      using assms(1) by auto
    also have "... = (\<integral>\<^sup>+ x. indicator A x * nn_transfer_operator f x \<partial>M)"
      by (rule nn_transfer_operator_intg[symmetric], auto)
    finally show ?thesis
      using mult.commute by (metis (no_types, lifting) nn_integral_cong)
  qed
  show ?thesis
    by (rule sigma_finite_measure.density_unique2, auto simp add: sigma_finite_measure_axioms *)
qed

text \<open>When $T$ is measure-preserving, $\hat T(f \circ T) = f$.\<close>

lemma (in mpt) nn_transfer_operator_foT:
  assumes [measurable]: "f \<in> borel_measurable M"
  shows "AE x in M. nn_transfer_operator (f o T) x = f x"
proof -
  have *: "(\<integral>\<^sup>+ x. indicator A x * f x \<partial>M) = (\<integral>\<^sup>+ x. indicator A (T x) * f (T x) \<partial>M)" if [measurable]: "A \<in> sets M" for A
    by (subst T_nn_integral_preserving[symmetric]) auto
  show ?thesis
    by (rule nn_transfer_operator_charact) (auto simp add: assms *)
qed

text \<open>In general, one only has $\hat T(f\circ T \cdot g) = f \cdot \hat T g$.\<close>
lemma nn_transfer_operator_foT_g:
  assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  shows "AE x in M. nn_transfer_operator (\<lambda>x. f (T x) * g x) x = f x * nn_transfer_operator g x"
proof -
  have *: "(\<integral>\<^sup>+ x. indicator A x * (f x * nn_transfer_operator g x) \<partial>M) = (\<integral>\<^sup>+ x. indicator A (T x) * (f (T x) * g x) \<partial>M)"
    if [measurable]: "A \<in> sets M" for A
    by (simp add: mult.assoc[symmetric] nn_transfer_operator_intg)
  show ?thesis
    by (rule nn_transfer_operator_charact) (auto simp add: assms *)
qed

lemma nn_transfer_operator_cmult:
  assumes [measurable]: "g \<in> borel_measurable M"
  shows "AE x in M. nn_transfer_operator (\<lambda>x. c * g x) x = c * nn_transfer_operator g x"
apply (rule nn_transfer_operator_foT_g) using assms by auto

lemma nn_transfer_operator_zero:
  "AE x in M. nn_transfer_operator (\<lambda>x. 0) x = 0"
using nn_transfer_operator_cmult[of "\<lambda>x. 0" 0] by auto

lemma nn_transfer_operator_sum:
  assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  shows "AE x in M. nn_transfer_operator (\<lambda>x. f x + g x) x = nn_transfer_operator f x + nn_transfer_operator g x"
proof (rule nn_transfer_operator_charact)
  fix A assume [measurable]: "A \<in> sets M"
  have "(\<integral>\<^sup>+ x. indicator A x * (nn_transfer_operator f x + nn_transfer_operator g x) \<partial>M) =
        (\<integral>\<^sup>+ x. indicator A x * nn_transfer_operator f x + indicator A x * nn_transfer_operator g x \<partial>M)"
    by (auto simp add: algebra_simps)
  also have "... = (\<integral>\<^sup>+x. indicator A x * nn_transfer_operator f x \<partial>M) + (\<integral>\<^sup>+x. indicator A x * nn_transfer_operator g x \<partial>M)"
    by (rule nn_integral_add, auto)
  also have "... = (\<integral>\<^sup>+x. indicator A (T x) * f x \<partial>M) + (\<integral>\<^sup>+x. indicator A (T x) * g x \<partial>M)"
    by (simp add: nn_transfer_operator_intg)
  also have "... = (\<integral>\<^sup>+x. indicator A (T x) * f x + indicator A (T x) * g x \<partial>M)"
    by (rule nn_integral_add[symmetric], auto)
  also have "... = (\<integral>\<^sup>+x. indicator A (T x) * (f x + g x) \<partial>M)"
    by (auto simp add: algebra_simps)
  finally show "(\<integral>\<^sup>+ x. indicator A x * (nn_transfer_operator f x + nn_transfer_operator g x) \<partial>M) = (\<integral>\<^sup>+x. indicator A (T x) * (f x + g x) \<partial>M)"
    by simp
qed (auto simp add: assms)

lemma nn_transfer_operator_cong:
  assumes "AE x in M. f x = g x"
      and [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  shows "AE x in M. nn_transfer_operator f x = nn_transfer_operator g x"
apply (rule nn_transfer_operator_charact)
apply (auto simp add: nn_transfer_operator_intg assms intro!: nn_integral_cong_AE)
using assms by auto

lemma nn_transfer_operator_mono:
  assumes "AE x in M. f x \<le> g x"
      and [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  shows "AE x in M. nn_transfer_operator f x \<le> nn_transfer_operator g x"
proof -
  define h where "h = (\<lambda>x. g x - f x)"
  have [measurable]: "h \<in> borel_measurable M" unfolding h_def by simp
  have *: "AE x in M. g x = f x + h x" unfolding h_def using assms(1) by (auto simp: ennreal_ineq_diff_add)
  have "AE x in M. nn_transfer_operator g x = nn_transfer_operator (\<lambda>x. f x + h x) x"
    by (rule nn_transfer_operator_cong) (auto simp add: * assms)
  moreover have "AE x in M. nn_transfer_operator (\<lambda>x. f x + h x) x = nn_transfer_operator f x + nn_transfer_operator h x"
    by (rule nn_transfer_operator_sum) (auto simp add: assms)
  ultimately have "AE x in M. nn_transfer_operator g x = nn_transfer_operator f x + nn_transfer_operator h x" by auto
  then show ?thesis by force
qed

subsection \<open>The transfer operator on real functions\<close>

text \<open>Once the transfer operator of positive functions is defined, the definition for real-valued
functions follows readily, by taking the difference of positive and negative parts.
\<close>

definition real_transfer_operator :: "('a \<Rightarrow> real) \<Rightarrow> ('a \<Rightarrow> real)" where
  "real_transfer_operator f =
    (\<lambda>x. enn2real(nn_transfer_operator (\<lambda>x. ennreal (f x)) x) - enn2real(nn_transfer_operator (\<lambda>x. ennreal (-f x)) x))"

lemma borel_measurable_transfer_operator [measurable]:
  "real_transfer_operator f \<in> borel_measurable M"
unfolding real_transfer_operator_def by auto

lemma borel_measurable_transfer_operator_iterates [measurable]:
  assumes [measurable]: "f \<in> borel_measurable M"
  shows "(real_transfer_operator^^n) f \<in> borel_measurable M"
by (cases n, auto)

lemma real_transfer_operator_abs:
  assumes [measurable]: "f \<in> borel_measurable M"
  shows "AE x in M. abs (real_transfer_operator f x) \<le> nn_transfer_operator (\<lambda>x. ennreal (abs(f x))) x"
proof -
  define fp where "fp = (\<lambda>x. ennreal (f x))"
  define fm where "fm = (\<lambda>x. ennreal (- f x))"
  have [measurable]: "fp \<in> borel_measurable M" "fm \<in> borel_measurable M" unfolding fp_def fm_def by auto
  have eq: "\<And>x. ennreal \<bar>f x\<bar> = fp x + fm x" unfolding fp_def fm_def by (simp add: abs_real_def ennreal_neg)

  {
    fix x assume H: "nn_transfer_operator (\<lambda>x. fp x + fm x) x = nn_transfer_operator fp x + nn_transfer_operator fm x"
    have "\<bar>real_transfer_operator f x\<bar> \<le> \<bar>enn2real(nn_transfer_operator fp x)\<bar> + \<bar>enn2real(nn_transfer_operator fm x)\<bar>"
      unfolding real_transfer_operator_def fp_def fm_def by (auto intro: abs_triangle_ineq4 simp del: enn2real_nonneg)
    from ennreal_leI[OF this]
    have "abs(real_transfer_operator f x) \<le> nn_transfer_operator fp x + nn_transfer_operator fm x"
      by simp (metis add.commute ennreal_enn2real le_iff_add not_le top_unique)
    also have "... = nn_transfer_operator (\<lambda>x. fp x + fm x) x" using H by simp
    finally have "abs(real_transfer_operator f x) \<le> nn_transfer_operator (\<lambda>x. fp x + fm x) x" by simp
  }
  moreover have "AE x in M. nn_transfer_operator (\<lambda>x. fp x + fm x) x = nn_transfer_operator fp x + nn_transfer_operator fm x"
    by (rule nn_transfer_operator_sum) (auto simp add: fp_def fm_def)
  ultimately have "AE x in M. abs(real_transfer_operator f x) \<le> nn_transfer_operator (\<lambda>x. fp x + fm x) x"
    by auto
  then show ?thesis using eq by simp
qed

text \<open>The next lemma shows that the transfer operator as we have defined it satisfies the basic
duality relation $\int \hat T f \cdot g = \int f \cdot g \circ T$. It follows from the same relation
for nonnegative functions, and splitting into positive and negative parts.

Moreover, this relation characterizes the transfer operator. Hence, once this lemma is proved, we
will never come back to the original definition of the transfer operator.\<close>

lemma real_transfer_operator_intg_fpos:
  assumes "integrable M (\<lambda>x. f (T x) * g x)" and f_pos[simp]: "\<And>x. f x \<ge> 0" and
          [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  shows "integrable M (\<lambda>x. f x * real_transfer_operator g x)"
        "(\<integral> x. f x * real_transfer_operator g x \<partial>M) = (\<integral> x. f (T x) * g x \<partial>M)"
proof -
  define gp where "gp = (\<lambda>x. ennreal (g x))"
  define gm where "gm = (\<lambda>x. ennreal (- g x))"
  have [measurable]: "gp \<in> borel_measurable M" "gm \<in> borel_measurable M" unfolding gp_def gm_def by auto
  define h where "h = (\<lambda>x. ennreal(abs(g x)))"
  have hgpgm: "\<And>x. h x = gp x + gm x" unfolding gp_def gm_def h_def by (simp add: abs_real_def ennreal_neg)
  have [measurable]: "h \<in> borel_measurable M" unfolding h_def by simp
  have pos[simp]: "\<And>x. h x \<ge> 0" "\<And>x. gp x \<ge> 0" "\<And>x. gm x \<ge> 0" unfolding h_def gp_def gm_def by simp_all
  have gp_real: "\<And>x. enn2real(gp x) = max (g x) 0"
    unfolding gp_def by (simp add: max_def ennreal_neg)
  have gm_real: "\<And>x. enn2real(gm x) = max (-g x) 0"
    unfolding gm_def by (simp add: max_def ennreal_neg)

  have "(\<integral>\<^sup>+ x. norm(f (T x) * max (g x) 0) \<partial>M) \<le> (\<integral>\<^sup>+ x. norm(f (T x) * g x) \<partial>M)"
    by (simp add: nn_integral_mono)
  also have "... < \<infinity>" using assms(1) by (simp add: integrable_iff_bounded)
  finally have "(\<integral>\<^sup>+ x. norm(f (T x) * max (g x) 0) \<partial>M) < \<infinity>" by simp
  then have int1: "integrable M (\<lambda>x. f (T x) * max (g x) 0)" by (simp add: integrableI_bounded)

  have "(\<integral>\<^sup>+ x. norm(f (T x) * max (-g x) 0) \<partial>M) \<le> (\<integral>\<^sup>+ x. norm(f (T x) * g x) \<partial>M)"
    by (simp add: nn_integral_mono)
  also have "... < \<infinity>" using assms(1) by (simp add: integrable_iff_bounded)
  finally have "(\<integral>\<^sup>+ x. norm(f (T x) * max (-g x) 0) \<partial>M) < \<infinity>" by simp
  then have int2: "integrable M (\<lambda>x. f (T x) * max (-g x) 0)" by (simp add: integrableI_bounded)

  have "(\<integral>\<^sup>+x. f x * nn_transfer_operator h x \<partial>M) = (\<integral>\<^sup>+x. f (T x) * h x \<partial>M)"
    by (rule nn_transfer_operator_intg) auto
  also have "\<dots> = \<integral>\<^sup>+ x. ennreal (f (T x) * max (g x) 0 + f (T x) * max (- g x) 0) \<partial>M"
    unfolding h_def
    by (intro nn_integral_cong)(auto simp: ennreal_mult[symmetric] abs_mult split: split_max)
  also have "... < \<infinity>"
    using Bochner_Integration.integrable_add[OF int1 int2, THEN integrableD(2)] by (auto simp add: less_top)
  finally have *: "(\<integral>\<^sup>+x. f x * nn_transfer_operator h x \<partial>M) < \<infinity>" by simp

  have "(\<integral>\<^sup>+x. norm(f x * real_transfer_operator g x) \<partial>M) = (\<integral>\<^sup>+x. f x * abs(real_transfer_operator g x) \<partial>M)"
    by (simp add: abs_mult)
  also have "... \<le> (\<integral>\<^sup>+x. f x * nn_transfer_operator h x \<partial>M)"
  proof (rule nn_integral_mono_AE)
    {
      fix x assume *: "abs(real_transfer_operator g x) \<le> nn_transfer_operator h x"
      have "ennreal (f x * \<bar>real_transfer_operator g x\<bar>) = f x * ennreal(\<bar>real_transfer_operator g x\<bar>)"
        by (simp add: ennreal_mult)
      also have "... \<le> f x * nn_transfer_operator h x"
        using * by (auto intro!: mult_left_mono)
      finally have "ennreal (f x * \<bar>real_transfer_operator g x\<bar>) \<le> f x * nn_transfer_operator h x"
        by simp
    }
    then show "AE x in M. ennreal (f x * \<bar>real_transfer_operator g x\<bar>) \<le> f x * nn_transfer_operator h x"
      using real_transfer_operator_abs[OF assms(4)] h_def by auto
  qed
  finally have **: "(\<integral>\<^sup>+x. norm(f x * real_transfer_operator g x) \<partial>M) < \<infinity>" using * by auto
  show "integrable M (\<lambda>x. f x * real_transfer_operator g x)"
    using ** by (intro integrableI_bounded) auto

  have "(\<integral>\<^sup>+x. f x * nn_transfer_operator gp x \<partial>M) \<le> (\<integral>\<^sup>+x. f x * nn_transfer_operator h x \<partial>M)"
  proof (rule nn_integral_mono_AE)
    have "AE x in M. nn_transfer_operator gp x \<le> nn_transfer_operator h x"
      by (rule nn_transfer_operator_mono) (auto simp add: hgpgm)
    then show "AE x in M. f x * nn_transfer_operator gp x \<le> f x * nn_transfer_operator h x"
      by (auto simp: mult_left_mono)
  qed
  then have a: "(\<integral>\<^sup>+x. f x * nn_transfer_operator gp x \<partial>M) < \<infinity>"
    using * by auto
  have "ennreal(norm(f x * enn2real(nn_transfer_operator gp x))) \<le> f x * nn_transfer_operator gp x" for x
    by (auto simp add: ennreal_mult intro!: mult_left_mono)
       (metis enn2real_ennreal enn2real_nonneg le_cases le_ennreal_iff)
  then have "(\<integral>\<^sup>+x. norm(f x * enn2real(nn_transfer_operator gp x)) \<partial>M) \<le> (\<integral>\<^sup>+x. f x * nn_transfer_operator gp x \<partial>M)"
    by (simp add: nn_integral_mono)
  then have "(\<integral>\<^sup>+x. norm(f x * enn2real(nn_transfer_operator gp x)) \<partial>M) < \<infinity>" using a by auto
  then have gp_int: "integrable M (\<lambda>x. f x * enn2real(nn_transfer_operator gp x))" by (simp add: integrableI_bounded)
  have gp_fin: "AE x in M. f x * nn_transfer_operator gp x \<noteq> \<infinity>"
    apply (rule nn_integral_PInf_AE) using a by auto

  have "(\<integral> x. f x * enn2real(nn_transfer_operator gp x) \<partial>M) = enn2real (\<integral>\<^sup>+ x. f x * enn2real(nn_transfer_operator gp x) \<partial>M)"
    by (rule integral_eq_nn_integral) auto
  also have "... = enn2real(\<integral>\<^sup>+ x. ennreal(f (T x) * enn2real(gp x)) \<partial>M)"
  proof -
    {
      fix x assume "f x * nn_transfer_operator gp x \<noteq> \<infinity>"
      then have "ennreal (f x * enn2real (nn_transfer_operator gp x)) = ennreal (f x) * nn_transfer_operator gp x"
        by (auto simp add: ennreal_mult ennreal_mult_eq_top_iff less_top intro!: ennreal_mult_left_cong)
    }
    then have "AE x in M. ennreal (f x * enn2real (nn_transfer_operator gp x)) = ennreal (f x) * nn_transfer_operator gp x"
      using gp_fin by auto
    then have "(\<integral>\<^sup>+ x. f x * enn2real(nn_transfer_operator gp x) \<partial>M) = (\<integral>\<^sup>+ x. f x * nn_transfer_operator gp x \<partial>M)"
      by (rule nn_integral_cong_AE)
    also have "... = (\<integral>\<^sup>+ x. f (T x) * gp x \<partial>M)"
      by (rule nn_transfer_operator_intg) (auto simp add: gp_def)
    also have "... = (\<integral>\<^sup>+ x. ennreal(f (T x) * enn2real(gp x)) \<partial>M)"
      by (rule nn_integral_cong_AE) (auto simp: ennreal_mult gp_def)
    finally have "(\<integral>\<^sup>+ x. f x * enn2real(nn_transfer_operator gp x) \<partial>M) = (\<integral>\<^sup>+ x. ennreal(f (T x) * enn2real(gp x)) \<partial>M)" by simp
    then show ?thesis by simp
  qed
  also have "... = (\<integral> x. f (T x) * enn2real(gp x) \<partial>M)"
    by (rule integral_eq_nn_integral[symmetric]) (auto simp add: gp_def)
  finally have gp_expr: "(\<integral> x. f x * enn2real(nn_transfer_operator gp x) \<partial>M) = (\<integral> x. f (T x) * enn2real(gp x) \<partial>M)" by simp

  have "(\<integral>\<^sup>+x. f x * nn_transfer_operator gm x \<partial>M) \<le> (\<integral>\<^sup>+x. f x * nn_transfer_operator h x \<partial>M)"
  proof (rule nn_integral_mono_AE)
    have "AE x in M. nn_transfer_operator gm x \<le> nn_transfer_operator h x"
      by (rule nn_transfer_operator_mono) (auto simp add: hgpgm)
    then show "AE x in M. f x * nn_transfer_operator gm x \<le> f x * nn_transfer_operator h x"
      by (auto simp: mult_left_mono)
  qed
  then have a: "(\<integral>\<^sup>+x. f x * nn_transfer_operator gm x \<partial>M) < \<infinity>"
    using * by auto
  have "\<And>x. ennreal(norm(f x * enn2real(nn_transfer_operator gm x))) \<le> f x * nn_transfer_operator gm x"
    by (auto simp add: ennreal_mult intro!: mult_left_mono)
       (metis enn2real_ennreal enn2real_nonneg le_cases le_ennreal_iff)
  then have "(\<integral>\<^sup>+x. norm(f x * enn2real(nn_transfer_operator gm x)) \<partial>M) \<le> (\<integral>\<^sup>+x. f x * nn_transfer_operator gm x \<partial>M)"
    by (simp add: nn_integral_mono)
  then have "(\<integral>\<^sup>+x. norm(f x * enn2real(nn_transfer_operator gm x)) \<partial>M) < \<infinity>" using a by auto
  then have gm_int: "integrable M (\<lambda>x. f x * enn2real(nn_transfer_operator gm x))" by (simp add: integrableI_bounded)
  have gm_fin: "AE x in M. f x * nn_transfer_operator gm x \<noteq> \<infinity>"
    apply (rule nn_integral_PInf_AE) using a by auto

  have "(\<integral> x. f x * enn2real(nn_transfer_operator gm x) \<partial>M) = enn2real (\<integral>\<^sup>+ x. f x * enn2real(nn_transfer_operator gm x) \<partial>M)"
    by (rule integral_eq_nn_integral) auto
  also have "... = enn2real(\<integral>\<^sup>+ x. ennreal(f (T x) * enn2real(gm x)) \<partial>M)"
  proof -
    {
      fix x assume "f x * nn_transfer_operator gm x \<noteq> \<infinity>"
      then have "ennreal (f x * enn2real (nn_transfer_operator gm x)) = ennreal (f x) * nn_transfer_operator gm x"
        by (auto simp add: ennreal_mult ennreal_mult_eq_top_iff less_top intro!: ennreal_mult_left_cong)
    }
    then have "AE x in M. ennreal (f x * enn2real (nn_transfer_operator gm x)) = ennreal (f x) * nn_transfer_operator gm x"
      using gm_fin by auto
    then have "(\<integral>\<^sup>+ x. f x * enn2real(nn_transfer_operator gm x) \<partial>M) = (\<integral>\<^sup>+ x. f x * nn_transfer_operator gm x \<partial>M)"
      by (rule nn_integral_cong_AE)
    also have "... = (\<integral>\<^sup>+ x. f (T x) * gm x \<partial>M)"
      by (rule nn_transfer_operator_intg) (auto simp add: gm_def)
    also have "... = (\<integral>\<^sup>+ x. ennreal(f (T x) * enn2real(gm x)) \<partial>M)"
      by (rule nn_integral_cong_AE) (auto simp: ennreal_mult gm_def)
    finally have "(\<integral>\<^sup>+ x. f x * enn2real(nn_transfer_operator gm x) \<partial>M) = (\<integral>\<^sup>+ x. ennreal(f (T x) * enn2real(gm x)) \<partial>M)" by simp
    then show ?thesis by simp
  qed
  also have "... = (\<integral> x. f (T x) * enn2real(gm x) \<partial>M)"
    by (rule integral_eq_nn_integral[symmetric]) (auto simp add: gm_def)
  finally have gm_expr: "(\<integral> x. f x * enn2real(nn_transfer_operator gm x) \<partial>M) = (\<integral> x. f (T x) * enn2real(gm x) \<partial>M)" by simp

  have "(\<integral> x. f x * real_transfer_operator g x \<partial>M) = (\<integral> x. f x * enn2real(nn_transfer_operator gp x) - f x * enn2real(nn_transfer_operator gm x) \<partial>M)"
    unfolding real_transfer_operator_def gp_def gm_def by (simp add: right_diff_distrib)
  also have "... = (\<integral> x. f x * enn2real(nn_transfer_operator gp x) \<partial>M) - (\<integral> x. f x * enn2real(nn_transfer_operator gm x) \<partial>M)"
    by (rule Bochner_Integration.integral_diff) (simp_all add: gp_int gm_int)
  also have "... = (\<integral> x. f (T x) * enn2real(gp x) \<partial>M) - (\<integral> x. f (T x) * enn2real(gm x) \<partial>M)"
    using gp_expr gm_expr by simp
  also have "... = (\<integral> x. f (T x) * max (g x) 0 \<partial>M) - (\<integral> x. f (T x) * max (-g x) 0 \<partial>M)"
    using gp_real gm_real by simp
  also have "... = (\<integral> x. f (T x) * max (g x) 0 - f (T x) * max (-g x) 0 \<partial>M)"
    by (rule Bochner_Integration.integral_diff[symmetric]) (simp_all add: int1 int2)
  also have "... = (\<integral>x. f (T x) * g x \<partial>M)"
    by (metis (mono_tags, opaque_lifting) diff_0 diff_zero eq_iff max.cobounded2 max_def minus_minus neg_le_0_iff_le right_diff_distrib)
  finally show "(\<integral> x. f x * real_transfer_operator g x \<partial>M) = (\<integral>x. f (T x) * g x \<partial>M)"
    by simp
qed

lemma real_transfer_operator_intg:
  assumes "integrable M (\<lambda>x. f (T x) * g x)" and
          [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  shows "integrable M (\<lambda>x. f x * real_transfer_operator g x)"
        "(\<integral> x. f x * real_transfer_operator g x \<partial>M) = (\<integral> x. f (T x) * g x \<partial>M)"
proof -
  define fp where "fp = (\<lambda>x. max (f x) 0)"
  define fm where "fm = (\<lambda>x. max (-f x) 0)"
  have [measurable]: "fp \<in> borel_measurable M" "fm \<in> borel_measurable M"
    unfolding fp_def fm_def by simp_all

  have "(\<integral>\<^sup>+ x. norm(fp (T x) * g x) \<partial>M) \<le> (\<integral>\<^sup>+ x. norm(f (T x) * g x) \<partial>M)"
    by (simp add: fp_def nn_integral_mono)
  also have "... < \<infinity>" using assms(1) by (simp add: integrable_iff_bounded)
  finally have "(\<integral>\<^sup>+ x. norm(fp (T x) * g x) \<partial>M) < \<infinity>" by simp
  then have intp: "integrable M (\<lambda>x. fp (T x) * g x)" by (simp add: integrableI_bounded)
  moreover have "\<And>x. fp x \<ge> 0" unfolding fp_def by simp
  ultimately have Rp: "integrable M (\<lambda>x. fp x * real_transfer_operator g x)"
    "(\<integral> x. fp x * real_transfer_operator g x \<partial>M) = (\<integral> x. fp (T x) * g x \<partial>M)"
  using real_transfer_operator_intg_fpos by auto

  have "(\<integral>\<^sup>+ x. norm(fm (T x) * g x) \<partial>M) \<le> (\<integral>\<^sup>+ x. norm(f (T x) * g x) \<partial>M)"
    by (simp add: fm_def nn_integral_mono)
  also have "... < \<infinity>" using assms(1) by (simp add: integrable_iff_bounded)
  finally have "(\<integral>\<^sup>+ x. norm(fm (T x) * g x) \<partial>M) < \<infinity>" by simp
  then have intm: "integrable M (\<lambda>x. fm (T x) * g x)" by (simp add: integrableI_bounded)
  moreover have "\<And>x. fm x \<ge> 0" unfolding fm_def by simp
  ultimately have Rm: "integrable M (\<lambda>x. fm x * real_transfer_operator g x)"
    "(\<integral> x. fm x * real_transfer_operator g x \<partial>M) = (\<integral> x. fm (T x) * g x \<partial>M)"
  using real_transfer_operator_intg_fpos by auto

  have "integrable M (\<lambda>x. fp x * real_transfer_operator g x - fm x * real_transfer_operator g x)"
    using Rp(1) Rm(1) integrable_diff by simp
  moreover have *: "\<And>x. f x * real_transfer_operator g x = fp x * real_transfer_operator g x - fm x * real_transfer_operator g x"
    unfolding fp_def fm_def by (simp add: max_def)
  ultimately show "integrable M (\<lambda>x. f x * real_transfer_operator g x)"
    by simp

  have "(\<integral> x. f x * real_transfer_operator g x \<partial>M) = (\<integral> x. fp x * real_transfer_operator g x - fm x * real_transfer_operator g x \<partial>M)"
    using * by simp
  also have "... = (\<integral> x. fp x * real_transfer_operator g x \<partial>M) - (\<integral> x. fm x * real_transfer_operator g x \<partial>M)"
    using Rp(1) Rm(1) by simp
  also have "... = (\<integral> x. fp (T x) * g x \<partial>M) - (\<integral> x. fm (T x) * g x \<partial>M)"
    using Rp(2) Rm(2) by simp
  also have "... = (\<integral> x. fp (T x) * g x - fm (T x) * g x \<partial>M)"
    using intm intp by simp
  also have "... = (\<integral> x. f (T x) * g x \<partial>M)"
    unfolding fp_def fm_def by (metis (no_types, opaque_lifting) diff_0 diff_zero max.commute
    max_def minus_minus mult.commute neg_le_iff_le right_diff_distrib)
  finally show "(\<integral> x. f x * real_transfer_operator g x \<partial>M) = (\<integral> x. f (T x) * g x \<partial>M)" by simp
qed

lemma real_transfer_operator_int [intro]:
  assumes "integrable M f"
  shows "integrable M (real_transfer_operator f)"
        "(\<integral>x. real_transfer_operator f x \<partial>M) = (\<integral>x. f x \<partial>M)"
using real_transfer_operator_intg[where ?f = "\<lambda>x. 1" and ?g = f] assms by auto

lemma real_transfer_operator_charact:
  assumes "\<And>A. A \<in> sets M \<Longrightarrow> (\<integral>x. indicator A x * g x \<partial>M) = (\<integral>x. indicator A (T x) * f x \<partial>M)"
      and [measurable]: "integrable M f" "integrable M g"
  shows "AE x in M. real_transfer_operator f x = g x"
proof (rule AE_symmetric[OF density_unique_real])
  fix A assume [measurable]: "A \<in> sets M"
  have "set_lebesgue_integral M A (real_transfer_operator f) = (\<integral>x. indicator A x * real_transfer_operator f x \<partial>M)"
    unfolding set_lebesgue_integral_def by auto
  also have "... = (\<integral>x. indicator A (T x) * f x \<partial>M)"
    apply (rule real_transfer_operator_intg, auto)
    by (rule Bochner_Integration.integrable_bound[of _ "\<lambda>x. abs(f x)"], auto simp add: assms indicator_def)
  also have "... = set_lebesgue_integral M A g"
    unfolding set_lebesgue_integral_def using assms(1)[OF \<open>A \<in> sets M\<close>] by auto
  finally show "set_lebesgue_integral M A g = set_lebesgue_integral M A (real_transfer_operator f)"
    by simp
qed (auto simp add: assms real_transfer_operator_int)

lemma (in mpt) real_transfer_operator_foT:
  assumes "integrable M f"
  shows "AE x in M. real_transfer_operator (f o T) x = f x"
proof -
  have *: "(\<integral> x. indicator A x * f x \<partial>M) = (\<integral>x. indicator A (T x) * f (T x) \<partial>M)" if [measurable]: "A \<in> sets M" for A
    apply (subst T_integral_preserving)
    using integrable_real_mult_indicator[OF that assms] by (auto simp add: mult.commute)
  show ?thesis
    apply (rule real_transfer_operator_charact)
    using assms * by (auto simp add: comp_def T_integral_preserving)
qed

lemma real_transfer_operator_foT_g:
  assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M" "integrable M (\<lambda>x. f (T x) * g x)"
  shows "AE x in M. real_transfer_operator (\<lambda>x. f (T x) * g x) x = f x * real_transfer_operator g x"
proof -
  have *: "(\<integral>x. indicator A x * (f x * real_transfer_operator g x) \<partial>M) = (\<integral>x. indicator A (T x) * (f (T x) * g x) \<partial>M)"
    if [measurable]: "A \<in> sets M" for A
    apply (simp add: mult.assoc[symmetric])
    apply (subst real_transfer_operator_intg)
    apply (rule Bochner_Integration.integrable_bound[of _ "(\<lambda>x. f (T x) * g x)"])
    by (auto simp add: assms indicator_def)
  show ?thesis
    by (rule real_transfer_operator_charact) (auto simp add: assms * intro!: real_transfer_operator_intg)
qed

lemma real_transfer_operator_add [intro]:
  assumes [measurable]: "integrable M f" "integrable M g"
  shows "AE x in M. real_transfer_operator (\<lambda>x. f x + g x) x = real_transfer_operator f x + real_transfer_operator g x"
proof (rule real_transfer_operator_charact)
  have "integrable M (real_transfer_operator f)" "integrable M (real_transfer_operator g)"
    using real_transfer_operator_int(1) assms by auto
  then show "integrable M (\<lambda>x. real_transfer_operator f x + real_transfer_operator g x)"
    by auto

  fix A assume [measurable]: "A \<in> sets M"
  have intAf: "integrable M (\<lambda>x. indicator A (T x) * f x)"
    apply (rule Bochner_Integration.integrable_bound[OF assms(1)]) unfolding indicator_def by auto
  have intAg: "integrable M (\<lambda>x. indicator A (T x) * g x)"
    apply (rule Bochner_Integration.integrable_bound[OF assms(2)]) unfolding indicator_def by auto

  have "(\<integral>x. indicator A x * (real_transfer_operator f x + real_transfer_operator g x)\<partial>M)
      = (\<integral>x. indicator A x * real_transfer_operator f x + indicator A x* real_transfer_operator g x \<partial>M)"
    by (simp add: algebra_simps)
  also have "... = (\<integral>x. indicator A x * real_transfer_operator f x \<partial>M) + (\<integral>x. indicator A x * real_transfer_operator g x \<partial>M)"
    apply (rule Bochner_Integration.integral_add)
    using integrable_real_mult_indicator[OF \<open>A \<in> sets M\<close> real_transfer_operator_int(1)[OF assms(1)]]
          integrable_real_mult_indicator[OF \<open>A \<in> sets M\<close> real_transfer_operator_int(1)[OF assms(2)]]
    by (auto simp add: mult.commute)
  also have "... = (\<integral>x. indicator A (T x) * f x \<partial>M) + (\<integral>x. indicator A (T x) * g x \<partial>M)"
    using real_transfer_operator_intg(2) assms \<open>A \<in> sets M\<close> intAf intAg by auto
  also have "... = (\<integral>x. indicator A (T x) * f x + indicator A (T x) * g x \<partial>M)"
    by (rule Bochner_Integration.integral_add[symmetric]) (auto simp add: assms \<open>A \<in> sets M\<close> intAf intAg)
  also have "... = \<integral>x. indicator A (T x) * (f x + g x)\<partial>M"
    by (simp add: algebra_simps)
  finally show "(\<integral>x. indicator A x * (real_transfer_operator f x + real_transfer_operator g x)\<partial>M) = \<integral>x. indicator A (T x) * (f x + g x)\<partial>M"
    by simp
qed (auto simp add: assms)

lemma real_transfer_operator_cong:
  assumes ae: "AE x in M. f x = g x" and [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  shows "AE x in M. real_transfer_operator f x = real_transfer_operator g x"
proof -
  have "AE x in M. nn_transfer_operator (\<lambda>x. ennreal (f x)) x = nn_transfer_operator (\<lambda>x. ennreal (g x)) x"
    apply (rule nn_transfer_operator_cong) using assms by auto
  moreover have "AE x in M. nn_transfer_operator (\<lambda>x. ennreal (-f x)) x = nn_transfer_operator (\<lambda>x. ennreal(-g x)) x"
    apply (rule nn_transfer_operator_cong) using assms by auto
  ultimately show "AE x in M. real_transfer_operator f x = real_transfer_operator g x"
    unfolding real_transfer_operator_def by auto
qed

lemma real_transfer_operator_cmult [intro, simp]:
  fixes c::real
  assumes "integrable M f"
  shows "AE x in M. real_transfer_operator (\<lambda>x. c * f x) x = c * real_transfer_operator f x"
by (rule real_transfer_operator_foT_g) (auto simp add: assms borel_measurable_integrable)

lemma real_transfer_operator_cdiv [intro, simp]:
  fixes c::real
  assumes "integrable M f"
  shows "AE x in M. real_transfer_operator (\<lambda>x. f x / c) x = real_transfer_operator f x / c"
using real_transfer_operator_cmult[of _ "1/c", OF assms] by (auto simp add: divide_simps)

lemma real_transfer_operator_diff [intro, simp]:
  assumes [measurable]: "integrable M f" "integrable M g"
  shows "AE x in M. real_transfer_operator (\<lambda>x. f x - g x) x = real_transfer_operator f x - real_transfer_operator g x"
proof -
  have "AE x in M. real_transfer_operator (\<lambda>x. f x + (- g x)) x = real_transfer_operator f x + real_transfer_operator (\<lambda>x. -g x) x"
    using real_transfer_operator_add[where ?f = f and ?g = "\<lambda>x. - g x"] assms by auto
  moreover have "AE x in M. real_transfer_operator (\<lambda>x. -g x) x = - real_transfer_operator g x"
    using real_transfer_operator_cmult[where ?f = g and ?c = "-1"] assms(2) by auto
  ultimately show ?thesis by auto
qed

lemma real_transfer_operator_pos [intro]:
  assumes "AE x in M. f x \<ge> 0" and [measurable]: "f \<in> borel_measurable M"
  shows "AE x in M. real_transfer_operator f x \<ge> 0"
proof -
  define g where "g = (\<lambda>x. max (f x) 0)"
  have "AE x in M. f x = g x" using assms g_def by auto
  then have *: "AE x in M. real_transfer_operator f x = real_transfer_operator g x" using real_transfer_operator_cong g_def by auto

  have "\<And>x. g x \<ge> 0" unfolding g_def by simp
  then have "(\<lambda>x. ennreal(-g x)) = (\<lambda>x. 0)"
    by (simp add: ennreal_neg)
  then have "AE x in M. nn_transfer_operator (\<lambda>x. ennreal(-g x)) x = 0"
    using nn_transfer_operator_zero by simp
  then have "AE x in M. real_transfer_operator g x = enn2real(nn_transfer_operator (\<lambda>x. ennreal (g x)) x)"
    unfolding real_transfer_operator_def by auto
  then have "AE x in M. real_transfer_operator g x \<ge> 0" by auto
  then show ?thesis using * by auto
qed

lemma real_transfer_operator_mono:
  assumes "AE x in M. f x \<le> g x" and [measurable]: "integrable M f" "integrable M g"
  shows "AE x in M. real_transfer_operator f x \<le> real_transfer_operator g x"
proof -
  have "AE x in M. real_transfer_operator g x - real_transfer_operator f x = real_transfer_operator (\<lambda>x. g x - f x) x"
    by (rule AE_symmetric[OF real_transfer_operator_diff], auto simp add: assms)
  moreover have "AE x in M. real_transfer_operator (\<lambda>x. g x - f x) x \<ge> 0"
    by (rule real_transfer_operator_pos, auto simp add: assms(1))
  ultimately have "AE x in M. real_transfer_operator g x - real_transfer_operator f x \<ge> 0" by auto
  then show ?thesis by auto
qed

lemma real_transfer_operator_sum [intro, simp]:
  fixes f::"'b \<Rightarrow> 'a \<Rightarrow> real"
  assumes [measurable]: "\<And>i. integrable M (f i)"
  shows "AE x in M. real_transfer_operator (\<lambda>x. \<Sum>i\<in>I. f i x) x = (\<Sum>i\<in>I. real_transfer_operator (f i) x)"
proof (rule real_transfer_operator_charact)
  fix A assume [measurable]: "A \<in> sets M"
  have *: "integrable M (\<lambda>x. indicator A (T x) * f i x)" for i
    apply (rule Bochner_Integration.integrable_bound[of _ "f i"]) by (auto simp add: assms indicator_def)
  have **: "integrable M (\<lambda>x. indicator A x * real_transfer_operator (f i) x)" for i
    apply (rule Bochner_Integration.integrable_bound[of _ "real_transfer_operator (f i)"]) by (auto simp add: assms indicator_def)
  have inti: "(\<integral>x. indicator A (T x) * f i x \<partial>M) = (\<integral>x. indicator A x * real_transfer_operator (f i) x \<partial>M)" for i
    by (rule real_transfer_operator_intg(2)[symmetric], auto simp add: *)

  have "(\<integral>x. indicator A (T x) * (\<Sum>i\<in>I. f i x)\<partial>M) = (\<integral>x. (\<Sum>i\<in>I. indicator A (T x) * f i x)\<partial>M)"
    by (simp add: sum_distrib_left)
  also have "... = (\<Sum>i\<in>I. (\<integral>x. indicator A (T x) * f i x \<partial>M))"
    by (rule Bochner_Integration.integral_sum, simp add: *)
  also have "... = (\<Sum>i\<in>I. (\<integral>x. indicator A x * real_transfer_operator (f i) x \<partial>M))"
    using inti by auto
  also have "... = (\<integral>x. (\<Sum>i\<in>I. indicator A x * real_transfer_operator (f i) x)\<partial>M)"
    by (rule Bochner_Integration.integral_sum[symmetric], simp add: **)
  also have "... = (\<integral>x. indicator A x * (\<Sum>i\<in>I. real_transfer_operator (f i) x)\<partial>M)"
    by (simp add: sum_distrib_left)
  finally show "(\<integral>x. indicator A x * (\<Sum>i\<in>I. real_transfer_operator (f i) x)\<partial>M) = (\<integral>x. indicator A (T x) * (\<Sum>i\<in>I. f i x)\<partial>M)" by auto
qed (auto simp add: assms real_transfer_operator_int(1)[OF assms(1)])
end (*of context qmpt*)

subsection \<open>Conservativity in terms of transfer operators\<close>

text \<open>Conservativity amounts to the fact that $\sum f(T^n x) = \infty$ for almost every $x$
such that $f(x)>0$, if $f$ is nonnegative (see Lemma \verb+recurrent_series_infinite+).
There is a dual formulation, in terms of transfer
operators, asserting that $\sum \hat T^n f(x) = \infty$ for almost every $x$ such that $f(x)>0$.
It is proved by duality, reducing to the previous statement.\<close>

theorem (in conservative) recurrence_series_infinite_transfer_operator:
  assumes [measurable]: "f \<in> borel_measurable M"
  shows "AE x in M. f x > 0 \<longrightarrow> (\<Sum>n. (nn_transfer_operator^^n) f x) = \<infinity>"
proof -
  define A where "A = {x \<in> space M. f x > 0}"
  have [measurable]: "A \<in> sets M"
    unfolding A_def by auto
  have K: "emeasure M {x \<in> A. (\<Sum>n. (nn_transfer_operator^^n) f x) \<le> K} = 0" if "K < \<infinity>" for K
  proof (rule ccontr)
    assume "emeasure M {x \<in> A. (\<Sum>n. (nn_transfer_operator^^n) f x) \<le> K} \<noteq> 0"
    then have *: "emeasure M {x \<in> A. (\<Sum>n. (nn_transfer_operator^^n) f x) \<le> K} > 0"
      using not_gr_zero by blast
    obtain B where B [measurable]: "B \<in> sets M" "B \<subseteq> {x \<in> A. (\<Sum>n. (nn_transfer_operator^^n) f x) \<le> K}" "emeasure M B < \<infinity>" "emeasure M B > 0"
      using approx_with_finite_emeasure[OF _ *] by auto
    have "f x > 0" if "x \<in> B" for x
      using B(2) that unfolding A_def by auto
    moreover have "AE x\<in>B in M. (\<Sum>n. indicator B ((T^^n) x)) = (\<infinity>::ennreal)"
      using recurrence_series_infinite[of "indicator B"] by (auto simp add: indicator_def)
    ultimately have PInf: "AE x\<in>B in M. (\<Sum>n. indicator B ((T^^n) x)) * f x = \<top>"
      unfolding ennreal_mult_eq_top_iff by fastforce

    have "(\<integral>\<^sup>+x. indicator B x * (\<Sum>n. (nn_transfer_operator^^n) f x) \<partial>M) \<le> (\<integral>\<^sup>+x. indicator B x * K \<partial>M)"
      apply (rule nn_integral_mono) using B(2) unfolding indicator_def by auto
    also have "... = K * emeasure M B"
      by (simp add: mult.commute nn_integral_cmult_indicator)
    also have "... < \<infinity>" using \<open>K < \<infinity>\<close> B(3)
      using ennreal_mult_eq_top_iff top.not_eq_extremum by auto
    finally have *: "(\<integral>\<^sup>+x. indicator B x * (\<Sum>n. (nn_transfer_operator^^n) f x) \<partial>M) < \<infinity>" by auto

    have "(\<integral>\<^sup>+x. indicator B x * (\<Sum>n. (nn_transfer_operator^^n) f x) \<partial>M)
            = (\<integral>\<^sup>+x. (\<Sum>n. indicator B x * (nn_transfer_operator^^n) f x) \<partial>M)"
      by auto
    also have "... = (\<Sum>n. (\<integral>\<^sup>+x. indicator B x * (nn_transfer_operator^^n) f x \<partial>M))"
      by (rule nn_integral_suminf, auto)
    also have "... = (\<Sum>n. (\<integral>\<^sup>+x. indicator B ((T^^n) x) * f x \<partial>M))"
      using nn_transfer_operator_intTn_g by auto
    also have "... = (\<integral>\<^sup>+x. (\<Sum>n. indicator B ((T^^n) x) * f x) \<partial>M)"
      by (rule nn_integral_suminf[symmetric], auto)
    also have "... = (\<integral>\<^sup>+x. (\<Sum>n. indicator B ((T^^n) x)) * f x \<partial>M)"
      by auto
    finally have **: "(\<integral>\<^sup>+x. (\<Sum>n. indicator B ((T^^n) x)) * f x \<partial>M) \<noteq> \<infinity>"
      using * by simp
    have "AE x in M. (\<Sum>n. indicator B ((T^^n) x)) * f x \<noteq> \<infinity>"
      by (rule nn_integral_noteq_infinite[OF _ **], auto)
    then have "AE x\<in>B in M. False"
      using PInf by auto
    then have "emeasure M B = 0"
      by (smt AE_E B(1) Collect_mem_eq Collect_mono_iff dual_order.trans emeasure_eq_0 subsetD sets.sets_into_space)
    then show False
      using B by auto
  qed
  have L: "{x \<in> A. (\<Sum>n. (nn_transfer_operator^^n) f x) \<le> K} \<in> null_sets M" if "K < \<infinity>" for K
    using K[OF that] by auto
  have P: "AE x in M. x \<in> A \<longrightarrow> (\<Sum>n. (nn_transfer_operator^^n) f x) \<ge> K" if "K < \<infinity>" for K
    using AE_not_in[OF L[OF that]] by auto
  have "AE x in M. \<forall>N::nat. (x \<in> A \<longrightarrow> (\<Sum>n. (nn_transfer_operator^^n) f x) \<ge> of_nat N)"
    unfolding AE_all_countable by (auto simp add: of_nat_less_top intro!: P)
  then have "AE x in M. f x > 0 \<longrightarrow> (\<forall>N::nat. (\<Sum>n. (nn_transfer_operator^^n) f x) \<ge> of_nat N)"
    unfolding A_def by auto
  then show "AE x in M. 0 < f x \<longrightarrow> (\<Sum>n. (nn_transfer_operator ^^ n) f x) = \<infinity>"
    using ennreal_ge_nat_imp_PInf by auto
qed

end (*of Transfer_Operator.thy*)