CartanPolarRegionMeasure.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A single target Haar normalization for all concentrated probes

theorem OAI.PolycyclicRecognition.CartanWordModel.MeasuredCone.sectionMeasure_eq line 24

Source documentation

Every adapted target section gives exactly the same measure, not just another scalar multiple of Haar measure.

theorem MeasuredCone.sectionMeasure_eq
    (σ τ : ContinuousMap D.Q.carrier F.N.carrier)
    (hσ : ∀ q, D.maps.quotient (σ q) = q)
    (hτ : ∀ q, D.maps.quotient (τ q) = q) :
    D.sectionMeasure M F C σ hσ = D.sectionMeasure M F C τ hτ := by
…

theorem OAI.PolycyclicRecognition.CartanWordModel.MeasuredCone.fixed_polar_region_factory line 59

Source documentation

Instantiate the published polar-region construction with twice the concentration error and retain the fixed original target Haar measure. The region threshold was chosen before the concentration error or its path constant.

theorem MeasuredCone.fixed_polar_region_factory
    (K : ProperCone ℝ (StrongDual ℝ W)) (A : W →ₗ[ℝ] W) (ε : ℝ) (w : W)
    (height : G →* Multiplicative W)
    (act : G →* Equiv.Perm D.Q.carrier)
    (ν : Measure F.D.carrier) (cell : Set (F.N.carrier × F.D.carrier))
    (scale : ℕ → ℝ) (P₂ δ δ₀ : ℝ) (hδ : 0 < δ) (hδ₀ : δ ≤ δ₀)
    (regions : ∀ (η : ℕ → ℝ), (∀ n, 0 ≤ η n) → Tendsto η atTop (𝓝 0) →
      ∀ Cp Clog : ℝ, 0 ≤ Cp → 0 ≤ Clog →
      ∃ R : MeasuredProbeRegions D.maps.quotient D.measures.measureQ
        (D.kernelMeasure M F C) ν scale P₂,
        ∀ δ' : ℝ, 0 < δ' → δ' ≤ δ₀ →
        ∀ᶠ n in atTop, R.ControlsTwoPaths
…

Mentions: OAI.PolycyclicRecognition.MeasuredProbeRegions