ProbeSourcePacking.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Separated source counts for the retained probe volume

theorem OAI.PolycyclicRecognition.exists_fixedSlice_image_net_constant line 29

Source documentation

Positive probe volume supplies genuinely separated image endpoints. The constant is independent of the source sheet, its Cartan pivot, the normalized map and the point at which its image is centered.

theorem exists_fixedSlice_image_net_constant
    {Λ : ℝ≥0} (hΛ : 0 < (Λ : ℝ)) :
    ∃ c : ℝ, 0 < c ∧ ∀ (p : NormalizedPair G Λ) (x a : G) (d : D)
      (S : Set N), IsCompact S →
      ∃ t : Finset G,
        (↑t : Set G) ⊆ (fun n => basedImage p.val.1 a (x * ι n * κ d)) '' S ∧
        (∀ u ∈ t, ∀ v ∈ t, u ≠ v → 1 ≤ dist u v) ∧
        c * (μ S).toReal ≤ (t.card : ℝ) := by
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.basedImage

theorem OAI.PolycyclicRecognition.exists_fixedSlice_probe_net_constant line 69

Source documentation

Apply the uniform fixed-slice count directly to a compact set retained from the original uniform probe distribution. Its probability loss becomes only a fixed multiplicative constant in the separated count.

theorem exists_fixedSlice_probe_net_constant
    {P : Type*} [TopologicalSpace P] [MeasurableSpace P]
    (ν : Measure P) (e : P → N) (he : MeasurableEmbedding e) (hec : Continuous e)
    (hμ : μ = Measure.map e ν) {Λ : ℝ≥0} (hΛ : 0 < (Λ : ℝ)) :
    ∃ c : ℝ, 0 < c ∧ ∀ (p : NormalizedPair G Λ) (x a : G) (d : D)
      (A K : Set P) (hA0 : ν A ≠ 0) (hAt : ν A ≠ ⊤),
      IsCompact K → MeasurableSet K → K ⊆ A →
      ∀ q : ℝ, 0 ≤ q →
      ENNReal.ofReal q ≤ (cellProbabilityMeasure ν A hA0 hAt : Measure P) K →
      ∃ t : Finset G,
        (↑t : Set G) ⊆ (fun y => basedImage p.val.1 a (x * ι (e y) * κ d)) '' K ∧
        (∀ u ∈ t, ∀ v ∈ t, u ≠ v → 1 ≤ dist u v) ∧
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.cellProbabilityMeasure, OAI.PolycyclicRecognition.basedImage

theorem OAI.PolycyclicRecognition.exists_probe_source_count_sequence line 98

Source documentation

A quarter of the original probe cell yields the full source exponent, uniformly over a sequence of maps, centers and moving Cartan pivots.

theorem exists_probe_source_count_sequence
    {P : Type*} [TopologicalSpace P] [MeasurableSpace P]
    (ν : Measure P) (e : ℕ → P → N)
    (he : ∀ n, MeasurableEmbedding (e n)) (hec : ∀ n, Continuous (e n))
    (hμ : ∀ n, μ = Measure.map (e n) ν)
    {Λ : ℝ≥0} (hΛ : 0 < (Λ : ℝ)) (p : ℕ → NormalizedPair G Λ)
    (x a : ℕ → G) (d : ℕ → D) (A K : ℕ → Set P)
    (hA0 : ∀ n, ν (A n) ≠ 0) (hAt : ∀ n, ν (A n) ≠ ⊤)
    (hK : ∀ n, IsCompact (K n)) (hKm : ∀ n, MeasurableSet (K n))
    (hKA : ∀ n, K n ⊆ A n)
    (hmass : ∀ n, ENNReal.ofReal (1 / 4 : ℝ) ≤
      (cellProbabilityMeasure ν (A n) (hA0 n) (hAt n) : Measure P) (K n))
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.cellProbabilityMeasure