OAI/Dynamics/ThreeTorus/TensorPackets.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Good-arc cutoffs, scalar and tensor packet constructors, fiber insertion, and initial dense tests.

  1. lemma OAI.ThreeTorus.sharp_cutoff_integral_bound line 14
  2. theorem OAI.ThreeTorus.exists_sharp_arc_cutoff line 50

    Source documentation

    Smooth compact arc cutoffs with arbitrarily small excess over the ACTUAL complement length. The standard neutral 4δ estimate is not sharp enough here.

    theorem exists_sharp_arc_cutoff {δ t : ℝ} (hδ : 0 ≤ δ) (ht : 0 < t)
    (hu : δ+t < 1/2) :
    ∃ χ : ℝ → ℝ, ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) χ ∧ HasCompactSupport χ ∧
      tsupport χ ⊆ Ioo δ (1-δ) ∧ (∀ x, 0 ≤ χ x ∧ χ x ≤ 1) ∧
      (∀ x ∈ Icc (δ+t) (1-δ-t), χ x = 1) ∧
      (∫ x in Ioo (0:ℝ) 1, (1-χ x)^2) ≤ 2*δ+2*t := by
…
  3. lemma OAI.ThreeTorus.circle_cutoff_squared_error line 73
  4. lemma OAI.ThreeTorus.cylinderTorusCutoff_scalar line 98
  5. theorem OAI.ThreeTorus.exists_scalar_cutoff_packets line 107

    Source documentation

    A common scalar good-arc cutoff produces literal smooth input packets; all data are fixed before any passage integer is chosen.

    theorem exists_scalar_cutoff_packets {ι : Type*}
    (m : ι → ℤ) (hm : ∀ i, m i ≠ 0)
    (C : ι → UnitAddCircle × UnitAddCircle → ℂ)
    (hCc : ∀ i, Continuous (C i))
    (hCs : ∀ i, ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (fun p : ℝ × ℝ => C i (p.1,p.2)))
    {χ : ℝ → ℝ} (hχs : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) χ)
    (hχc : HasCompactSupport χ) {δ : ℝ} (hδ : 0 ≤ δ) (hd : δ < 1/2)
    (hχI : tsupport χ ⊆ Ioo δ (1-δ))
    (V : ℝ → ℝ) (hVp : Periodic V 1)
    (hVs : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) V)
    (hVd : ∀ x ∈ Ioo δ (1-δ), 0 < deriv V x) :
    ∃ F : PassagePackets ι, F.m=m ∧ F.V=V ∧ F.GoodArc δ ∧
…

    Mentions: OAI.ThreeTorus.PassagePackets

  6. lemma OAI.ThreeTorus.scalar_packets_reflection line 139
  7. lemma OAI.ThreeTorus.tensor_filter_reflection line 162
  8. lemma OAI.ThreeTorus.tensorAngular_reflection line 169
  9. lemma OAI.ThreeTorus.tensorMiddle_reflection line 172
  10. lemma OAI.ThreeTorus.tensorLast_reflection line 175
  11. def OAI.ThreeTorus.tensorSupportNeg line 179
  12. lemma OAI.ThreeTorus.tensorSupportNeg_involutive line 184
  13. theorem OAI.ThreeTorus.exists_rotated_tensor_packets line 189

    Source documentation

    Literal smooth packets of a finite tensor polynomial after a cyclic coordinate change. The unused old coordinate is not silently discarded.

    theorem exists_rotated_tensor_packets (c : TensorIndex →₀ ℂ)
    (hc : ∀ k, c (-k)=conj (c k)) (a b d : Fin 3)
    (hn : ∀ k ∈ c.support, k a ≠ 0)
    {χ : ℝ → ℝ} (hχs : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) χ)
    (hχc : HasCompactSupport χ) {δ : ℝ} (hδ : 0 ≤ δ) (hd : δ < 1/2)
    (hχI : tsupport χ ⊆ Ioo δ (1-δ))
    (V : ℝ → ℝ) (hVp : Periodic V 1)
    (hVs : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) V)
    (hVd : ∀ x ∈ Ioo δ (1-δ), 0 < deriv V x) :
    ∃ F : PassagePackets ↥c.support, F.V=V ∧ F.GoodArc δ ∧
      F.Reflection (tensorSupportNeg hc) ∧
      (∀ k, F.m k=k.val a) ∧
…

    Mentions: OAI.ThreeTorus.TensorIndex, OAI.ThreeTorus.PassagePackets, OAI.ThreeTorus.tensorSupportNeg

  14. lemma OAI.ThreeTorus.tensorPolynomial_add line 236
  15. lemma OAI.ThreeTorus.tensorPolynomial_filter line 242
  16. lemma OAI.ThreeTorus.tensorCharacter_angular_integral line 251
  17. lemma OAI.ThreeTorus.tensorAngular_eq_remove_mean line 257
  18. lemma OAI.ThreeTorus.tensorAngular_fiber_energy_le line 281
  19. lemma OAI.ThreeTorus.tensorAngular_cutoff_energy line 298

    Source documentation

    Exact constant-one angular cutoff bound; it is the actual lost arc length, not four times that length, which appears in the preparation error.

    lemma tensorAngular_cutoff_energy (c : TensorIndex →₀ ℂ) {B : ℝ} (hB : 0 ≤ B)
    (hc : ∀ x, ‖tensorPolynomial c x‖ ≤ B) {χ : UnitAddCircle → ℝ} (hχ : Continuous χ) :
    (∫ x : TripleTorus, ‖tensorPolynomial (tensorAngular c) x-
      (χ x.2.1:ℂ)*tensorPolynomial (tensorAngular c) x‖^2 ∂tripleVolume) ≤
      B^2 * ∫ u, (1-χ u)^2 ∂phaseHaar := by
