OAI/Analysis/MassAction/AffineTrajectory.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem326.hasDerivAt_dot_curve line 16

   Source documentation

   Differentiation of a fixed linear functional along a state-space curve.

   theorem hasDerivAt_dot_curve {d : ℕ} (a : Fin d → ℝ)
       {x : ℝ → (Fin d → ℝ)} {v : Fin d → ℝ} {t : ℝ}
       (hx : HasDerivAt x v t) :
       HasDerivAt (fun u => dot a (x u)) (dot a v) t := by
   …

   Mentions: OAI.Problem326.dot

2. theorem OAI.Problem326.continuousOn_dot_curve line 24

   Source documentation

   Fixed affine functionals preserve continuity on a time interval.

   theorem continuousOn_dot_curve {d : ℕ} (a : Fin d → ℝ)
       {x : ℝ → (Fin d → ℝ)} {S : Set ℝ} (hx : ContinuousOn x S) :
       ContinuousOn (fun t => dot a (x t)) S := by
   …

   Mentions: OAI.Problem326.dot

3. theorem OAI.Problem326.affineMinimum_monotoneOn line 32

   Source documentation

   An active inward-pointing condition makes a finite affine minimum nondecreasing along any differentiable curve in the specified region.

   theorem affineMinimum_monotoneOn
       {d : ℕ} {ι : Type uIota} (s : Finset ι) (hs : s.Nonempty)
       (a : ι → (Fin d → ℝ)) (c : ι → ℝ)
       (f : (Fin d → ℝ) → (Fin d → ℝ)) (B : Set (Fin d → ℝ))
       {x : ℝ → (Fin d → ℝ)} {u v : ℝ}
       (hx : ContinuousOn x (Icc u v))
       (hxd : ∀ t ∈ Ioo u v, HasDerivAt x (f (x t)) t)
       (hB : ∀ t ∈ Icc u v, x t ∈ B)
       (hinward : ∀ z ∈ B, ∀ i ∈ s,
         dot (a i) z + c i = s.inf' hs (fun j => dot (a j) z + c j) →
         0 ≤ dot (a i) (f z)) :
       MonotoneOn (fun t => s.inf' hs (fun i => dot (a i) (x t) + c i)) (Icc u v) := by
   …

   Mentions: OAI.Problem326.dot

4. theorem OAI.Problem326.affineMinimum_eq_of_ceiling line 54

   Source documentation

   The maximum-level plateau is preserved along a solution segment in the region where all active affine branches point inward.

   theorem affineMinimum_eq_of_ceiling
       {d : ℕ} {ι : Type uIota} (s : Finset ι) (hs : s.Nonempty)
       (a : ι → (Fin d → ℝ)) (c : ι → ℝ)
       (f : (Fin d → ℝ) → (Fin d → ℝ)) (B : Set (Fin d → ℝ))
       {x : ℝ → (Fin d → ℝ)} {u v M : ℝ}
       (hx : ContinuousOn x (Icc u v))
       (hxd : ∀ t ∈ Ioo u v, HasDerivAt x (f (x t)) t)
       (hB : ∀ t ∈ Icc u v, x t ∈ B)
       (hinward : ∀ z ∈ B, ∀ i ∈ s,
         dot (a i) z + c i = s.inf' hs (fun j => dot (a j) z + c j) →
         0 ≤ dot (a i) (f z))
       (hceiling : ∀ z ∈ B, s.inf' hs (fun i => dot (a i) z + c i) ≤ M)
   …

   Mentions: OAI.Problem326.dot

5. theorem OAI.Problem326.IsForwardSolutionOn.affineMinimum_eq line 75

   Source documentation

   Exact finite-forward-solution specialization of affine plateau preservation.

   theorem IsForwardSolutionOn.affineMinimum_eq
       {d : ℕ} {N : ReactionNetwork d} {κ : Reaction N → ℝ}
       {z : Fin d → ℝ} {T : ℝ} {x : ℝ → (Fin d → ℝ)}
       (hx : IsForwardSolutionOn N κ z T x)
       {ι : Type uIota} (s : Finset ι) (hs : s.Nonempty)
       (a : ι → (Fin d → ℝ)) (c : ι → ℝ) (B : Set (Fin d → ℝ)) {M : ℝ}
       (hB : ∀ t ∈ Icc 0 T, x t ∈ B)
       (hinward : ∀ y ∈ B, ∀ i ∈ s,
         dot (a i) y + c i = s.inf' hs (fun j => dot (a j) y + c j) →
         0 ≤ dot (a i) (massAction N κ y))
       (hceiling : ∀ y ∈ B, s.inf' hs (fun i => dot (a i) y + c i) ≤ M)
       (hstart : s.inf' hs (fun i => dot (a i) z + c i) = M) :
   …

   Mentions: OAI.Problem326.ReactionNetwork, OAI.Problem326.Reaction, OAI.Problem326.IsForwardSolutionOn, OAI.Problem326.dot, OAI.Problem326.massAction

6. theorem OAI.Problem326.affineMinimum_trapped line 95

   Source documentation

   A finite affine plateau traps any solution segment, without an a priori assumption that the segment stays in the region. The first-boundary argument uses the active inward estimate only inside the closed region.

   theorem affineMinimum_trapped
       {d : ℕ} {ι : Type uIota} (s : Finset ι) (hs : s.Nonempty)
       (a : ι → (Fin d → ℝ)) (c : ι → ℝ)
       (f : (Fin d → ℝ) → (Fin d → ℝ)) (B : Set (Fin d → ℝ))
       {x : ℝ → (Fin d → ℝ)} {T M : ℝ}
       (hT : 0 ≤ T) (hclosed : IsClosed B)
       (hx : ContinuousOn x (Icc 0 T))
       (hxd : ∀ t ∈ Ioo 0 T, HasDerivAt x (f (x t)) t)
       (hx0 : x 0 ∈ interior B)
       (hinward : ∀ z ∈ B, ∀ i ∈ s,
         dot (a i) z + c i = s.inf' hs (fun j => dot (a j) z + c j) →
         0 ≤ dot (a i) (f z))
   …

   Mentions: OAI.Problem326.dot

7. theorem OAI.Problem326.IsForwardSolutionOn.affineMinimum_trapped line 126

   Source documentation

   Exact mass-action specialization of the finite-interval trapping theorem.

   theorem IsForwardSolutionOn.affineMinimum_trapped
       {d : ℕ} {N : ReactionNetwork d} {κ : Reaction N → ℝ}
       {z : Fin d → ℝ} {T : ℝ} {x : ℝ → (Fin d → ℝ)}
       (hx : IsForwardSolutionOn N κ z T x)
       {ι : Type uIota} (s : Finset ι) (hs : s.Nonempty)
       (a : ι → (Fin d → ℝ)) (c : ι → ℝ) (B : Set (Fin d → ℝ)) {M : ℝ}
       (hT : 0 ≤ T) (hclosed : IsClosed B) (hz : z ∈ interior B)
       (hinward : ∀ y ∈ B, ∀ i ∈ s,
         dot (a i) y + c i = s.inf' hs (fun j => dot (a j) y + c j) →
         0 ≤ dot (a i) (massAction N κ y))
       (hceiling : ∀ y ∈ B, s.inf' hs (fun i => dot (a i) y + c i) ≤ M)
       (hstart : s.inf' hs (fun i => dot (a i) z + c i) = M)
   …

   Mentions: OAI.Problem326.ReactionNetwork, OAI.Problem326.Reaction, OAI.Problem326.IsForwardSolutionOn, OAI.Problem326.dot, OAI.Problem326.massAction