PairMeasureScaling.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Normalizing a finite stationary measure

The inverse coupling produces a finite nonzero measure. Its probability normalization retains the same sublinear error and therefore the same prescribed inverse coefficient.

theorem OAI.PolycyclicRecognition.eLpNorm_pairHeight_error_finite line 26

Source documentation

The pointwise error and the Hilbert error agree for every finite measure.

theorem eLpNorm_pairHeight_error_finite
    (μ : Measure (NormalizedPair G Λ)) [IsFiniteMeasure μ]
    (π : G →* Multiplicative W) (hπ : Continuous fun g => (π g).toAdd)
    (l : G →* Multiplicative W) (g : G) :
    eLpNorm (fun p : NormalizedPair G Λ => pairHeight π g p - (l g).toAdd) 2 μ =
      ENNReal.ofReal ‖pairHeightL2 μ π hπ g - Lp.const 2 μ (l g).toAdd‖ := by
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairHeight, OAI.PolycyclicRecognition.pairHeightL2

theorem OAI.PolycyclicRecognition.norm_pairHeight_error_smul_measure line 39

Source documentation

Scaling the measure scales every height-error norm by one fixed factor.

theorem norm_pairHeight_error_smul_measure
    (μ : Measure (NormalizedPair G Λ)) [IsFiniteMeasure μ]
    (c : ℝ≥0∞) [IsFiniteMeasure (c • μ)]
    (π : G →* Multiplicative W) (hπ : Continuous fun g => (π g).toAdd)
    (l : G →* Multiplicative W) (g : G) :
    ‖pairHeightL2 (c • μ) π hπ g - Lp.const 2 (c • μ) (l g).toAdd‖ =
      (c ^ (1 / 2 : ℝ)).toReal * ‖pairHeightL2 μ π hπ g - Lp.const 2 μ (l g).toAdd‖ := by
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairHeightL2

theorem OAI.PolycyclicRecognition.pairHeight_sublinear_smul_measure line 56

Source documentation

Sublinearity survives every finite scaling of the stationary measure.

theorem pairHeight_sublinear_smul_measure
    (μ : Measure (NormalizedPair G Λ)) [IsFiniteMeasure μ]
    (c : ℝ≥0∞) [IsFiniteMeasure (c • μ)]
    (π l : G →* Multiplicative W) (hπ : Continuous fun g => (π g).toAdd)
    (hsub : ∀ ε : ℝ, 0 < ε → ∃ B : ℝ, 0 ≤ B ∧ ∀ g,
      ‖pairHeightL2 μ π hπ g - Lp.const 2 μ (l g).toAdd‖ ≤ ε * dist 1 g + B) :
    ∀ ε : ℝ, 0 < ε → ∃ B : ℝ, 0 ≤ B ∧ ∀ g,
      ‖pairHeightL2 (c • μ) π hπ g - Lp.const 2 (c • μ) (l g).toAdd‖ ≤
        ε * dist 1 g + B := by
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairHeightL2

theorem OAI.PolycyclicRecognition.exists_probability_with_same_pairHeight_slope line 83

Source documentation

A finite nonzero invariant measure can be normalized without changing its prescribed sublinear slope.

theorem exists_probability_with_same_pairHeight_slope
    (μ : Measure (NormalizedPair G Λ)) [IsFiniteMeasure μ]
    [SMulInvariantMeasure G (NormalizedPair G Λ) μ] (hμ : μ ≠ 0)
    (π l : G →* Multiplicative W) (hπ : Continuous fun g => (π g).toAdd)
    (hsub : ∀ ε : ℝ, 0 < ε → ∃ B : ℝ, 0 ≤ B ∧ ∀ g,
      ‖pairHeightL2 μ π hπ g - Lp.const 2 μ (l g).toAdd‖ ≤ ε * dist 1 g + B) :
    ∃ ν : Measure (NormalizedPair G Λ), ∃ hν : IsProbabilityMeasure ν,
      SMulInvariantMeasure G (NormalizedPair G Λ) ν ∧
      let := hν
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairHeightL2