ScalarPenalty.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The actual positive scalar softening factors

Absolute affine deviations, positive parts and interval distances have convex integer exponents. Their powers of two are positive log-concave sequences, supplying the concrete line and unary factors of both papers.

def OAI.ContingencyTables.ScalarPenalty.factor line 18
lemma OAI.ContingencyTables.ScalarPenalty.factor_positive line 20
theorem OAI.ContingencyTables.ScalarPenalty.factor_logConcave line 24
Source documentation
Convex discrete exponents give the exact scalar log-concavity test.
```
theorem factor_logConcave (A : ℝ) (hA : 0 ≤ A) (p : ℕ → ℝ) (n : ℕ)
    (hp : 2*p (n-1) ≤ p n+p (n-2)) :
    factor A p n * factor A p (n-2) ≤ (factor A p (n-1))^2 := by
…
```
Mentions: OAI.ContingencyTables.ScalarPenalty.factor
lemma OAI.ContingencyTables.ScalarPenalty.affine_midpoint line 33
lemma OAI.ContingencyTables.ScalarPenalty.abs_affine_convex line 39
lemma OAI.ContingencyTables.ScalarPenalty.max_convex line 46

theorem OAI.ContingencyTables.ScalarPenalty.abs_factor_logConcave line 56

Source documentation

The row and column absolute-deviation softeners used in both papers.

theorem abs_factor_logConcave (A a b : ℝ) (hA : 0 ≤ A) (n : ℕ) (hn : 2 ≤ n) :
    factor A (fun k => |a+(k:ℝ)*b|) n * factor A (fun k => |a+(k:ℝ)*b|) (n-2) ≤
      (factor A (fun k => |a+(k:ℝ)*b|) (n-1))^2 :=
…

Mentions: OAI.ContingencyTables.ScalarPenalty.factor

theorem OAI.ContingencyTables.ScalarPenalty.positivePart_factor_logConcave line 62

Source documentation

Positive-part small-slot penalties of the first paper.

theorem positivePart_factor_logConcave (A a b : ℝ) (hA : 0 ≤ A) (n : ℕ) (hn : 2 ≤ n) :
    factor A (fun k => max (a+(k:ℝ)*b) 0) n * factor A (fun k => max (a+(k:ℝ)*b) 0) (n-2) ≤
      (factor A (fun k => max (a+(k:ℝ)*b) 0) (n-1))^2 := by
…

Mentions: OAI.ContingencyTables.ScalarPenalty.factor

def OAI.ContingencyTables.ScalarPenalty.intervalDistance line 71
Source documentation
Distance from a physical value ell+n to [0,b]. This formula applies to the companion's unary tree penalties.
```
noncomputable def intervalDistance (ell b : ℝ) (n : ℕ) : ℝ :=
…
```
lemma OAI.ContingencyTables.ScalarPenalty.intervalDistance_convex line 74
theorem OAI.ContingencyTables.ScalarPenalty.interval_factor_logConcave line 87
Source documentation
Unary distance softeners are positive and satisfy the exact integer second-difference inequality needed by the product signature.
```
theorem interval_factor_logConcave (A ell b : ℝ) (hA : 0 ≤ A) (n : ℕ) (hn : 2 ≤ n) :
    factor A (intervalDistance ell b) n * factor A (intervalDistance ell b) (n-2) ≤
      (factor A (intervalDistance ell b) (n-1))^2 :=
…
```
Mentions: OAI.ContingencyTables.ScalarPenalty.factor, OAI.ContingencyTables.ScalarPenalty.intervalDistance
theorem OAI.ContingencyTables.ScalarPenalty.factor_limit line 94
Source documentation
The positive equality softener tends to its exact equality indicator. This is the actual finite limiting operation used after marginalization.
```
theorem factor_limit (D : ℝ) (hD : 0 ≤ D) :
    Filter.Tendsto (fun A : ℝ => (2:ℝ)^(-A*D)) Filter.atTop
      (nhds (if D=0 then 1 else 0)) := by
…
```

theorem OAI.ContingencyTables.ScalarPenalty.mul_logConcave line 113

Source documentation

Products of positive scalar log-concave sequences remain log-concave.

theorem mul_logConcave (a b : ℕ → ℝ) (n : ℕ)
    (ha : a n*a (n-2) ≤ (a (n-1))^2)
    (hb : b n*b (n-2) ≤ (b (n-1))^2)
    (hapos : 0 ≤ a n*a (n-2)) (hbpos : 0 ≤ b n*b (n-2)) :
    (a n*b n)*(a (n-2)*b (n-2)) ≤ (a (n-1)*b (n-1))^2 := by
…