Main.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FourRow.strictExponent line 9
def OAI.FourRow.robustRadius line 11
theorem OAI.FourRow.normalized_robust_permanent line 13

theorem OAI.FourRow.lpNorm_scale line 29

Source comment

Homogeneity extends the bound to unrestricted nonnegative rows.

theorem lpNorm_scale (p : ℝ) (hp : p ≠ 0) (c : ℝ) (hc : 0 ≤ c)
    (a : Site → ℝ) (ha : ∀ j, 0 ≤ a j) :
    lpNorm p (fun j => c * a j) = c * lpNorm p a := by
…

Mentions: OAI.FourRow.Site, OAI.FourRow.lpNorm

theorem OAI.FourRow.expectation_scale line 39
theorem OAI.FourRow.rowSq_zero_entries line 49
theorem OAI.FourRow.robust_permanent_explicit line 56
theorem OAI.FourRow.robust_permanent line 100
Source documentation
A robust permanent inequality with explicit absolute constants.
Distinct definitions of this name: ComparatorChallenges/FourRowPermanent.lean:37 (same statement text; different proof or body). Qualify references as OAI.FourRow.robust_permanent@path.
```
theorem robust_permanent :
  ∃ p₀ : ℝ, 4 / 3 < p₀ ∧ p₀ < 2 ∧
    ∃ ε : ℝ, 0 < ε ∧ ∀ ν : Law,
      IsProbability ν → totalVariation ν < ε → UniformMarginals ν →
      ∀ f : Functions, (∀ i j, 0 ≤ f i j) →
        permanentExpectation ν f ≤ ∏ i, lpNorm p₀ (f i) := by
…
```
Mentions: OAI.FourRow.Law, OAI.FourRow.IsProbability, OAI.FourRow.totalVariation, OAI.FourRow.UniformMarginals, OAI.FourRow.Functions, OAI.FourRow.permanentExpectation, OAI.FourRow.lpNorm