SectionWeightedBoxes.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform weighted-box comparison in ideal section coordinates

theorem OAI.PolycyclicRecognition.exponentialRescaleBasis_reindex line 12

theorem OAI.PolycyclicRecognition.basisWithQuotientLifts_rescale line 26

Source documentation

Only ideal coordinates are rescaled; the quotient lifts have zero width.

theorem basisWithQuotientLifts_rescale (cost : I → ℝ) (r : ℝ) :
    basisWithQuotientLifts U.toSubmodule (exponentialRescaleBasis bI cost r) bQ lift hlift =
      exponentialRescaleBasis (basisWithQuotientLifts U.toSubmodule bI bQ lift hlift)
        (Sum.elim cost (fun _ => 0)) r := by
…

Mentions: OAI.PolycyclicRecognition.basisWithQuotientLifts, OAI.PolycyclicRecognition.exponentialRescaleBasis

theorem OAI.PolycyclicRecognition.weighted_section_box_factorization line 57

Source documentation

A full weighted box has bounded quotient logarithm and polynomially bounded ideal coordinate, with a constant uniform in the height scale.

theorem weighted_section_box_factorization
    (hbr : ∀ r : ℝ, 0 ≤ r → ∀ i j k, |(Br r).repr ⁅Br r i, Br r j⁆ k| ≤ C)
    (r R : ℝ) (hr : 0 ≤ r) (hR : 0 ≤ R) {n : N}
    (hn : n ∈ exponentialCoordinateBox ExpN (Br r) R) :
    ∃ (u : U) (q : V ⧸ U.toSubmodule),
      n = ExpN (u : V) * ExpN (quotientLinearSection U bQ lift q) ∧
      ‖(exponentialRescaleBasis bI cost r).equivFun u‖ ≤ K * (1 + R) ^ c ∧
      ‖bQ.equivFun q‖ ≤ R := by
…

Mentions: OAI.PolycyclicRecognition.exponentialCoordinateBox, OAI.PolycyclicRecognition.quotientLinearSection, OAI.PolycyclicRecognition.exponentialRescaleBasis

theorem OAI.PolycyclicRecognition.weighted_section_box_product line 83

Source documentation

Conversely, the product of a weighted ideal box and a bounded pure quotient section lies in the full box with one uniform polynomial loss.

theorem weighted_section_box_product
    (hbr : ∀ r : ℝ, 0 ≤ r → ∀ i j k, |(Br r).repr ⁅Br r i, Br r j⁆ k| ≤ C)
    (r R : ℝ) (hr : 0 ≤ r) (hR : 0 ≤ R)
    (u : U) (q : V ⧸ U.toSubmodule)
    (hu : ‖(exponentialRescaleBasis bI cost r).equivFun u‖ ≤ R)
    (hq : ‖bQ.equivFun q‖ ≤ R) :
    ExpN (u : V) * ExpN (quotientLinearSection U bQ lift q) ∈
      exponentialCoordinateBox ExpN (Br r) (K * (1 + R) ^ c) := by
…

Mentions: OAI.PolycyclicRecognition.exponentialRescaleBasis, OAI.PolycyclicRecognition.quotientLinearSection, OAI.PolycyclicRecognition.exponentialCoordinateBox