Compression.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform compression of the actual logarithmic graph matrix

A single common index is chosen for all levels. Greedy pivots are replaced by representatives fixed from their labels, and only those labels and rounded grouped weights enter the finite code. The resulting list has no factor depending on the number of vertices.

theorem OAI.MetricEntropyDuality.exists_compressionCode line 32

Source documentation

Construct an actual finite code for a nonnegative mixture of graph profiles, including profiles at infinite distance.

theorem exists_compressionCode
    (L : (i : Fin u) → X → Label i) (E : FixedLabels L q)
    (v : Y → X) (T : Y → Finset (Fin u)) (μ : Y → ℝ)
    (hμ : ∀ y, 0 ≤ μ y) (hmass : ∑ y, μ y ≤ 1)
    (hu : 0 < u) (hh : 0 < h) (hs : 0 < s)
    (θ : ℝ) (hθ : 0 < θ) (hsθ : 1 ≤ (s : ℝ) * θ)
    (hprofile : Real.log 3 / Real.log ((h : ℝ) + 1) ≤ θ)
    (hcomp : ∀ y, ((Finset.univ \ T y).card : ℝ) ≤ θ * (u : ℝ)) :
    ∃ code : CompressionCode u q h s (weightCodeSize (roundingStep θ s u)),
      ∀ x, profileMixture L v T h μ x - 3 * θ ≤ compressionDecode L E h s θ code x ∧
        compressionDecode L E h s θ code x ≤ profileMixture L v T h μ x + θ := by
…

Mentions: OAI.MetricEntropyDuality.FixedLabels, OAI.MetricEntropyDuality.CompressionCode, OAI.MetricEntropyDuality.weightCodeSize, OAI.MetricEntropyDuality.roundingStep, OAI.MetricEntropyDuality.compressionDecode

theorem OAI.MetricEntropyDuality.compressionList_bounds line 105

Source documentation

The fixed decoded list uniformly approximates every nonnegative mixture with one-sided errors.

theorem compressionList_bounds
    (L : (i : Fin u) → X → Label i) (E : FixedLabels L q)
    (𝒯 : Finset (Finset (Fin u)))
    (hu : 0 < u) (hh : 0 < h) (hs : 0 < s)
    (θ : ℝ) (hθ : 0 < θ) (hsθ : 1 ≤ (s : ℝ) * θ)
    (hprofile : Real.log 3 / Real.log ((h : ℝ) + 1) ≤ θ)
    (hcomp : ∀ T ∈ 𝒯, ((Finset.univ \ T).card : ℝ) ≤ θ * (u : ℝ))
    (μ : GraphProfile.Columns X 𝒯 → ℝ)
    (hμ : ∀ y, 0 ≤ μ y) (hmass : ∑ y, μ y ≤ 1) :
    ∃ a ∈ compressionList L E h s θ, ∀ x,
      columnCombination (GraphProfile.column L 𝒯 h) μ x - 3 * θ ≤ a x ∧
        a x ≤ columnCombination (GraphProfile.column L 𝒯 h) μ x + θ := by
…

Mentions: OAI.MetricEntropyDuality.FixedLabels, OAI.MetricEntropyDuality.GraphProfile.Columns, OAI.MetricEntropyDuality.compressionList, OAI.MetricEntropyDuality.columnCombination, OAI.MetricEntropyDuality.GraphProfile.column

theorem OAI.MetricEntropyDuality.uniform_compression line 125

Source documentation

Complete positive compression from the actual partition graph and logarithmic profile, with a fixed list and the literal finite-code bound.

theorem uniform_compression
    (L : (i : Fin u) → X → Label i)
    (hlabels : ∀ i, Nat.card (Set.range (L i)) ≤ q)
    (𝒯 : Finset (Finset (Fin u)))
    (hu : 0 < u) (hq : 0 < q) (hh : 0 < h) (hs : 0 < s)
    (θ : ℝ) (hθ : 0 < θ) (hsθ : 1 ≤ (s : ℝ) * θ)
    (hprofile : Real.log 3 / Real.log ((h : ℝ) + 1) ≤ θ)
    (hcomp : ∀ T ∈ 𝒯, ((Finset.univ \ T).card : ℝ) ≤ θ * (u : ℝ)) :
    ∃ A : Finset (X → ℝ), A.Nonempty ∧
      (A.card : ℝ) ≤ (u : ℝ) * (q : ℝ) ^ (h * s) *
        (1 + (s : ℝ) * 2 ^ u / θ) ^ (h * s * 2 ^ u) ∧
      SignedCompression.PositiveApproximation (GraphProfile.column L 𝒯 h) θ A := by
…

Mentions: OAI.MetricEntropyDuality.SignedCompression.PositiveApproximation, OAI.MetricEntropyDuality.GraphProfile.column

theorem OAI.MetricEntropyDuality.uniform_signed_compression line 151

Source documentation

Signed compression is supplied by the actual difference list of the constructed positive list; its cardinal is at most the square of that list.

theorem uniform_signed_compression
    (L : (i : Fin u) → X → Label i)
    (hlabels : ∀ i, Nat.card (Set.range (L i)) ≤ q)
    (𝒯 : Finset (Finset (Fin u)))
    (hu : 0 < u) (hq : 0 < q) (hh : 0 < h) (hs : 0 < s)
    (θ : ℝ) (hθ : 0 < θ) (hsθ : 1 ≤ (s : ℝ) * θ)
    (hprofile : Real.log 3 / Real.log ((h : ℝ) + 1) ≤ θ)
    (hcomp : ∀ T ∈ 𝒯, ((Finset.univ \ T).card : ℝ) ≤ θ * (u : ℝ)) :
    ∃ A B : Finset (X → ℝ), A.Nonempty ∧
      (A.card : ℝ) ≤ (u : ℝ) * (q : ℝ) ^ (h * s) *
        (1 + (s : ℝ) * 2 ^ u / θ) ^ (h * s * 2 ^ u) ∧
      B.card ≤ A.card ^ 2 ∧
…