…

    Mentions: OAI.ThreeTorus.TensorIndex, OAI.ThreeTorus.tensorPolynomial, OAI.ThreeTorus.TripleTorus, OAI.ThreeTorus.tensorAngular, OAI.ThreeTorus.tripleVolume, OAI.ThreeTorus.phaseHaar

  20. lemma OAI.ThreeTorus.neutralCircleCutoff_squared_error line 340
  21. lemma OAI.ThreeTorus.uniform_slow_cutoff_energy line 353
  22. lemma OAI.ThreeTorus.tensorMiddle_coords line 381
  23. lemma OAI.ThreeTorus.tensorLast_coords line 397
  24. def OAI.ThreeTorus.rotatedTensor line 422
  25. def OAI.ThreeTorus.tensorBudget line 424
  26. lemma OAI.ThreeTorus.tensorBudget_nonneg line 425
  27. lemma OAI.ThreeTorus.rotatedTensor_continuous line 427
  28. lemma OAI.ThreeTorus.rotatedTensor_norm_le line 433
  29. lemma OAI.ThreeTorus.exists_tensor_cutoff_family line 438
  30. lemma OAI.ThreeTorus.tensorAngular_nonzero line 459
  31. lemma OAI.ThreeTorus.tensorMiddle_nonzero line 464
  32. lemma OAI.ThreeTorus.tensor_split_vector line 471
  33. lemma OAI.ThreeTorus.continuous_triple_memLp line 490
  34. lemma OAI.ThreeTorus.exists_cutoff_loss_budget line 493
  35. theorem OAI.ThreeTorus.exists_two_slow_insertions line 507

    Source documentation

    Two literal neutral passages convert both retained slow Fourier components into nonzero angular packets. The F list alone is kept orthogonal. All objects, cutoffs and bounds are fixed before their respective passage integer choices.

    theorem exists_two_slow_insertions (F H : RealPacketFamily) (hmi : Injective F.data.m)
    {δ : ℝ} (hδ : 0 ≤ δ) (hgF : F.data.GoodArc δ) (hgH : H.data.GoodArc δ) (hV : H.data.V=F.data.V)
    (c : TensorIndex →₀ ℂ) (hc0 : c 0=0) (hcr : ∀ k, c (-k)=conj (c k))
    (Q : PhysicalJetData) (frame : PhysicalFrame)
    {ε κ ζ : ℝ} (hε : 0 < ε) (hκ : 0 < κ) (hζ : 0 < ζ) :
    ∃ F' H' : RealPacketFamily, ∃ α : Equiv.Perm TripleTorus, ∃ frame' : PhysicalFrame,
      Continuous α ∧ MeasurePreserving α tripleVolume tripleVolume ∧
      frame'.chart=frame.chart.trans α ∧ H'.data.V=F'.data.V ∧ Injective F'.data.m ∧
      (∃ δ' : ℝ, 0 < δ' ∧ δ' < 1/8 ∧ δ' < κ ∧ F'.data.GoodArc δ' ∧ H'.data.GoodArc δ') ∧
      Q.Close ζ frame F.data.V frame' F'.data.V ∧
      physicalDist F.vector (F'.vector ∘ α) < ε ∧
      physicalDist (fun x => H.vector x+tensorPolynomial (tensorMiddle c) x+tensorPolynomial (tensorLast c) x)
…

    Mentions: OAI.ThreeTorus.H, OAI.ThreeTorus.RealPacketFamily, OAI.ThreeTorus.TensorIndex, OAI.ThreeTorus.PhysicalJetData, OAI.ThreeTorus.PhysicalFrame, OAI.ThreeTorus.TripleTorus, OAI.ThreeTorus.tripleVolume, OAI.ThreeTorus.physicalDist, OAI.ThreeTorus.tensorPolynomial, OAI.ThreeTorus.tensorMiddle, OAI.ThreeTorus.tensorLast

  36. lemma OAI.ThreeTorus.physicalDist_le_of_uniform line 604
  37. lemma OAI.ThreeTorus.small_angular_loss line 616
  38. theorem OAI.ThreeTorus.exists_initial_tensor_test line 636

    Source documentation

    The INITIAL cutoff costs the exact old complement square root. Both slow components are retained as the very same finite real tensor polynomial.

    theorem exists_initial_tensor_test {h : TripleTorus → ℂ} (hh : Continuous h)
    (hr : ∀ x, conj (h x)=h x) (hc : ∫ x, h x ∂tripleVolume=0) (hb : ∀ x, ‖h x‖ ≤ 1)
    {δ : ℝ} (hδ : 0 ≤ δ) (hd : δ < 1/2)
    (V : ℝ → ℝ) (hp : Periodic V 1) (hs : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) V)
    (hv : ∀ x ∈ Ioo δ (1-δ), 0 < deriv V x)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ c : TensorIndex →₀ ℂ, c 0=0 ∧ (∀ k, c (-k)=conj (c k)) ∧
      ∃ H : RealPacketFamily, H.data.V=V ∧ H.data.GoodArc δ ∧
      physicalDist h (fun x => H.vector x+tensorPolynomial (tensorMiddle c) x+tensorPolynomial (tensorLast c) x)
        < Real.sqrt (2*δ)+ε := by
…

    Mentions: OAI.ThreeTorus.TripleTorus, OAI.ThreeTorus.tripleVolume, OAI.ThreeTorus.TensorIndex, OAI.ThreeTorus.H, OAI.ThreeTorus.RealPacketFamily, OAI.ThreeTorus.physicalDist, OAI.ThreeTorus.tensorPolynomial, OAI.ThreeTorus.tensorMiddle, OAI.ThreeTorus.tensorLast