OAI/Dynamics/ThreeTorus/SymmetricPackets.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Reflected neutral and signal producers, symmetric colors, physical control, and grouped cutoffs.

  1. lemma OAI.ThreeTorus.retainedRealAmplitude_reflect line 16
  2. def OAI.ThreeTorus.reflectedOutputIndex line 24
  3. lemma OAI.ThreeTorus.literal_output_reflection line 28
  4. lemma OAI.ThreeTorus.scalar_exact_indices_reflect line 58
  5. theorem OAI.ThreeTorus.eventually_neutral_anchor_reflected_family line 79
  6. theorem OAI.ThreeTorus.exists_neutral_reflected_tracked_family line 280
  7. theorem OAI.ThreeTorus.exists_signal_state_reflected_family line 385
  8. theorem OAI.ThreeTorus.exists_signal_reflected_tracked_family line 612
  9. theorem OAI.ThreeTorus.exists_neutral_reflected_geometry_state line 724
  10. theorem OAI.ThreeTorus.exists_signal_reflected_geometry_state line 754
  11. theorem OAI.ThreeTorus.exists_refresh_transmit_reflected_state line 811

    Source documentation

    Actual refresh/transmit state, with the exact positive strength fixed before all data and error budgets. Each input packet can carry its original color's continuous coefficient; finite color grouping is by summation.

    theorem exists_refresh_transmit_reflected_state
    {b D : ℝ} (hb : 0 < b) (hbD : b < D)
    {d : ℝ → ℂ} (hd : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) d)
    (hdc : HasCompactSupport d) (hdr : ∀ v, d (-v) = starRingEnd ℂ (d v))
    (hd0 : d 0 = 0) (hds : support d ⊆ Icc (-D) D) :
    ∃ L : ℕ, ∃ γ₀ : ℝ, 2 ≤ L ∧ D/b < L ∧ 0 < γ₀ ∧
      ∀ γ : ℝ, 0 < γ → γ ≤ γ₀ →
      (∀ v, 2*γ*‖d v‖ ≤ 1/2) ∧
      ∀ (ι : Type u) [Fintype ι], ∀ (F : PassagePackets ι),
      Injective F.m → F.SpareIndependent → ∀ τref : ι → ι, F.Reflection τref → ∀ B : ℝ, 0 < B →
      ∀ margin : ℝ, 0 < margin →
      (∀ i, b+margin ≤ |(F.m i:ℝ)/B| ∧ |(F.m i:ℝ)/B| ≤ D-margin) →
…

    Mentions: OAI.ThreeTorus.PassagePackets

  12. def OAI.ThreeTorus.ColoredState.Reflection line 959
  13. lemma OAI.ThreeTorus.ColoredState.Reflection.density line 963
  14. theorem OAI.ThreeTorus.exists_colored_reflected_signal line 982

    Source documentation

    Symmetric actual refresh--signal pairs, retaining the complete good arc with arbitrarily small excluded measure.

    theorem exists_colored_reflected_signal {b D : ℝ} (hb : 0 < b) (hbD : b < D)
    {d : ℝ → ℂ} (hd : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) d)
    (hdc : HasCompactSupport d) (hdr : ∀ v, d (-v) = starRingEnd ℂ (d v))
    (hd0 : d 0 = 0) (hds : support d ⊆ Icc (-D) D) :
    ∃ L : ℕ, ∃ γ₀ : ℝ, 2 ≤ L ∧ D/b < L ∧ 0 < γ₀ ∧
      ∀ γ : ℝ, 0 < γ → γ ≤ γ₀ →
      (∀ v, 2*γ*‖d v‖ ≤ 1/2) ∧
      ∀ (R : Type) [DecidableEq R], ∀ (C : ColoredState R),
      ∀ τR : R → R, C.Reflection τR →
      ∀ margin : ℝ, 0 < margin → C.InBand b D margin →
      ∀ (a : R → UnitAddCircle → ℂ), (∀ r, Continuous (a r)) →
      ∀ ω : ℝ, 0 ≤ ω → C.Matches d a ω →
