ProbeKernelVolume.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The ideal restriction has its intrinsic weighted Haar volume

theorem OAI.PolycyclicRecognition.exponentialIdealKernelRegion_eq_image line 27
Source documentation
The ideal region used for the target-cell restriction is the image of the actual intrinsic ideal set, not a possibly larger preimage region.
```
theorem exponentialIdealKernelRegion_eq_image (A : Set U) :
    exponentialIdealKernelRegion U π ExpN A =
      kernelRealization π ι hι hrange '' (ExpI '' A) := by
…
```
Mentions: OAI.PolycyclicRecognition.exponentialIdealKernelRegion, OAI.PolycyclicRecognition.kernelRealization
theorem OAI.PolycyclicRecognition.exponentialIdealKernelRegion_measure line 45
Source documentation
Transport through the kernel homeomorphism preserves the exact ideal volume, for the same kernel measure used by quotient integration.
```
theorem exponentialIdealKernelRegion_measure (μ : Measure I) (A : Set U) :
    (Measure.map (kernelRealization π ι hι hrange) μ)
      (exponentialIdealKernelRegion U π ExpN A) = μ (ExpI '' A) := by
…
```
Mentions: OAI.PolycyclicRecognition.kernelRealization, OAI.PolycyclicRecognition.exponentialIdealKernelRegion

theorem OAI.PolycyclicRecognition.exists_exponential_kernel_box_volumes line 63

Source documentation

The actual kernel region in the target packing has the expected ideal exponent and a subexponential radius loss, in its transported Haar measure.

theorem exists_exponential_kernel_box_volumes
    (haar : NilpotentExponentialHaarInput E I)
    (groupExp : GroupLieAlgebra (𝓘(ℝ, E)) I → I) (hExp : IsGroupExponential groupExp)
    (e : U ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) I) (hnil : LieRing.IsNilpotent U)
    (hc : ∀ u : U, ι (groupExp (e u)) = ExpN u)
    {m : ℕ} (b : Basis (Fin m) ℝ U) (cost : Fin m → ℝ)
    (μ : Measure I) [μ.IsHaarMeasure]
    (scale R : ℕ → ℝ) (hs : Tendsto scale atTop atTop)
    (hR0 : ∀ n, 0 ≤ R n) (hR : HasSubexponentialUpperBoundSeq scale R) :
    let μK := Measure.map (kernelRealization π ι hι hrange) μ
…

Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.HasSubexponentialUpperBoundSeq, OAI.PolycyclicRecognition.kernelRealization

theorem OAI.PolycyclicRecognition.exists_exponential_kernel_unit_volumes line 98

Source documentation

The source ideal unit boxes have a positive fixed coefficient, in the same transported kernel measure used in the section coordinates.

theorem exists_exponential_kernel_unit_volumes
    (haar : NilpotentExponentialHaarInput E I)
    (groupExp : GroupLieAlgebra (𝓘(ℝ, E)) I → I) (hExp : IsGroupExponential groupExp)
    (e : U ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) I) (hnil : LieRing.IsNilpotent U)
    (hc : ∀ u : U, ι (groupExp (e u)) = ExpN u)
    {m : ℕ} (b : Basis (Fin m) ℝ U) (cost : Fin m → ℝ)
    (μ : Measure I) [μ.IsHaarMeasure] :
    let μK := Measure.map (kernelRealization π ι hι hrange) μ
…

Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.kernelRealization