OAI/Probability/InvariantIsing/Unconditional.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Limiting invariant Ising pressure, magnetic fields, and Gaussian patterns.

  1. theorem OAI.InvariantIsing.limiting_pressure_of_extreme_limits_unconditional line 27

    Distinct definitions of this name: ComparatorChallenges/InvariantIsing.lean:282 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.limiting_pressure_of_extreme_limits_unconditional@path.

  2. theorem OAI.InvariantIsing.limiting_wasserstein_field_pressure_of_extreme_limits_unconditional line 45

    Distinct definitions of this name: ComparatorChallenges/InvariantIsing.lean:300 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.limiting_wasserstein_field_pressure_of_extreme_limits_unconditional@path.

  3. theorem OAI.InvariantIsing.positive_temperature_pressure_unconditional line 67

    Distinct definitions of this name: ComparatorChallenges/InvariantIsing.lean:322 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.positive_temperature_pressure_unconditional@path.

  4. theorem OAI.InvariantIsing.ground_state_limit_unconditional line 84

    Distinct definitions of this name: ComparatorChallenges/InvariantIsing.lean:339 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.ground_state_limit_unconditional@path.

  5. theorem OAI.InvariantIsing.random_pressure_tendsto_in_measure_unconditional line 102

    Distinct definitions of this name: ComparatorChallenges/InvariantIsing.lean:357 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.random_pressure_tendsto_in_measure_unconditional@path.

  6. theorem OAI.InvariantIsing.random_pressure_limit_unconditional line 124

    Distinct definitions of this name: ComparatorChallenges/InvariantIsing.lean:377 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.random_pressure_limit_unconditional@path.

  7. theorem OAI.InvariantIsing.random_pressure_tendsto_ae_unconditional line 149

    Distinct definitions of this name: ComparatorChallenges/InvariantIsing.lean:402 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.random_pressure_tendsto_ae_unconditional@path.

  8. theorem OAI.InvariantIsing.random_field_pressure_tendsto_ae_unconditional line 168

    Distinct definitions of this name: ComparatorChallenges/InvariantIsing.lean:421 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.random_field_pressure_tendsto_ae_unconditional@path.

  9. theorem OAI.InvariantIsing.gaussianPattern_pressure_limit_unconditional line 190

    Distinct definitions of this name: ComparatorChallenges/InvariantIsing.lean:443 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.gaussianPattern_pressure_limit_unconditional@path.

  10. theorem OAI.InvariantIsing.gaussianPattern_ground_limit_unconditional line 204

    Distinct definitions of this name: ComparatorChallenges/InvariantIsing.lean:457 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.gaussianPattern_ground_limit_unconditional@path.

  11. theorem OAI.InvariantIsing.gaussianPattern_norm_limits_unconditional line 218

    Distinct definitions of this name: ComparatorChallenges/InvariantIsing.lean:471 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.gaussianPattern_norm_limits_unconditional@path.