…

    Mentions: OAI.ThreeTorus.ColoredState

  15. structure OAI.ThreeTorus.PhysicalJetData line 1041
  16. def OAI.ThreeTorus.PhysicalJetData.Close line 1050
  17. lemma OAI.ThreeTorus.PhysicalJetData.close_refl line 1056
  18. lemma OAI.ThreeTorus.PhysicalJetData.Close.mono line 1059
  19. lemma OAI.ThreeTorus.PhysicalJetData.Close.trans line 1063
  20. lemma OAI.ThreeTorus.PhysicalJetData.eventually_next line 1069
  21. def OAI.ThreeTorus.ColoredPair.nextFrame line 1093
  22. lemma OAI.ThreeTorus.ColoredPair.nextFrame_chart line 1096
  23. theorem OAI.ThreeTorus.exists_general_neutral line 1119

    Source documentation

    Generic actual neutral output. It intentionally does not assert injectivity of the new modes: the first support separation does not give it.

    theorem exists_general_neutral {ι : Type*} [Fintype ι]
    (F : PassagePackets ι) {c : ℕ} (hc : 0 < c)
    (h0 : ∀ x : ℝ, (c:ℝ)+F.V x ≠ 0)
    (χ : ι → ℝ → UnitAddCircle → ℝ)
    (hχs : ∀ i, CylinderSmooth (χ i).uncurry)
    (hχc : ∀ i, HasCompactSupport (χ i).uncurry)
    (hχ0 : ∀ i a, χ i 0 a = 0)
    (hχb : ∀ i s a, 0 ≤ χ i s a ∧ χ i s a ≤ 1)
    (hχW : ∀ i (C : Set ℝ) a s, stationaryWeight C
      (fun x => (F.m i:ℝ)*((c:ℝ)+F.V x)) (F.A₀ i a) s ≠ 0 → χ i s a = 1)
    {ε κ : ℝ} (hε : 0 < ε) (hκ : 0 < κ) :
    ∃ δ : ℝ, ∃ cut : LawCutoffs δ, ∃ L : ℝ, ∃ g : PassageGeometryFamily F.V,
…

    Mentions: OAI.ThreeTorus.PassagePackets, OAI.ThreeTorus.CylinderSmooth, OAI.ThreeTorus.stationaryWeight, OAI.ThreeTorus.LawCutoffs, OAI.ThreeTorus.PassageGeometryFamily

  24. structure OAI.ThreeTorus.NeutralStep line 1277
  25. def OAI.ThreeTorus.NeutralStep.chart line 1304
  26. def OAI.ThreeTorus.NeutralStep.nextFrame line 1305
  27. lemma OAI.ThreeTorus.NeutralStep.nextFrame_chart line 1308
  28. lemma OAI.ThreeTorus.NeutralStep.nonzero line 1311
  29. lemma OAI.ThreeTorus.NeutralStep.reflection line 1314
  30. theorem OAI.ThreeTorus.exists_controlled_neutral line 1340

    Source documentation

    Finite physical restrictions are imposed only after the coefficients, cutoffs, carrier, broad jitter and its rounding sequence have all been fixed.

    theorem exists_controlled_neutral {ι : Type*} [Fintype ι]
    (F : PassagePackets ι) {c : ℕ} (hc : 0 < c)
    (h0 : ∀ x : ℝ, (c:ℝ)+F.V x ≠ 0)
    (χ : ι → ℝ → UnitAddCircle → ℝ)
    (hχs : ∀ i, CylinderSmooth (χ i).uncurry)
    (hχc : ∀ i, HasCompactSupport (χ i).uncurry)
    (hχ0 : ∀ i a, χ i 0 a = 0)
    (hχb : ∀ i x a, 0 ≤ χ i x a ∧ χ i x a ≤ 1)
    (hχW : ∀ i (C : Set ℝ) a x, stationaryWeight C
      (fun t => (F.m i:ℝ)*((c:ℝ)+F.V t)) (F.A₀ i a) x ≠ 0 → χ i x a = 1)
    (Q : PhysicalJetData) (frame : PhysicalFrame)
    {ε κ ζ : ℝ} (hε : 0 < ε) (hκ : 0 < κ) (hζ : 0 < ζ) :
