ProfileMixtures.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Combining graph-ball levels using the actual logarithmic profile

The profile expansion and dilation estimate are applied to each actual extended graph distance. The finite sums below retain disconnected distances, with no extra finite-distance hypothesis. The final theorem combines the two losses from column assignment and the one loss from rounding.

theorem OAI.MetricEntropyDuality.ProfileMixtures.sum_gamma_fin line 27
def OAI.MetricEntropyDuality.ProfileMixtures.profileMixture line 33
Source documentation
The actual nonnegative column mixture, before imposing any sign or mass condition on its coefficients.
```
def profileMixture (L : (i : ι) → X → Label i) (v : Y → X) (T : Y → Finset ι)
    (h : ℕ) (μ : Y → ℝ) (x : X) : ℝ :=
…
```
theorem OAI.MetricEntropyDuality.ProfileMixtures.ballIndicator_eq_distance line 37
theorem OAI.MetricEntropyDuality.ProfileMixtures.sum_weighted_levels line 45
theorem OAI.MetricEntropyDuality.ProfileMixtures.profileMixture_eq_sum line 59
Source documentation
The literal logarithmic profile is exactly the weighted sum of the original graph-ball mixture at all levels.
```
theorem profileMixture_eq_sum (L : (i : ι) → X → Label i) (v : Y → X)
    (T : Y → Finset ι) {h : ℕ} (hh : 0 < h) (μ : Y → ℝ) (x : X) :
    profileMixture L v T h μ x = ∑ j : Fin h,
      LogProfile.gamma h j.val * CompressionLevels.levelValue L v T μ j.val x := by
…
```
Mentions: OAI.MetricEntropyDuality.ProfileMixtures.profileMixture, OAI.MetricEntropyDuality.LogProfile.gamma, OAI.MetricEntropyDuality.CompressionLevels.levelValue
theorem OAI.MetricEntropyDuality.ProfileMixtures.profileMixture_columns line 75
Source documentation
With the actual graph-column index type, the mixture is the shared literal columnCombination, rather than a separate abstract approximation predicate.
```
theorem profileMixture_columns [Fintype X]
    (L : (i : ι) → X → Label i) (𝒯 : Finset (Finset ι)) (h : ℕ)
    (μ : GraphProfile.Columns X 𝒯 → ℝ) (x : X) :
    profileMixture L (fun y : GraphProfile.Columns X 𝒯 => y.1)
        (fun y => y.2.val) h μ x =
      columnCombination (GraphProfile.column L 𝒯 h) μ x := rfl
```
Mentions: OAI.MetricEntropyDuality.GraphProfile.Columns, OAI.MetricEntropyDuality.ProfileMixtures.profileMixture, OAI.MetricEntropyDuality.columnCombination, OAI.MetricEntropyDuality.GraphProfile.column

theorem OAI.MetricEntropyDuality.ProfileMixtures.dilated_level_sum_le line 84

Source documentation

The actual factor-three dilation bound survives mixing columns whose nonnegative coefficients have total mass at most one.

theorem dilated_level_sum_le (L : (i : ι) → X → Label i) (v : Y → X)
    (T : Y → Finset ι) (μ : Y → ℝ) (hμ : ∀ y, 0 ≤ μ y)
    (hmass : ∑ y, μ y ≤ 1) {h : ℕ} (hh : 0 < h) {θ : ℝ}
    (hθ0 : 0 ≤ θ) (hprofile : Real.log 3 / Real.log ((h : ℝ) + 1) ≤ θ) (x : X) :
    (∑ j : Fin h, LogProfile.gamma h j.val *
      CompressionLevels.levelValue L v T μ (3 * j.val + 2) x) ≤
        profileMixture L v T h μ x + θ := by
…

Mentions: OAI.MetricEntropyDuality.LogProfile.gamma, OAI.MetricEntropyDuality.CompressionLevels.levelValue, OAI.MetricEntropyDuality.ProfileMixtures.profileMixture

theorem OAI.MetricEntropyDuality.ProfileMixtures.rounded_level_sum_bounds line 117

Source documentation

Per-level assignment losses and rounding losses combine into the actual one-sided profile bounds from uniform compression.

theorem rounded_level_sum_bounds (L : (i : ι) → X → Label i) (v : Y → X)
    (T : Y → Finset ι) (μ : Y → ℝ) (hμ : ∀ y, 0 ≤ μ y)
    (hmass : ∑ y, μ y ≤ 1) {h : ℕ} (hh : 0 < h) {θ : ℝ}
    (hθ0 : 0 ≤ θ) (hprofile : Real.log 3 / Real.log ((h : ℝ) + 1) ≤ θ)
    (x : X) (assigned rounded : Fin h → ℝ)
    (hlower : ∀ j, CompressionLevels.levelValue L v T μ j.val x - 2 * θ ≤ assigned j)
    (hupper : ∀ j, assigned j ≤ CompressionLevels.levelValue L v T μ (3 * j.val + 2) x)
    (hround : ∀ j, 0 ≤ assigned j - rounded j ∧ assigned j - rounded j ≤ θ) :
    profileMixture L v T h μ x - 3 * θ ≤
        ∑ j : Fin h, LogProfile.gamma h j.val * rounded j ∧
      (∑ j : Fin h, LogProfile.gamma h j.val * rounded j) ≤
        profileMixture L v T h μ x + θ := by
…

Mentions: OAI.MetricEntropyDuality.CompressionLevels.levelValue, OAI.MetricEntropyDuality.ProfileMixtures.profileMixture, OAI.MetricEntropyDuality.LogProfile.gamma