ResidueProfiles.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Compatible finite residue profiles

A profile records the conditional averages on every finite residue space. Compatibility is tested against all functions on a coarser residue space. The energy identity below is the finite conditional-expectation identity.

structure OAI.JointDickman.ResidueProfile line 15
theorem OAI.JointDickman.residueMean_re line 22
theorem OAI.JointDickman.residueMean_self_conj_re line 28
theorem OAI.JointDickman.residueEnergy_sub line 37
theorem OAI.JointDickman.ResidueProfile.refinement_energy line 50
theorem OAI.JointDickman.ResidueProfile.energy_mono line 61
theorem OAI.JointDickman.ResidueProfile.exists_approximation line 68
Source documentation
One finite residue coordinate approximates every refinement in mean square.
```
theorem exists_approximation (W : ResidueProfile) {ε : ℝ} (hε : 0 < ε) :
    ∃ d : ℕ+, ∀ q : ℕ+, (d : ℕ) ∣ (q : ℕ) →
      residueEnergy (fun a => W.value q a - residueLift (W.value d) a) < ε := by
…
```
Mentions: OAI.JointDickman.ResidueProfile, OAI.JointDickman.residueEnergy, OAI.JointDickman.residueLift