Products.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FiniteFactor.sourceKappa line 12
Source documentation
The source's kappa_s, with natural indices shifted to start at one.
Also declared: ComparatorChallenges/ProductBrown.lean:141 (same declaration text).
```
def sourceKappa (s : ℕ) : ℝ := 1 / (100*((s : ℝ)+1))
```
theorem OAI.FiniteFactor.sourceKappa_sq_summable line 14
theorem OAI.FiniteFactor.CouplingParameters.block_energy_cancellation line 27
theorem OAI.FiniteFactor.CouplingParameters.uniform_block_budget line 35
Source documentation
The sum over arbitrary finite sets of whole blocks is uniformly bounded. The unique tagged block contributes at most one, even when it is absent.
```
theorem uniform_block_budget (p : ℕ → CouplingParameters) (j : ℕ)
    (htag : ∀ s, (p s).tagged = decide (s=j))
    (hκ : Summable (fun s => (p s).kappa^2)) (B : Finset ℕ) :
    (∑ s ∈ B, (p s).m * (2*(p s).kappa^2/(p s).m + (p s).tagMass)) ≤
      2*(∑' s, (p s).kappa^2) + 1 := by
…
```
Mentions: OAI.FiniteFactor.CouplingParameters, OAI.FiniteFactor.CouplingParameters.tagMass
def OAI.FiniteFactor.CouplingParameters.selectedDensity line 50
Source documentation
A coordinate may be omitted altogether, and every included coordinate may choose its endpoint independently of every other coordinate.
```
def selectedDensity (p : CouplingParameters) (enabled right : Bool) (t : ℝ) : ℝ :=
…
```
Mentions: OAI.FiniteFactor.CouplingParameters
theorem OAI.FiniteFactor.CouplingParameters.selectedDensity_energy line 53
def OAI.FiniteFactor.CouplingParameters.finiteProductDensity line 66
Source documentation
Actual finite product of the chosen coordinate densities.
```
def finiteProductDensity {ι : Type*} [Fintype ι] (p : ι → CouplingParameters)
    (enabled right : ι → Bool) (x : ι → ℝ) : ℝ :=
…
```
Mentions: OAI.FiniteFactor.CouplingParameters
theorem OAI.FiniteFactor.CouplingParameters.finiteProductDensity_energy line 70

theorem OAI.FiniteFactor.CouplingParameters.finite_block_product_uniform line 83

Source documentation

Prefixes and all intermediate endpoint selections have a common square integral bound. A finite prefix is represented by enabling its coordinates inside any finite collection of blocks containing that prefix.

theorem finite_block_product_uniform (p : ℕ → CouplingParameters) (m : ℕ → ℕ)
    (hm : ∀ s, (p s).m = (m s : ℝ)) (j : ℕ)
    (htag : ∀ s, (p s).tagged = decide (s=j))
    (hκ : Summable (fun s => (p s).kappa^2)) (B : Finset ℕ)
    (enabled right : (Σ s : B, Fin (m s)) → Bool) :
    (∫ x, finiteProductDensity (fun i : Σ s : B, Fin (m s) => p i.1)
      enabled right x ^ 2 ∂Measure.pi (fun _ : Σ s : B, Fin (m s) => unitIntervalMeasure)) ≤
      Real.exp (20*(2*(∑' s, (p s).kappa^2)+1)) := by
…

Mentions: OAI.FiniteFactor.CouplingParameters, OAI.FiniteFactor.CouplingParameters.finiteProductDensity, OAI.FiniteFactor.unitIntervalMeasure

theorem OAI.FiniteFactor.CouplingParameters.selectedDensity_nonneg line 107
theorem OAI.FiniteFactor.CouplingParameters.selectedDensity_le_ten line 113
theorem OAI.FiniteFactor.CouplingParameters.selectedDensity_measurable line 119
theorem OAI.FiniteFactor.CouplingParameters.selectedDensity_memLp line 125
theorem OAI.FiniteFactor.CouplingParameters.selectedDensity_integral line 131
theorem OAI.FiniteFactor.CouplingParameters.finiteProductDensity_measurable line 137
theorem OAI.FiniteFactor.CouplingParameters.finiteProductDensity_memLp line 145
Source documentation
Membership in L2 is proved, so the uniform square-integral bound is not an assertion about a Bochner integral of a nonintegrable function.
```
theorem finiteProductDensity_memLp {ι : Type*} [Fintype ι]
    (p : ι → CouplingParameters) (enabled right : ι → Bool) :
    MemLp (finiteProductDensity p enabled right) 2 (Measure.pi (fun _ : ι => unitIntervalMeasure)) := by
…
```
Mentions: OAI.FiniteFactor.CouplingParameters, OAI.FiniteFactor.CouplingParameters.finiteProductDensity, OAI.FiniteFactor.unitIntervalMeasure
theorem OAI.FiniteFactor.CouplingParameters.finiteProductDensity_integral line 162

theorem OAI.FiniteFactor.CouplingParameters.finite_block_product_source_uniform line 170

Source documentation

Exact source kappa, independent of the tagged stage, yields one fixed bound.

theorem finite_block_product_source_uniform (p : ℕ → CouplingParameters) (m : ℕ → ℕ)
    (hm : ∀ s, (p s).m = (m s : ℝ)) (j : ℕ)
    (htag : ∀ s, (p s).tagged = decide (s=j)) (hκ : ∀ s, (p s).kappa = sourceKappa s)
    (B : Finset ℕ) (enabled right : (Σ s : B, Fin (m s)) → Bool) :
    (∫ x, finiteProductDensity (fun i : Σ s : B, Fin (m s) => p i.1)
      enabled right x ^ 2 ∂Measure.pi (fun _ : Σ s : B, Fin (m s) => unitIntervalMeasure)) ≤
      Real.exp (20*(2*(∑' s, sourceKappa s ^ 2)+1)) := by
…

Mentions: OAI.FiniteFactor.CouplingParameters, OAI.FiniteFactor.sourceKappa, OAI.FiniteFactor.CouplingParameters.finiteProductDensity, OAI.FiniteFactor.unitIntervalMeasure