GAN theory

TorchLean's baseline GAN spec uses least-squares GAN losses. This avoids partial logarithms in the public spec surface while still capturing the generator/discriminator game:

• the discriminator regresses real samples toward score 1 and generated samples toward 0;
• the generator tries to make generated samples score as real.

These lemmas expose the exact composition and loss decomposition used by examples and downstream verification work.

The mathematical reason this file is more compact than the VAE/VQ-VAE theory files is that the public spec deliberately chooses the LSGAN square-loss objective rather than the original minimax log D + log(1-D) objective. That keeps the executable Lean surface total over every supported scalar backend; logarithmic GAN objectives belong in a domain-restricted layer with explicit 0 < D(x) < 1 assumptions. The facts below are therefore the safe core: they make the generator/discriminator composition and the score-regression targets transparent, without smuggling analytic side conditions into a total spec.

• Ian Goodfellow et al., "Generative Adversarial Nets", NeurIPS 2014.
• Xudong Mao et al., "Least Squares Generative Adversarial Networks", ICCV 2017.
• Martin Arjovsky, Soumith Chintala, and Léon Bottou, "Wasserstein GAN", ICML 2017, for the broader critic-vs-discriminator viewpoint that motivates keeping the score head abstract.

@[simp]

theorem NN.MLTheory.Generative.Latent.GAN.generate_eq_generator {α : Type} [Context α] {latent obs : Spec.Shape} (model : Generative.GAN.Model α latent obs) (z : Spec.Tensor α latent) : Generative.GAN.generate model z = model.generator.forward z

Generated samples are obtained by applying the generator to latent noise.

@[simp]

theorem NN.MLTheory.Generative.Latent.GAN.fakeScore_is_discriminator_after_generator {α : Type} [Context α] {latent obs : Spec.Shape} (model : Generative.GAN.Model α latent obs) (z : Spec.Tensor α latent) : Generative.GAN.fakeScore model z = model.discriminator.forward (model.generator.forward z)

Fake scores are discriminator scores on generated samples.

@[simp]

theorem NN.MLTheory.Generative.Latent.GAN.generatorLoss_eq_mse_fake_real {α : Type} [Context α] {latent obs : Spec.Shape} [DecidableRel fun (x1 x2 : α) => x1 > x2] [LE α] (model : Generative.GAN.Model α latent obs) (z : Spec.Tensor α latent) : Generative.GAN.generatorLoss model z = Spec.mseSpec (Generative.GAN.fakeScore model z) Generative.GAN.realTarget

LSGAN generator loss regresses fake scores toward the real target.

This is the generator side of Mao et al.'s least-squares objective: the generator does not receive the discriminator's "fake" target; it tries to move generated samples onto the real-score target.

@[simp]

theorem NN.MLTheory.Generative.Latent.GAN.discriminatorLoss_eq_real_fake_terms {α : Type} [Context α] {latent obs : Spec.Shape} [DecidableRel fun (x1 x2 : α) => x1 > x2] [LE α] (model : Generative.GAN.Model α latent obs) (xReal : Spec.Tensor α obs) (z : Spec.Tensor α latent) : Generative.GAN.discriminatorLoss model xReal z = Spec.mseSpec (Generative.GAN.realScore model xReal) Generative.GAN.realTarget + Spec.mseSpec (Generative.GAN.fakeScore model z) Generative.GAN.fakeTarget

LSGAN discriminator loss splits into real-score and fake-score regression terms.

The first term pushes D(x_real) toward 1; the second pushes D(G(z)) toward 0. Keeping this as a named theorem gives downstream examples and proof files a stable reference point for the game semantics, instead of requiring them to unfold the spec directly.

Connection to shared objective algebra and equilibrium checks

noncomputable def NN.MLTheory.Generative.Latent.GAN.generatorObjectiveTerms {latent obs : Spec.Shape} [DecidableRel fun (x1 x2 : ℝ) => x1 > x2] (model : Generative.GAN.Model ℝ latent obs) (z : Spec.Tensor ℝ latent) : Objective.WeightedTwoTerm

Package the LSGAN generator objective as a two-term objective with no regularizer.

noncomputable def NN.MLTheory.Generative.Latent.GAN.discriminatorObjectiveTerms {latent obs : Spec.Shape} [DecidableRel fun (x1 x2 : ℝ) => x1 > x2] (model : Generative.GAN.Model ℝ latent obs) (xReal : Spec.Tensor ℝ obs) (z : Spec.Tensor ℝ latent) : Objective.WeightedThreeTerm

Package the LSGAN discriminator objective as real-score plus fake-score regression.

theorem NN.MLTheory.Generative.Latent.GAN.generatorLoss_eq_weightedTwoTerm {latent obs : Spec.Shape} [DecidableRel fun (x1 x2 : ℝ) => x1 > x2] (model : Generative.GAN.Model ℝ latent obs) (z : Spec.Tensor ℝ latent) (weight : ℝ) : Generative.GAN.generatorLoss model z = Objective.weightedTwoTerm weight (generatorObjectiveTerms model z)

LSGAN generator loss is the shared two-term objective with zero regularizer.

theorem NN.MLTheory.Generative.Latent.GAN.discriminatorLoss_eq_weightedThreeTerm {latent obs : Spec.Shape} [DecidableRel fun (x1 x2 : ℝ) => x1 > x2] (model : Generative.GAN.Model ℝ latent obs) (xReal : Spec.Tensor ℝ obs) (z : Spec.Tensor ℝ latent) (weight : ℝ) : Generative.GAN.discriminatorLoss model xReal z = Objective.weightedThreeTerm weight (discriminatorObjectiveTerms model xReal z)

LSGAN discriminator loss is the shared three-term objective with zero regularizer.

theorem NN.MLTheory.Generative.Latent.GAN.generatorLoss_zero_of_fake_score_real {latent obs : Spec.Shape} [DecidableRel fun (x1 x2 : ℝ) => x1 > x2] (model : Generative.GAN.Model ℝ latent obs) (z : Spec.Tensor ℝ latent) (hfake : Generative.GAN.fakeScore model z = Generative.GAN.realTarget) : Generative.GAN.generatorLoss model z = 0

If generated samples receive the real target score, the LSGAN generator loss is zero.

theorem NN.MLTheory.Generative.Latent.GAN.discriminatorLoss_zero_of_perfect_scores {latent obs : Spec.Shape} [DecidableRel fun (x1 x2 : ℝ) => x1 > x2] (model : Generative.GAN.Model ℝ latent obs) (xReal : Spec.Tensor ℝ obs) (z : Spec.Tensor ℝ latent) (hreal : Generative.GAN.realScore model xReal = Generative.GAN.realTarget) (hfake : Generative.GAN.fakeScore model z = Generative.GAN.fakeTarget) : Generative.GAN.discriminatorLoss model xReal z = 0

If real samples receive target 1 and generated samples receive target 0, the LSGAN discriminator loss is zero.