Documentation

Anderson4D.DetParametrix.Paper41_Renorm.R322AnalyticActiveCarrierGeometry

Active carriers along the R-322 analytic schedule #

After a prefix of the inside-to-outside schedule has been collapsed, its concrete blocks have been deleted. This file identifies the next concrete block with the ambient endpoint interval restricted to that active carrier.

source
def Anderson4D.r322AnalyticActiveCarrier {m : ℕ} (pre : List (R322ExtractionStep m)) :
Finset (Fin m)

Ambient vertices which remain after deleting a schedule prefix.

Equations
Instances For
    source
    @[simp]
    theorem Anderson4D.r322AnalyticActiveCarrier_nil {m : ℕ} :
    r322AnalyticActiveCarrier [] = Finset.univ
    source
    theorem Anderson4D.mem_r322AnalyticActiveCarrier_iff {m : ℕ} (pre : List (R322ExtractionStep m)) (i : Fin m) :
    i ∈ r322AnalyticActiveCarrier pre ↔ ∀ s ∈ pre, i ∉ s.2

    Membership means avoiding every block already processed.

    source
    theorem Anderson4D.r322AnalyticActiveCarrier_append_subset {m : ℕ} (pre suffix : List (R322ExtractionStep m)) :
    r322AnalyticActiveCarrier (pre ++ suffix) ⊆ r322AnalyticActiveCarrier pre

    Processing more blocks can only shrink the active carrier.

    source
    @[simp]
    theorem Anderson4D.r322AnalyticActiveCarrier_append_singleton {m : ℕ} (pre : List (R322ExtractionStep m)) (step : R322ExtractionStep m) :
    r322AnalyticActiveCarrier (pre ++ [step]) = r322AnalyticActiveCarrier pre \ step.2

    The next carrier is obtained by deleting exactly the next block.

    source
    theorem Anderson4D.r322AnalyticSchedule_mem_prefix_of_right_lt {m : ℕ} (κ : PartialPairing (Fin m)) (pre suffix : List (R322ExtractionStep m)) (step earlier : R322ExtractionStep m) (hschedule : r322AnalyticSchedule κ = pre ++ step :: suffix) (hearlier : earlier ∈ r322AnalyticSchedule κ) (hright : earlier.1.2 < step.1.2) :
    earlier ∈ pre

    A scheduled step with smaller right endpoint lies in the displayed prefix, rather than at or after the current step.

    source
    theorem Anderson4D.r322AnalyticSchedule_prefixBlock_disjoint_step {m : ℕ} (κ : PartialPairing (Fin m)) (pre suffix : List (R322ExtractionStep m)) (step earlier : R322ExtractionStep m) (hschedule : r322AnalyticSchedule κ = pre ++ step :: suffix) (hearlier : earlier ∈ pre) :
    Disjoint earlier.2 step.2

    Every block in the displayed prefix is disjoint from the next block.

    source
    theorem Anderson4D.r322AnalyticSchedule_step_block_eq_activeCarrier_inter_Icc {m : ℕ} (κ : PartialPairing (Fin m)) (pre suffix : List (R322ExtractionStep m)) (step : R322ExtractionStep m) (hschedule : r322AnalyticSchedule κ = pre ++ step :: suffix) :
    step.2 = r322AnalyticActiveCarrier pre ∩ Finset.Icc step.1.1 step.1.2

    At any point of the analytic schedule, the next concrete block is the endpoint interval relative to the current active carrier.

    source
    theorem Anderson4D.r322AnalyticSchedule_step_endpoints_mem_activeCarrier {m : ℕ} (κ : PartialPairing (Fin m)) (pre suffix : List (R322ExtractionStep m)) (step : R322ExtractionStep m) (hschedule : r322AnalyticSchedule κ = pre ++ step :: suffix) :
    step.1.1 ∈ r322AnalyticActiveCarrier pre ∧ step.1.2 ∈ r322AnalyticActiveCarrier pre

    Both endpoints of the next step are still active.