Documentation

LeanPool.LanguageGeneration.FiniteWitness.Width.Divergence

Witness-size divergence in the two-core family #

source
noncomputable def GenLimit.FiniteWitness.TwoCore.rightPart (S : Finset Point) :
Finset ℕ

The natural-number indices of the right-copy elements in a sample.

Equations
Instances For
    source
    noncomputable def GenLimit.FiniteWitness.TwoCore.leftPart (S : Finset Point) :
    Finset ℕ

    The natural-number indices of the left-copy elements in a sample.

    Equations
    Instances For
      source
      @[simp]
      theorem GenLimit.FiniteWitness.TwoCore.mem_rightPart (S : Finset Point) (n : ℕ) :
      n ∈ rightPart S ↔ Sum.inr n ∈ S
      source
      @[simp]
      theorem GenLimit.FiniteWitness.TwoCore.mem_leftPart (S : Finset Point) (n : ℕ) :
      n ∈ leftPart S ↔ Sum.inl n ∈ S
      source
      def GenLimit.FiniteWitness.TwoCore.rightChain (n : ℕ) :
      Set Point

      A full right copy together with the first n points of the left copy.

      Equations
      Instances For
        source
        def GenLimit.FiniteWitness.TwoCore.leftChain (n : ℕ) :
        Set Point

        A full left copy together with the first n points of the right copy.

        Equations
        Instances For
          source
          def GenLimit.FiniteWitness.TwoCore.leftCore (T : Set Point → Finset Point) (S : Finset Point) :
          Set ℕ

          The common right part of the active targets that contain the entire left copy.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem GenLimit.FiniteWitness.TwoCore.leftCore_infinite {T : Set Point → Finset Point} (hT : Valid family T) {S : Finset Point} {n : ℕ} (hK : rightChain n ∈ active family T S) :
            (leftCore T S).Infinite
            source
            theorem GenLimit.FiniteWitness.TwoCore.bounded_indices_finite {T : Set Point → Finset Point} (hT : Valid family T) (d : ℕ) :
            {n : ℕ | (rightPart (T (rightChain n))).card ≤ d}.Finite

            No infinite subsequence of this specified chain has bounded right-part witnesses.

            source
            theorem GenLimit.FiniteWitness.TwoCore.right_witness_divergence {T : Set Point → Finset Point} (hT : Valid family T) (d : ℕ) :
            ∃ (N : ℕ), ∀ n ≥ N, d ≤ (rightPart (T (rightChain n))).card
            source
            theorem GenLimit.FiniteWitness.TwoCore.right_witness_tendsto {T : Set Point → Finset Point} (hT : Valid family T) :
            Filter.Tendsto (fun (n : ℕ) => (rightPart (T (rightChain n))).card) Filter.atTop Filter.atTop
            source
            @[simp]
            theorem GenLimit.FiniteWitness.TwoCore.swap_family :
            transportClass (Equiv.sumComm ℕ ℕ) family = family
            source
            theorem GenLimit.FiniteWitness.TwoCore.swap_rightChain (n : ℕ) :
            ⇑(Equiv.sumComm ℕ ℕ) ⁻¹' rightChain n = leftChain n
            source
            theorem GenLimit.FiniteWitness.TwoCore.swap_rightPart (T : Set Point → Finset Point) (n : ℕ) :
            rightPart (transportAssignment (Equiv.sumComm ℕ ℕ) T (rightChain n)) = leftPart (T (leftChain n))
            source
            theorem GenLimit.FiniteWitness.TwoCore.left_witness_divergence {T : Set Point → Finset Point} (hT : Valid family T) (d : ℕ) :
            ∃ (N : ℕ), ∀ n ≥ N, d ≤ (leftPart (T (leftChain n))).card
            source
            theorem GenLimit.FiniteWitness.TwoCore.left_witness_tendsto {T : Set Point → Finset Point} (hT : Valid family T) :
            Filter.Tendsto (fun (n : ℕ) => (leftPart (T (leftChain n))).card) Filter.atTop Filter.atTop