Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. metadata
  2. min-range approximations for all remaining floatarith-constants; formalization of Poincare map; numerics for variational equation and Poincare map; computation of enclosure for Lorenz attractor; verified algorithms for checking C1-information of Lorenz attractor
Changeset 8329:b355113d158f by immler:
metadata
The file was modified metadata/metadata (diff)
Changeset 8328:e659b098f239 by immler:
min-range approximations for all remaining floatarith-constants; formalization of Poincare map; numerics for variational equation and Poincare map; computation of enclosure for Lorenz attractor; verified algorithms for checking C1-information of Lorenz attractor
The file was addedthys/Affine_Arithmetic/Affine_Arithmetic_Auxiliarities.thy
The file was addedthys/Affine_Arithmetic/Floatarith_Expression.thy
The file was addedthys/Affine_Arithmetic/Optimize_Float.thy
The file was addedthys/Affine_Arithmetic/Optimize_Integer.thy
The file was addedthys/Affine_Arithmetic/Print.thy
The file was addedthys/Ordinary_Differential_Equations/Ex/Examples_Integral.thy
The file was addedthys/Ordinary_Differential_Equations/Ex/Examples_One_Step_Method.thy
The file was addedthys/Ordinary_Differential_Equations/Ex/Examples_Poincare_Map.thy
The file was addedthys/Ordinary_Differential_Equations/Ex/Lorenz/Lorenz_C0.thy
The file was addedthys/Ordinary_Differential_Equations/Ex/Lorenz/Lorenz_C1.thy
The file was addedthys/Ordinary_Differential_Equations/Ex/Lorenz/Result_Elements.thy
The file was addedthys/Ordinary_Differential_Equations/Ex/Lorenz/Result_File_Coarse.thy
The file was addedthys/Ordinary_Differential_Equations/Ex/Lorenz/output/output
The file was addedthys/Ordinary_Differential_Equations/Ex/Lorenz/output_c1/output_c1
The file was addedthys/Ordinary_Differential_Equations/Ex/plot_file.plg
The file was addedthys/Ordinary_Differential_Equations/IVP/Cones.thy
The file was addedthys/Ordinary_Differential_Equations/IVP/Poincare_Map.thy
The file was addedthys/Ordinary_Differential_Equations/Library/Matrix_Exponential.thy
The file was addedthys/Ordinary_Differential_Equations/Numerics/Example_Utilities.thy
The file was addedthys/Ordinary_Differential_Equations/Numerics/Refine_Vector_List.thy
The file was addedthys/Ordinary_Differential_Equations/Numerics/Transfer_Euclidean_Space_Vector.thy
The file was modified thys/Affine_Arithmetic/Affine_Approximation.thy (diff)
The file was modified thys/Affine_Arithmetic/Affine_Code.thy (diff)
The file was modified thys/Affine_Arithmetic/Affine_Form.thy (diff)
The file was modified thys/Affine_Arithmetic/Counterclockwise_2D_Strict.thy (diff)
The file was modified thys/Affine_Arithmetic/Ex_Affine_Approximation.thy (diff)
The file was modified thys/Affine_Arithmetic/Ex_Ineqs.thy (diff)
The file was modified thys/Affine_Arithmetic/Ex_Inter.thy (diff)
The file was modified thys/Affine_Arithmetic/Executable_Euclidean_Space.thy (diff)
The file was modified thys/Affine_Arithmetic/Float_Real.thy (diff)
The file was modified thys/Affine_Arithmetic/Intersection.thy (diff)
The file was modified thys/Affine_Arithmetic/ROOT (diff)
The file was modified thys/Affine_Arithmetic/Straight_Line_Program.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Ex/Lorenz/Lorenz_Approximation.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/IVP/Flow.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/IVP/Initial_Value_Problem.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/IVP/Picard_Lindeloef_Qualitative.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/IVP/Reachability_Analysis.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Library/Multivariate_Taylor.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Numerics/Refine_Reachability_Analysis.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Numerics/Refine_Rigorous_Numerics.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Numerics/Refine_Rigorous_Numerics_Aform.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Numerics/Runge_Kutta.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/ODE_Analysis.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/ODE_Auxiliarities.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/ODE_Examples.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/ODE_Numerics.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/ROOT (diff)
The file was modified thys/Ordinary_Differential_Equations/Refinement/Autoref_Misc.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Refinement/Refine_Folds.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Refinement/Refine_String.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Refinement/Weak_Set.thy (diff)
The file was removedthys/Affine_Arithmetic/Euclidean_Space_Explicit.thy
The file was removedthys/Ordinary_Differential_Equations/Ex/Example1.thy
The file was removedthys/Ordinary_Differential_Equations/Ex/Example3.thy
The file was removedthys/Ordinary_Differential_Equations/Ex/Example_Bessel.thy
The file was removedthys/Ordinary_Differential_Equations/Ex/Example_Exp.thy
The file was removedthys/Ordinary_Differential_Equations/Ex/Example_Lorenz_Classic.thy
The file was removedthys/Ordinary_Differential_Equations/Ex/Example_Oil.thy
The file was removedthys/Ordinary_Differential_Equations/Ex/Example_Utilities.thy
The file was removedthys/Ordinary_Differential_Equations/Ex/Example_Variational_Equation.thy
The file was removedthys/Ordinary_Differential_Equations/Ex/Example_van_der_Pol.thy
The file was removedthys/Ordinary_Differential_Equations/Ex/Lorenz/Initials.thy
The file was removedthys/Ordinary_Differential_Equations/Ex/Lorenz/Lorenz_Parallel.thy
The file was removedthys/Ordinary_Differential_Equations/Numerics/Optimize_Float.thy
The file was removedthys/Ordinary_Differential_Equations/Numerics/Optimize_Integer.thy
The file was removedthys/Ordinary_Differential_Equations/Numerics/Plot.thy
The file was removedthys/Ordinary_Differential_Equations/Numerics/Print.thy