Theory Lorenz_C1

theory Lorenz_C1
  imports
    Lorenz_Approximation.Lorenz_Approximation
begin

locale check_lines_c1 =
  assumes check_lines_c1: "check_lines True ordered_lines"
begin

lemma all_coarse_results: "Ball (set coarse_results) correct_res" if NF
  apply (rule Ball_coarseI)
   apply fact
   apply (rule check_lines_c1)
  apply eval
  done

theorem lorenz_bounds:
  "∀x ∈ N - Γ. x returns_to Σ"                              ― ‹‹R› is well defined›
  "R ` (N - Γ) ⊆ N"                                         ― ‹‹R› is forward invariant›
  "∀x ∈ N - Γ. (R has_derivative DR x) (at x within Σ⇩l⇩e)" ― ‹‹DR› is derivative›
  "∀x ∈ N - Γ. DR x ` ℭ x ⊆ ℭ (R x)"                        ― ‹‹ℭ› is mapped strictly into itself›
  "∀x ∈ N - Γ. ∀c ∈ ℭ x. norm (DR x c) ≥ ℰ x      * norm c" ― ‹expansion›
  "∀x ∈ N - Γ. ∀c ∈ ℭ x. norm (DR x c) ≥ ℰ⇩p (R x) * norm c"― ‹pre-expansion›
  if NF
  using lorenz_bounds_lemma_asym[OF ‹NF› reduce_lorenz_symmetry, OF all_coarse_results[OF ‹NF›]]
  by auto

end

interpretation check_lines_c1
  apply unfold_locales
  oops― ‹very very slow: about 50 CPU hours›
    ― ‹‹by (parallel_check (* "output_c1/lorenz_c1_" *) _ 60 20)››

end