Topological producer for a genuine minus first crossing #
The crossing is the least point of the nonempty compact set on which the
normalized minus slope reaches c.
theorem
Section10MinusFirstCrossingProducer.normalizedMinusBase_continuousAt
{R : ℝ → ℝ}
{β s : ℝ}
(h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β)
(hβs : β < s)
:
The normalized minus base is continuous at every point strictly to the right of the apparatus threshold.
theorem
Section10MinusFirstCrossingProducer.minusFirstCrossing_of_reaches
{R : ℝ → ℝ}
{β c S v : ℝ}
(h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β)
(hβS : β < S)
(hβoneS : β + 1 ≤ S)
(hinitial : ∀ u ∈ Set.Icc β S, Section10Lemma1028FirstCrossing.normalizedMinusBase R Section10CanonicalXi.xi u < c)
(hSv : S ≤ v)
(hv : c ≤ Section10Lemma1028FirstCrossing.normalizedMinusBase R Section10CanonicalXi.xi v)
:
∃ (w : Section10Equation1053MinusFirstCrossing.MinusFirstCrossing R Section10CanonicalXi.xi c β S), S ≤ w.s
If the normalized base starts strictly below c and reaches c by v,
the least point of the closed crossing set is a genuine first crossing.
hDDEβ is the endpoint derivative required literally by the current
MinusFirstCrossing.hasDeriv field. The apparatus itself supplies the DDE only
for β < u, so this one endpoint cannot be inferred from that interface.
theorem
Section10MinusFirstCrossingProducer.producesMinusFirstCrossing
{R : ℝ → ℝ}
{β c S : ℝ}
(h : Section10Lemma1028FirstCrossing.FirstCrossingDDEApparatus R β)
(hβS : β < S)
(hβoneS : β + 1 ≤ S)
(hinitial : ∀ u ∈ Set.Icc β S, Section10Lemma1028FirstCrossing.normalizedMinusBase R Section10CanonicalXi.xi u < c)
(v : ℝ)
:
S ≤ v →
c ≤ Section10Lemma1028FirstCrossing.normalizedMinusBase R Section10CanonicalXi.xi v →
∃ (w : Section10Equation1053MinusFirstCrossing.MinusFirstCrossing R Section10CanonicalXi.xi c β S), S ≤ w.s
Pointwise crossing production, in the exact shape consumed by
ProducesMinusFirstCrossing after unfolding that definition.