…

    Mentions: OAI.ThreeTorus.PassagePackets, OAI.ThreeTorus.CylinderSmooth, OAI.ThreeTorus.stationaryWeight, OAI.ThreeTorus.PhysicalJetData, OAI.ThreeTorus.PhysicalFrame

  31. theorem OAI.ThreeTorus.exists_controlled_neutral_eventually line 1385

    Source documentation

    An arbitrary cofinal restriction may be imposed on the LAST integer. No passage or smooth producer is assumed by this restriction.

    theorem exists_controlled_neutral_eventually {ι : Type*} [Fintype ι]
    (F : PassagePackets ι) {c : ℕ} (hc : 0 < c)
    (h0 : ∀ x : ℝ, (c:ℝ)+F.V x ≠ 0)
    (χ : ι → ℝ → UnitAddCircle → ℝ)
    (hχs : ∀ i, CylinderSmooth (χ i).uncurry)
    (hχc : ∀ i, HasCompactSupport (χ i).uncurry)
    (hχ0 : ∀ i a, χ i 0 a = 0)
    (hχb : ∀ i x a, 0 ≤ χ i x a ∧ χ i x a ≤ 1)
    (hχW : ∀ i (C : Set ℝ) a x, stationaryWeight C
      (fun t => (F.m i:ℝ)*((c:ℝ)+F.V t)) (F.A₀ i a) x ≠ 0 → χ i x a = 1)
    (Q : PhysicalJetData) (frame : PhysicalFrame)
    (P : ℕ → Prop) (hP : ∀ᶠ n : ℕ in atTop, P n)
…

    Mentions: OAI.ThreeTorus.PassagePackets, OAI.ThreeTorus.CylinderSmooth, OAI.ThreeTorus.stationaryWeight, OAI.ThreeTorus.PhysicalJetData, OAI.ThreeTorus.PhysicalFrame

  32. lemma OAI.ThreeTorus.compact_cylinder_gap line 1419
  33. lemma OAI.ThreeTorus.eventually_retained_indices_large line 1436
  34. theorem OAI.ThreeTorus.mode_grouped_neutral_cutoffs line 1466

    Source documentation

    The simultaneous-list version of neutral cutoffs: repeated occurrences of one angular mode share exactly the same cutoff, whereas different modes have disjoint retained sets. In particular F and H are not falsely declared orthogonal to one another.

    theorem mode_grouped_neutral_cutoffs {ι : Type*} [Fintype ι]
    (F : PassagePackets ι) (τ : ι → ι) (_hτ : Involutive τ) (hr : F.Reflection τ) :
    ∃ c : ℕ, 0 < c ∧ (∀ x : ℝ, (c:ℝ)+F.V x ≠ 0) ∧
      ∃ χ : ι → ℝ → UnitAddCircle → ℝ,
        (∀ i, CylinderSmooth (χ i).uncurry ∧ HasCompactSupport (χ i).uncurry ∧
          tsupport (χ i).uncurry ⊆ {p | p.1 ≠ 0} ∧
          (∀ s a, 0 ≤ χ i s a ∧ χ i s a ≤ 1) ∧
          ∀ (C : Set ℝ) a s, stationaryWeight C
            (fun x => (F.m i:ℝ)*((c:ℝ)+F.V x)) (F.A₀ i a) s ≠ 0 → χ i s a = 1) ∧
        (∀ i j, F.m i ≠ F.m j → Disjoint (tsupport (χ i).uncurry) (tsupport (χ j).uncurry)) ∧
        (∀ i j, F.m i = F.m j → χ i = χ j) ∧
        (∀ i s a, χ (τ i) s a = χ i (-s) a) := by
…

    Mentions: OAI.ThreeTorus.PassagePackets, OAI.ThreeTorus.CylinderSmooth, OAI.ThreeTorus.stationaryWeight

  35. theorem OAI.ThreeTorus.scalar_grouped_neutral_cutoffs line 1570

    Source documentation

    A repeated-mode neutral cutoff, independent of the spare coordinate. Separation is in scalar frequency, not just on the cylinder.

    theorem scalar_grouped_neutral_cutoffs {ι : Type*} [Fintype ι]
    (F : PassagePackets ι) {τ : ι → ι} (hr : F.Reflection τ) :
    ∃ c : ℕ, 0 < c ∧ (∀ x : ℝ, (c:ℝ)+F.V x ≠ 0) ∧
      ∃ χ : ι → ℝ → ℝ,
        (∀ i, ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (χ i) ∧ HasCompactSupport (χ i) ∧
          χ i 0=0 ∧ (∀ s, 0 ≤ χ i s ∧ χ i s ≤ 1) ∧
          ∀ (C : Set ℝ) a s, stationaryWeight C
            (fun x => (F.m i:ℝ)*((c:ℝ)+F.V x)) (F.A₀ i a) s ≠ 0 → χ i s=1) ∧
        (∀ i j, F.m i ≠ F.m j → Disjoint (tsupport (χ i)) (tsupport (χ j))) ∧
        (∀ i j, F.m i=F.m j → χ i=χ j) ∧
        ∀ i s, χ (τ i) s=χ i (-s) := by
…

    Mentions: OAI.ThreeTorus.PassagePackets, OAI.ThreeTorus.stationaryWeight