WeightedHaarVolume.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Weighted ideal-box volumes in a chosen Haar normalization

theorem OAI.PolycyclicRecognition.det_exponentialRescaleBasis line 18
Source documentation
The basis rescaling contributes exactly the sum of its coordinate weights to the exponential volume rate.
```
theorem det_exponentialRescaleBasis {n : ℕ} (b : Basis (Fin n) ℝ L)
    (cost : Fin n → ℝ) (r : ℝ) :
    (b.toMatrix (exponentialRescaleBasis b cost r)).det = Real.exp (r * ∑ j, cost j) := by
…
```
Mentions: OAI.PolycyclicRecognition.exponentialRescaleBasis

theorem OAI.PolycyclicRecognition.haar_model_weighted_box_volume line 38

Source documentation

The same Haar normalization can be used for section coordinates and weighted ideal boxes. The constant is fixed for all scales and radii.

theorem haar_model_weighted_box_volume
    (haar : NilpotentExponentialHaarInput E G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G) (hnil : LieRing.IsNilpotent L)
    {n : ℕ} (b : Basis (Fin n) ℝ L) (cost : Fin n → ℝ)
    (μ : Measure G) [μ.IsHaarMeasure] :
    ∃ c : ℝ≥0, 0 < c ∧ ∀ r R : ℝ, 0 ≤ R →
      μ (exponentialCoordinateBox (Exp ∘ e) (exponentialRescaleBasis b cost r) R) =
        (c : ℝ≥0∞) * ENNReal.ofReal (Real.exp (r * ∑ j, cost j)) *
          ENNReal.ofReal (2 * R) ^ n := by
…

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

theorem OAI.PolycyclicRecognition.haar_model_weighted_unit_volume line 78

Source documentation

Unit boxes have a fixed strictly positive volume coefficient at every scale. This is the lower exponential rate needed for the source probes.

theorem haar_model_weighted_unit_volume
    (haar : NilpotentExponentialHaarInput E G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G) (hnil : LieRing.IsNilpotent L)
    {n : ℕ} (b : Basis (Fin n) ℝ L) (cost : Fin n → ℝ)
    (μ : Measure G) [μ.IsHaarMeasure] :
    ∃ v : ℝ, 0 < v ∧ ∀ r : ℝ,
      μ (exponentialCoordinateBox (Exp ∘ e) (exponentialRescaleBasis b cost r) 1) ≠ 0 ∧
      μ (exponentialCoordinateBox (Exp ∘ e) (exponentialRescaleBasis b cost r) 1) ≠ ⊤ ∧
      (μ (exponentialCoordinateBox (Exp ∘ e) (exponentialRescaleBasis b cost r) 1)).toReal =
        v * Real.exp (r * ∑ j, cost j) := by
…

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

theorem OAI.PolycyclicRecognition.haar_model_sequence_weighted_boxes line 106

Source documentation

Only the sum of the ideal widths contributes to the exponential rate; the radius loss has a common subexponential volume bound.

theorem haar_model_sequence_weighted_boxes
    (haar : NilpotentExponentialHaarInput E G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G) (hnil : LieRing.IsNilpotent L)
    {n : ℕ} (b : Basis (Fin n) ℝ L) (cost : Fin n → ℝ)
    (μ : Measure G) [μ.IsHaarMeasure]
    (scale R : ℕ → ℝ) (hs : Tendsto scale atTop atTop)
    (hR0 : ∀ j, 0 ≤ R j) (hR : HasSubexponentialUpperBoundSeq scale R) :
    ∃ V : ℕ → ℝ, (∀ j, 0 ≤ V j) ∧ HasSubexponentialUpperBoundSeq scale V ∧
      ∀ j, μ (exponentialCoordinateBox (Exp ∘ e)
        (exponentialRescaleBasis b cost (scale j)) (R j)) ≠ ⊤ ∧
        (μ (exponentialCoordinateBox (Exp ∘ e)
…

Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.HasSubexponentialUpperBoundSeq, OAI.PolycyclicRecognition.exponentialCoordinateBox, OAI.PolycyclicRecognition.exponentialRescaleBasis