The rounds on the nonmonomial part are indifferent to empty boundary members #
The counterpart, for boundary members, of the empty blow-up convention [Kol07, 32], for the value of
the rounds on the nonmonomial part: when
the nonempty members of E are the members of F' along an order embedding e : F'.ι ↪o E.ι
(matched members, the others empty), the value on every relatively compact open for (M, 𝓘, E) is
its value for (M, 𝓘, F') (stepAFamOn_indiff, packaged as
stepAFunctor_indifferentToEmptyMembers, the shape of
AnalyticFamilyFunctor.IndifferentToEmptyMembers).
The proof follows the descent link by link: the two descents run along the same canonical chain
from the same bound, since the round order does not see empty members (roundOrderOn_withBoundary,
from nonmonomialPart_eq_of_isEmptyExtension), and two states with the same list link to the same
list (BState.descentLink_L_indiff): the restricted triples over the open are again related by a
boundary change along e, and the value of the round is the value of the functor
nonmonomialFunctor (bo d) at the induced triples, which is indifferent to empty members along the
index correspondence of the induced boundaries
(AnalyticFamilyFunctor.IndifferentToEmptyMembers.seqOn_induced_indiff, stated for an arbitrary
family functor). The final values are read with the bound as an explicit parameter (valueAt,
StepACompat.lean), so that the equal bounds are identified by a substitution (valueAt_congr).
A functor indifferent to empty members is indifferent at the induced triples #
Indifference to empty boundary members along a list: a family functor indifferent to empty
members takes the same value at the induced triples of T and of T with its boundary replaced by
F' along the same list L, the induced boundaries being matched along the index correspondence
corrIdx e (hyp_corrIdxAux_of_forall, hyp_eq_empty_of_notMem_range_corrIdx); the counterpart,
for boundary members, of [Kol07, 32].
The bound does not see empty members #
The nonmonomial part of the boundary change is the nonmonomial part
(nonmonomialPart_eq_of_isEmptyExtension), read on the triples.
The round order (roundOrderOn, the maximum of ord N(𝓘) on the closure of an open) does not
see empty members.
One link is indifferent to empty members #
One link of the descent is indifferent to empty members: two states with the same list, for
T and for the boundary change, link to the same list. The restricted triples over the open are
again related by a boundary change along e (AnalyticTriple.ext'), and the value of the round is
the value of the functor at the induced triples (seqOn_induced_indiff with
nonmonomialFunctor_indifferentToEmptyMembers).
The descent along the same chain from the same bound #
The two descents along the same chain from the same bound have the same lists, link by link
(descentLink_L_indiff; both initial states have the empty list).
The value with the bound as a parameter #
The value along the same chain from the same bound is indifferent to empty members
(descentStateAux_L_indiff).
Indifference of the value of the rounds #
The value of the rounds is indifferent to empty boundary members (the counterpart, for
boundary members, of [Kol07, 32]): the canonical
chain does not see the boundary, the canonical bound does not see empty members
(roundOrderOn_withBoundary), and the two descents along that chain from that bound have the same
lists (valueAt_indiff).
The family functor of the rounds is indifferent to empty boundary members (the counterpart, for boundary members, of [Kol07, 32]).